Abstrakt. Programverifiering görs vanligtvis genom att lägga till specifikationer och invarianter till programmet och sedan bevisa att verifieringsvillkoren är alla sanna. Detta gör programverifiering till ett alternativ till eller ett komplement till testning. Vi beskriver här en annan strategi för programkonstruktion, som vi kallar invariantbaserad programmering, där vi börjar med att formulera specifikationerna och den interna loopen invarianter för programmet, innan vi skriver programkoden själv. Korrektheten i koden är då lätt att kontrollera samtidigt som man konstruerar den. I detta tillvägagångssätt, programverifiering blir ett komplement till kodning snarare än till testning. Syftet är att producera program och programvara som är korrekta genom konstruktion. Vi presenterar en ny typ av diagram, näst invarianta diagram, där programspecifikationer och invarianter (snarare än kontroll) ger den huvudsakliga organisationsstrukturen. Bosättning av invarianter ger en förlängningshierarki som gör det möjligt för oss att uttrycka invarianter på ett mycket kompakt sätt. Vi har studerat genomförbarheten av att formulera specifikationer och loopinvarianter innan själva koden har skrivits i ett antal fallstudier. Vår erfarenhet är att en systematisk användning av siffror, i kombination med en grov idé om det avsedda beteendet hos algoritmen, gör det ganska enkelt att formulera de invarianter som behövs för programmet, att konstruera koden kring dessa invarianter och att kontrollera att det resulterande programmet verkligen är korrekt. Vi beskriver våra erfarenheter av att använda invariantbaserad programmering i praktiken, både från att lära programmerare hur man konstruerar program som de bevisar rätta sig själva, och från att undervisa invariantbaserad programmering för CS-studenter i klass.
En ny variant av denna princip är Backs "invariantbaserade programmering" REF där programinvarianter konstrueras innan den faktiska koden beaktas.
Invariant based programming: basic approach and teaching experiences
{'venue': 'Formal Aspects of Computing', 'journal': 'Formal Aspects of Computing', 'mag_field_of_study': ['Computer Science']}