Femte kursveckan : Planering, ledning och mätning Flashcards
Vad är formella metoder för programverifiering?
Det är ju när vi använder tekniker från matematik och logik för att bevisa att en implementation uppfyller en specifikation. Det bevisar inte att det gäller universellt korrekt, för det kan inte bevisa specifikationens korrekthet.
- Bevisa matematiskt att programmet är korrekt
- Programverifiering
- Konstruera programmet med matematiskt noggranhet, utifrån programspecifikationen.
Vad är Hoare Tripple? {P} S {Q}
Pre condition, en eller flera programsatser, Post condition
● Skrivsättet är alltså {P} S {Q}
där {P} och {Q} är predikat (här kallade assertions) och S är programsatser.
S = en eller flera programsatser
● P är alltså precondition och Q är postcondition.
● Kallas för Hoare Triples efter Tony Hoare som införde dem i Floyd-Hoare logic för formell verifiering av program 1969.
Vad är partiell kontra total korrekthet?
Partiell korrekthet garanterar inte att programmet terminerar:
{P} S {Q} tolkas som att om P är sann initialt och när S terminerar så är Q sann efteråt; men garanterar inte att S nånsin slutar.
Total korrekthet garanterar även terminering: {P} S {Q} tolkas som att om P är sann initialt så kommer S att terminera och Q vara sann efteråt
Total korrekthet kan vara mycket svårare att bevisa, så oftast ”räcker” partiell korrekthet.
För analys av terminering brukar man formulera ett heltalsuttryck, vars värde är positivt, men minskar för varje varv i loopen – detta garanterar att något förändras
Partiellt korrekhet är att vi kan bevisa om den här terminerar då kommer post condition att vara uppfyllt. Total korrekthet är det ovanstående plus att vi bevisar att den kommer att terminera.
Vad är preconditions ?
Någonting som måste vara sant innan, för att vi ska lova att post condition kommer vara uppfyllt.
● Kallas precondition (vad som måste vara sant, för att vi ska kunna uppfylla postcondition)– i vårt fall kan det vara {arr != null}
Vad är postconditions ?
Det är vad vi garanterar är uppfylld om pre condition är uppfylld.
● Detta kallas postcondition – det metoden garanterar uppfylla om den anropas på rätt sätt. Postcondition: efter att metoden är körd, kommer dessa villkoren att gälla, OM metoden anropas på rätt sätt.
Vad är loop-invariant ?
Loop-invarant är någonting som är sant innan loopen och efter varje varav, men inte nödvändigtvis under själva varvet.
Vad är loop-variant ?
Invariant är något oföränderligt. Vanligast är loop-invarianter och klass-varianter.
Klass-invariant är något som måste vara sant för ett objekt. T.ex. att ett objekt måste ha vissa värden, enligt konstruktion.
● En loop-invariant är ett predikat (utsaga, påstående, assertion) som är sann vid ingången till en loop och förblir sann efter varje varv i loopen.
● När en loop är klar ska alltså loop-invarianten vara sann och loopens repetitionsvillkor ska vara falsk.
● Informellt är en loop-invariant ett oföränderligt sant påstående om loopen, och alltså en beskrivning vad loopen egentligen gör.
Är någonting som varierar för varje varv i loopen som ofta används för att bevisa total korrekthet, genom att vi studerar hur den där och vi kan garantera att det når ett värde förr eller senare och när det når värdet terminera loopen.
Vad är klass-invariant ?
Klassinvariant: något som alltid är sant före och efter en metod. T.ex. ett saldo som aldrig får vara under min över max.
Någonting som är sant för en objekt hela tiden utom precis när en metod i klassen körs, för då kan saldo vara negativt för exempel.
Vad är exekverbara utsagor (assertions), speciellt assert satsen i Java
Det är dokumentation i koden som kan köras och kontrolleras. De är inte en del av programflödet och de ska aldrig ha effekt på programmet, de ska bara kontrollera saker men aldrig förändra någonting (VIKTIGT)
De kan stängas av plötsligt och då ska programmet fungera som vanligt. De är oftast avstängda per default pga hastighetsskäl.
McCabes cyclomatic number (complexity)
Numera cyklomatisk komplexitet.
Används för ett mått av komplexitet, som mäts ut på en flödesgraf. Mäter noder och bågar.
Är inte komplett för komplexitet, men kan ta upp en viss grej: linjärt oberoende vägar (som också är antalet testfall som krävs för att täcka alla bågar).
Fan-in, fan-out
Två mått på kommunikation. Exempel på kopplingsmått. Används för att titta på connection complexity. ● Fan-in Antal flöden in – # flows into + # data structures read ● Fan-out Antal flöden ut – # flows out + # data structures written
Traditionella kodmått
● LOC – lines of codes ● McCabe - komplexitetsmått ● Software Science ● Information flow - kopplingsmått ● Ordo/Big-O
LOC – vad ska räknas med?
För att rader kod ska vara intressant borde det finnas en motivering till varför det är intressant, vilken fråga som den ska besvara (varför ska det mätas?). Därefter kan definitionen vara intressant. ● Executable ● Non-executable – Declarations – Compiler directives – Comments on… • On own line • On line with source code • Banners and non-blank spacers • Empty comments • Blank lines ● Programmed ● Generated – av programmet, inte skapade av person ● Converted ● Copied/reused without modifications ● Modified ● Removed – borttagen kod, kanske pga refaktorering ● etc
Software science
Av Halstead. Skapade trend om att skapa en matematisk modell över hur mjukvaruutveckling går till. Ville skapa en formel för det. ● n1 # of unique operators ● n2 # of unique operands ● N1 total # of operators ● N2 total # of operands
Big O
Big O notation is a mathematical notation used to describe the asymptotic behaviour of functions. More precisely, it is used to describe an asymptotic upper bound for the magnitude of a function in terms of another, usually simpler, function.
Wikipedia
Att räkna ut ordo sker manuellt, genom att granska koden. ● Söka igenom en lista O(n) ● Bubble sort O(n2) ● Quick sort O(n log n)
