Derivarea programului - Program derivation

În informatică , derivarea programelor este derivarea unui program din specificația sa, prin mijloace matematice.

A deriva un program înseamnă a scrie o specificație formală, care este de obicei neexecutabilă, și apoi aplică reguli corecte din punct de vedere matematic pentru a obține un program executabil care să satisfacă specificația respectivă. Programul astfel obținut este apoi corect prin construcție. Dovada programului și corectitudinii sunt construite împreună.

Abordarea adoptată de obicei în verificarea formală este de a scrie mai întâi un program, apoi de a oferi o dovadă că acesta se conformează unei specificații date . Principalele probleme în acest sens sunt că

  • dovada rezultată este adesea lungă și greoaie;
  • nu se oferă informații despre modul în care a fost dezvoltat programul; apare „ca un iepure din pălărie”;
  • în cazul în care programul este incorect într-un mod subtil, încercarea de a verifica este probabil să fie lungă și sigur că nu are roade.

Programul de derivare încearcă să remedieze aceste deficiențe prin

  • menținerea probelor mai scurte, prin elaborarea notărilor matematice adecvate;
  • luarea deciziilor de proiectare prin manipularea formală a caietului de sarcini.

Termenii care sunt aproximativ sinonimi cu derivarea programelor sunt: ​​programare transformațională, algoritmică, programare deductivă.

Bird-Meertens Formalismul este o abordare a derivare programului.

Vezi si

Referințe

  • Edsger W. Dijkstra , Wim HJ Feijen, O metodă de programare , Addison-Wesley, 1988, 188 pagini
  • Edward Cohen, Programare în anii ’90 , Springer-Verlag, 1990
  • Anne Kaldewaij, Programare: Derivarea algoritmilor , Prentice-Hall, 1990, 216 pagini
  • David Gries, Știința programării , Springer-Verlag, 1981, 350 de pagini
  • Carroll Morgan (informatician) , Programarea din specificații , Seria Internațională în Informatică (ediția a II-a), Prentice-Hall, 1998.
  • Eric CR Hehner , o teorie practică a programării , 2008, 235 pagini
  • AJM van Gasteren. În forma argumentelor matematice . Note de prelegere în informatică nr. 445, Springer-Verlag, 1990. Învață cum să scrieți dovezi cu claritate și precizie.
  • Martin Rem. „Exerciții mici de programare”, apărute în Science of Programming Computer , Vol.3 (1983) prin Vol.14 (1990).
  • Backhouse Roland. Construirea programului: calculul implementărilor din specificații . Wiley, 2003. ISBN  978-0-470-84882-1 .
  • Derrick G. Kourie, Bruce W. Watson. Abordarea corectă-prin-construcție a programării . Springer-Verlag, 2012. ISBN  978-3-642-27919-5 . Oferă o explicație pas cu pas a modului de a obține algoritmi corecți din punct de vedere matematic folosind rafinamente mici și tratabile.