Post-condiție
În programare , o condiție postală este o condiție sau un predicat care trebuie să fie întotdeauna adevărat imediat după executarea unei secțiuni de cod sau după o operație într-o specificație formală . Condițiile postale sunt de obicei verificate folosind afirmații din același cod. Adesea, condițiile postale sunt incluse numai în documentația segmentului de cod relevant.
De exemplu: rezultatul unui factorial este întotdeauna un întreg mai mare sau egal cu 1. Prin urmare, un program care calculează factorialul unui număr de intrare va avea ca postcondiție că rezultatul după calcul este un număr întreg și că este mai mare decât sau egalitate 1. Un alt exemplu: un program care calculează rădăcina pătrată a unui număr din intrare trebuie să aibă ca condiție postală că rezultatul este un număr și că pătratul său este egal cu intrarea.
Condiții postale în programarea orientată pe obiecte
În programarea orientată obiect, postcondițiile, împreună cu condițiile prealabile și invarianții , sunt componente ale modelului de proiectare software contractual .
Postcondiția unei proceduri este declararea proprietăților care sunt garantate la finalizarea executării procedurii în sine. [1] Deoarece este legat de contractul rutinei, postcondiția asigură potențialul apelant că, dacă rutina este apelată într-o stare în care sunt îndeplinite condițiile prealabile, proprietățile declarate de postcondiție sunt asigurate.
Exemplu în Eiffel
Următorul exemplu scris în Eiffel setează valoarea atributului hour al unei clase pe baza valorii oferite de apelantul a_hour . Postcondiția urmează cuvântul cheie ensure . În acest exemplu, postcondiția garantează, în cazul în care sunt îndeplinite condițiile prealabile (de exemplu, atunci când a_hour reprezintă un moment valid al zilei), că după executarea set_hour atributul clasei de hour va avea aceeași valoare ca a_hour . Eticheta „ hour_set: ” descrie clauza postcondiționată și servește la identificarea acesteia în caz de încălcare în timpul executării.
set_hour ( a_hour : INTEGER )
- Setați „ora” la „o_ora”
solicita
argument_valid : 0 <= a_hour și a_hour <= 23
do
ora : = o_ora
asigura
oră_set : oră = o_oră
Sfârșit
Postcondiții și moștenire
În prezența moștenirii, rutinele care coboară din clasă (subclasele) moștenesc și contractul, care include condițiile prealabile și postcondițiile care sunt în prezent în vigoare. Aceasta înseamnă că orice implementare sau redefinire a rutinelor moștenite trebuie să adere la contractul moștenit. Condițiile postale pot fi schimbate în rutinele redefinite, dar numai dacă sunt consolidate. [2] Aceasta înseamnă că redefinirea poate crește doar beneficiile pe care le oferă utilizatorilor și nu le poate diminua niciodată.
Notă
- ^ Meyer, Bertrand , Obiect-Oriented Software Construction , ediția a doua, Prentice Hall, 1997, p. 342.
- ^ Meyer, 1997, pp. 570-573.