Program härledning

Inom datavetenskap är programhärledning härledningen av ett program från dess specifikation, med matematiska medel .

Att härleda ett program innebär att skriva en formell specifikation, som vanligtvis inte är körbar, och sedan tillämpa matematiskt korrekta regler för att få ett körbart program som uppfyller den specifikationen. Det sålunda erhållna programmet är då korrekt genom konstruktion. Program- och korrekthetsbevis är konstruerade tillsammans.

Det tillvägagångssätt som vanligtvis används vid formell verifiering är att först skriva ett program och sedan ge ett bevis på att det överensstämmer med en given specifikation . De största problemen med detta är att

det resulterande beviset är ofta långt och besvärligt;
ingen insikt ges om hur programmet utvecklades; det verkar "som en kanin ur en hatt";
skulle programmet råka vara felaktigt på något subtilt sätt, kommer försöket att verifiera det sannolikt att bli långt och säkert fruktlöst.

Programavledning försöker åtgärda dessa brister genom att

hålla bevis kortare genom att utveckla lämpliga matematiska notationer;
fatta designbeslut genom formell manipulation av specifikationen.

Termer som är ungefär synonyma med programavledning är: transformationsprogrammering, algoritmik, deduktiv programmering.

Bird -Meertens Formalism är en metod för programavledning.

Se även

Edsger W. Dijkstra , Wim HJ Feijen, A Method of Programming , Addison-Wesley, 1988, 188 sidor
Edward Cohen, Programmering på 1990-talet , Springer-Verlag, 1990
Anne Kaldewaij, Programming: The Derivation of Algorithms , Prentice-Hall, 1990, 216 sidor
David Gries, The Science of Programming , Springer-Verlag, 1981, 350 sidor
Carroll Morgan (datavetare) , Programmering från specifikationer , International Series in Computer Science (2:a upplagan), Prentice-Hall, 1998.
Eric CR Hehner , a Practical Theory of Programming , 2008, 235 sidor
AJM van Gasteren. Om formen på matematiska argument . Lecture Notes in Computer Science #445, Springer-Verlag, 1990. Lär ut hur man skriver korrektur med tydlighet och precision.
Martin Rem. "Small Programming Exercises", dök upp i Science of Computer Programming , Vol.3 (1983) till Vol.14 (1990).
Roland Backhouse. Programkonstruktion: Beräkna implementeringar från specifikationer . Wiley, 2003. ISBN 978-0-470-84882-1 .
Derrick G. Kourie, Bruce W. Watson. Korrekthet-by-konstruktion tillvägagångssätt för programmering . Springer-Verlag, 2012. ISBN 978-3-642-27919-5 . Ger en steg-för-steg-förklaring av hur man härleder matematiskt korrekta algoritmer med hjälp av små och lättillgängliga förbättringar.