Odvození programu - Program derivation

v počítačová věda, odvození programu je odvození programu od jeho specifikace matematickými prostředky.

Na odvodit program znamená napsat formální specifikaci, která je obvykle neproveditelná, a poté použít matematicky správná pravidla za účelem získání spustitelného programu vyhovujícího této specifikaci. Takto získaný program je potom správný konstrukcí. Program a správnost důkazy jsou konstruovány společně.

Přístup obvykle přijatý formální ověření je nejprve napsat program a pak poskytnout a důkaz že odpovídá danému Specifikace. Hlavní problémy jsou v tom

• výsledný důkaz je často dlouhý a těžkopádný;
• neposkytuje se žádný pohled na to, jak byl program vyvinut; vypadá to „jako králík z klobouku“;
• pokud by byl program náhodou nějakým rafinovaným způsobem nesprávný, pokus o ověření bude pravděpodobně dlouhý a jistě neúspěšný.

Odvození programu se snaží tyto nedostatky napravit

• udržování kratších důkazů vytvořením vhodných matematických notací;
• rozhodování o návrhu formální manipulací se specifikací.

Pojmy, které jsou zhruba synonymem pro odvození programu, jsou: transformační programování, algoritmizace, deduktivní programování.

The Bird-Meertensův formalismus je přístup k derivaci programu.

Viz také

• Automatické programování
• Logika hoare
• Upřesnění programu
• Návrh na základě smlouvy
• Syntéza programu
• Kód s důkazem

Reference

• Edsger W. Dijkstra, Wim H. J. Feijen, Metoda programováníAddison-Wesley, 1988, 188 stran
• Edward Cohen, Programování v 90. letechSpringer-Verlag, 1990
• Anne Kaldewaij, Programování: Odvození algoritmů, Prentice-Hall, 1990, 216 stran
• David Gries, Věda o programováníSpringer-Verlag, 1981, 350 stran
• Carroll Morgan (počítačový vědec), Programování ze specifikací, International Series in Computer Science (2. vyd.), Prentice-Hall, 1998.
• Eric CR Hehner, Praktická teorie programování, 2008, 235 stran
• A.J.M. van Gasteren. Na tvaru matematických argumentů. Lecture Notes in Computer Science # 445, Springer-Verlag, 1990. Učí, jak psát důkazy s jasností a přesností.
• Martin Rem. „Malá programovací cvičení“, objevila se v Věda o počítačovém programování, Sv. 3 (1983) až sv. 14 (1990).
• Roland Backhouse. Konstrukce programu: Výpočet implementací ze specifikací. Wiley, 2003. ISBN  978-0-470-84882-1.
• Derrick G. Kourie, Bruce W. Watson. Přístup k programování správnosti podle konstrukce. Springer-Verlag, 2012. ISBN  978-3-642-27919-5. Poskytuje podrobné vysvětlení, jak odvodit matematicky správné algoritmy pomocí malých a přitažlivých vylepšení.