Expresie booleană
5.1 Specificații bazate pe stări
Specificațiile bazate pe stări descriu sistemele software în termeni de stări și efectele operațiilor asupra stărilor. Astfel de specificații sunt susținute de mai multe limbaje de specificații, pe care le-am grupat în două seturi: limbaje de specificații clasice, cum ar fi Z , B , și VDM , și limbaje de aserțiuni, cum ar fi Eiffel , JML (Java Modeling Language) , și tabelele lui Peters și Parnas . În timp ce limbajele de specificații clasice definesc stările și tranzițiile independent de implementare, limbajele de aserțiuni specifică stările și tranzițiile ca declarații sau adnotări ale programului sursă.
Specificațiile bazate pe stări sunt utilizate ca oracole de testare prin verificarea conformității execuțiilor de testare cu specificațiile. Principala problemă în generarea de oracole de testare din specificațiile bazate pe stări provine din nivelurile diferite de abstractizare dintre specificații și operațiile monitorizate în timpul execuției testului; astfel, specificațiile operațiilor vor fi traduse într-o formă verificabilă. Limbajele de specificații sunt, de obicei, suficient de expresive pentru a reprezenta diverse structuri de date și proprietăți bazate pe stare, dar expresivitatea lor complică traducerea în formă executabilă. Adesea, traducerea face unele ipoteze simplificatoare, cum ar fi limitarea seturilor infinite, de exemplu setul infinit al numerelor naturale, și tratarea elementelor neexecutabile doar parțial și, uneori, necesită o anumită intervenție umană.
În cele ce urmează, discutăm principalele abordări pentru a traduce specificațiile bazate pe stare într-o formă executabilă. Traducerea specificațiilor Z, B și VDM prezintă aceleași probleme legate de structurile de date infinite, expresiile parțial definite și structurile orientate pe obiecte. Traducerea lui Eiffel, JML și a altor limbaje de aserțiuni într-o formă verificabilă prezintă probleme similare, dar la un nivel de abstractizare diferit. În cele ce urmează, prezentăm principalele abordări pentru traducerea specificațiilor bazate pe stări în formă verificabilă cu referire la Z; abordările pentru alte limbaje sunt similare. Apoi, discutăm problemele de compilare a aserțiunilor în verificări executabile referindu-ne la Eiffel, JML și tabelele lui Peters și Parnas.
Compilatorul de predicate de schemă propus de Mikk compilează specificațiile Z în cod C. Pentru fiecare schemă Z, care este unitatea de bază în Z, abordarea generează o funcție C care evaluează predicatele schemei folosind starea programului transmisă funcției ca parametru. Codul generat evaluează predictele schemei cu ajutorul unei strategii de „forță brută”: Având în vedere o stare, codul înlocuiește, în esență, expresiile cu valorile lor, evaluează formulele de calcul propozițional prin utilizarea tabelelor de adevăr și evaluează cuantificările și construcțiile de seturi prin iterația prin structurile de date. Pentru a reduce complexitatea funcțiilor C generate, abordarea propune o etapă de optimizare pentru a se asigura că codul C generat se termină întotdeauna. Pentru a optimiza codul, tehnica definește un subset „executabil” al limbajului Z. Subansamblul este format din predicate finite, cum ar fi formule de calcul propozițional, cuantificări asupra seturilor finite și construcții de seturi bazate pe iterația finită. Tehnica extinde setul de predicate executabile cu un set de reguli pentru a transforma predicatele speciale neexecutabile care îndeplinesc anumite condiții în predicate executabile fără a le modifica semantica. De exemplu, următoarele două reguli elimină cuantificatorii:
unde M este un ansamblu, variabila x reprezintă un element din M, iar P este un predicat. Operatorul -, cunoscut și sub numele de „pata de notație Z”, înseamnă „astfel încât” atunci când este utilizat cu cuantificatorul ∃ și „că”, atunci când este utilizat cu cuantificatorul ∀. De exemplu, ∃ x : M – P înseamnă că există cel puțin o valoare x în M astfel încât predicatul P să fie adevărat. Condiția NotOccur(x, P) indică faptul că x nu este o variabilă liberă în predicatul P. Deși setul M poate fi infinit, compilatorul poate în continuare să compileze specificații care utilizează cuantificatori peste M, atâta timp cât cuantificatorii pot fi eliminați prin aplicarea regulilor de mai sus. Pentru funcțiile definite de utilizator care pot fi introduse prin definiții axiomatice sau generice, compilatorul cere utilizatorului să furnizeze codul corespunzător. Mikk propune, de asemenea, o soluție la problema specificațiilor parțial definite. El folosește VDM-SL ca formă intermediară și compilatorul VDM-SL dezvoltat de Schmidt și Hörcher pentru a traduce specificațiile Z în cod C . Atunci când are de-a face cu expresii parțial definite, adică fie funcții, fie relații care pot fi evaluate nedefinite (notate cu ⊥) atunci când sunt evaluate în afara domeniului lor de definiție, abordarea generează gestionari de excepții.
Extensiile orientate pe obiecte ale Z, cum ar fi Object-Z, exacerbează problemele. McDonald et al. traduc specificațiile Ojbect-Z ale claselor container în cod C++ în trei etape: optimizare, cartografiere structurală și traducerea predicatului . În etapa de optimizare, ei rearanjează specificația pentru a simplifica traducerea ulterioară prin mai multe etape, inclusiv înlocuirea variabilelor constante cu valorile lor și eliminarea variabilelor secundare și a îmbogățirii schemei. În etapa de cartografiere structurală, aceștia cartografiază structurile din specificația Object-Z în elementele de cod corespunzătoare: Constantele și variabilele din specificație în variabile cu inițializări corespunzătoare, iar tipurile de variabile în tipuri primitive C++ sau în clasele corespunzătoare din biblioteca setului de instrumente Z utilizate de tehnică. De exemplu, ei mapează tipurile de numere întregi și booleene în int, iar tipul de seturi de numere întregi în z_set<int >. Ei mapează schema de inițializare la un constructor, iar schemele de operații la funcții membre, creează o funcție membră specială, inv(), pentru a verifica invarianții clasei și generează o clasă de excepție pentru fiecare schemă de excepție.
În traducerea predicatului DeepL, tehnica se concentrează pe modul de generare a codului pentru verificarea stării programului, în loc de evaluarea predicatelor. De exemplu, traducerea împiedică funcția inv() să apeleze orice altă funcție membră, pentru a evita recursivitatea infinită. Într-un constructor, invariantul clasei este verificat la ieșirea acestuia.
Richardson et al. se concentrează asupra sistemelor critice din punct de vedere al timpului, tratează o combinație între logica Z și logica intervalelor temporale și propun o traducere a specificațiilor în oracole de testare prin intermediul interpretării simbolice. Interpretarea simbolică atribuie denumirile simbolice din specificații intrărilor de stimuli și variabilelor de stare inițială, prin referire la corespondențele de date și control. Apoi, interpretarea simbolică interpretează fiecare cale de control din specificații, adică creează o afirmație care exprimă condiția privind datele din specificații pe baza stării simbolice la fiecare punct de control al specificației. Un punct de control al specificației este un element relevant, cum ar fi un eveniment parametrizat, o tranziție și o operație. După interpretarea simbolică a specificației Z, informațiile oracolului sunt reprezentate sub forma unei liste de scheme Z relevante și a afirmațiilor lor corespunzătoare, care sunt verificate dacă schema este invocată. Executarea unui caz de testare se referă la o intrare concretă de testare din care variabilele și evenimentele concrete sunt legate de omologii lor din clasa de testare (fiecare clasă de testare este o partiție a intrării de testare). Executarea cazului de test produce un profil de execuție, iar evenimentele concrete și valorile variabilelor conținute în profilul de execuție sunt mapate la nivelul oracolului pentru a verifica coerența lor cu informațiile din oracol.
Limbajele de afirmare îmbină specificațiile cu codul sursă, simplificând astfel, dar nu eliminând problema traducerii. Aserțiunile sunt susținute de diferite limbaje și metodologii. Proiectarea prin contract este o paradigmă de proiectare software care postulează proiectarea comună a codului și a aserțiunilor. Proiectarea prin contract a fost propusă de Meyer și este pe deplin susținută de limbajul de programare Eiffel . Spre deosebire de limbajele de specificații generale, cum ar fi Z, specificațiile din Eiffel, numite contracte, sunt încorporate în codul sursă și definesc obligațiile și beneficiile componentelor software care comunică prin intermediul unor interfețe bine concepute. În limbajele care suportă contracte, obligațiile și beneficiile clienților sunt exprimate ca pre și postcondiții ale furnizorilor de servicii. Codul sursă este îmbogățit cu invarianți care reprezintă proprietăți de stare care trebuie să se mențină în timpul oricărei interacțiuni.
Contractele au fost extinse la multe limbaje. iContract a fost primul instrument care a susținut contractele în Java . În iContract, contractele sunt scrise ca și comentarii de cod cu ajutorul unor etichete speciale. Contractele suportate de iContract sunt expresii booleene conforme cu sintaxa Java, cu excepția câtorva extensii sintactice care includ cuantificarea universală (∀), cuantificarea existențială (∃) și implicația (→). Aceste extensii sunt concepute pentru a simplifica traducerea lor în cod Java. De exemplu, the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: „if C then check I.”
În afară de traducerea simplă a expresiilor booleene, iContract abordează aspecte legate de ciclul de viață al obiectelor, domeniul de aplicare al variabilelor și moștenirea, cele mai multe dintre acestea fiind specifice programării orientate pe obiecte. Cele mai importante reguli legate de ciclul de viață al obiectelor sunt următoarele:
În construcția unui obiect, precondițiile trebuie verificate la începutul construcției, în timp ce invarianții și postcondițiile sunt verificate numai dacă construcția se termină normal (fără excepții).
Pentru invocările normale de metode pe obiecte, precondițiile și postcondițiile sunt verificate la intrarea și ieșirea metodelor invocate, iar invarianții nu sunt verificați pentru metodele private.
În distrugerea unui obiect, nu este necesară nicio verificare. Astfel, nu se inserează niciun cod de verificare în metodele finalize().
Predicatele utilizate în postcondiții se referă adesea atât la valoarea de întoarcere a metodei, cât și la „vechea” valoare (sau „valoarea de intrare”) a unor variabile. iContract sintetizează o pseudo-variabilă, numită return, pentru a reprezenta valoarea de întoarcere, stochează valorile variabilelor la intrare și le face accesibile ca nume de variabile cu postfixul @pre. expresii, referințele la obiect ale acestora sunt stocate direct. iContract permite apeluri la metode membre în contracte. Ca urmare, pot exista potențiale recursiuni infinite în verificarea invarianților. Pentru a rezolva această problemă, iContract ține evidența profunzimii de recursivitate pentru fiecare obiect din cadrul fiecărui fir și verifică numai invarianții cu profunzimea 0. Mecanismele de extindere a tipurilor din Java au mai multe implicații asupra modului în care ar trebui tratate contractele tipurilor. iContract propagă contractele urmând următoarele reguli:
Invarianții sunt conjuncți, adică invarianții unui subtip sunt conjuncția invarianților tuturor supratipurilor sale.
Postcondițiile sunt conjuncte, adică postcondiția unui subtip este conjuncția postcondițiilor tuturor supertipurilor sale.
Precondițiile sunt disjuncte, adică precondiția unui subtip este disjuncția precondițiilor tuturor supertipurilor sale.
JML este un limbaj popular de specificații comportamentale care suportă Design by Contract în Java . Contractele JML se prezintă sub forma unor comentarii speciale în Java. JML exprimă precondițiile, postcondițiile și invarianții sub formă de expresii booleene precedate de cuvintele cheie requires, ensures și, respectiv, invariant, și utilizează metoda încorporată \ old(x) pentru a reprezenta valoarea lui x înainte de o operație. Asemănător cu notația ▵ din Z, JML oferă cuvântul cheie modifies pentru a indica variabilele care sunt modificate în corpul unei metode. În plus, JML tratează mai multe caracteristici orientate pe obiecte, cum ar fi vizibilitatea și moștenirea.
JML stă la baza multor abordări pentru generarea de oracole de testare. Bhorkar a propus o tehnică de traducere a contractelor JML în aserțiuni Java . Deși suportă numai precondiții, această tehnică abordează probleme legate de variabilele numai de specificație, rafinament, moștenirea specificațiilor și confidențialitate. Similar cu iContract, tehnica tratează moștenirea contractelor prin conjuncția și disjuncția contractelor în funcție de tipurile lor. Tehnica utilizează, de asemenea, un tabel hash (pe fir de execuție) pentru a evita recurențele în verificarea în timp de execuție. Expresiile care utilizează cuantificatori sunt considerate ca neexecutabile de către tehnică și nu se generează cod Java pentru astfel de expresii.
Korat a propus o tehnică pentru a genera atât cazuri de testare, cât și oracole din specificațiile JML . Tehnica lui Korat generează cazuri de test din precondiții și invarianți și oracole din postcondiții și invarianți. Araujo et al. au extins JML prin adăugarea de contracte concurente și au propus un suport de execuție pentru a permite verificarea în timp de execuție a aserțiunilor care specifică proprietăți concurente .
Peters și Parnas au introdus o abordare pentru a genera oracole de testare din documentația formală . Documentația este dată într-o formă tabelară care constă din relații care specifică interfețele procedurilor și este tradusă în oracole în cod C și C++. Elementul central al documentației formale constă în expresii de predicat scrise într-o variantă de logică a predicatului cu construcții speciale pentru a trata funcțiile parțiale. Similar altor tehnici de oracole bazate pe specificații, această tehnică tratează cuantificatorii prin restricționarea lor la seturi finite.
Pentru a permite iterații peste seturi de elemente cu cuantificatori, Peters și Parnas introduc predicate definite inductiv. Pentru un set S (care urmează să fie utilizat în cuantificări), un predicat definit inductiv P este definit cu trei elemente I, G și Q. Setul inițial I conține un număr finit de elemente, G este o funcție, numită „funcție generatoare”, care generează elementele din set, iar Q este un predicat care caracterizează proprietățile setului. Setul S este definit ca fiind cel mai mic set construit în pașii inductivi de mai jos:
S0 = I
Sn + 1 = Sn ∪ {G(x)|x ∈ Sn ∧ Q(x)}
I, G și Q trebuie să fie definite pentru a satisface o condiție specială care asigură că setul construit S este finit .
Peters și Parnas propun o abordare pentru a traduce documentațiile tabulare în cod C . Deoarece forma expresiilor utilizate în documentații este bine definită, traducerea se face în mod sistematic.
Pentru derivarea oracolelor de testare se utilizează și alte specificații bazate pe stări. Modelele UML sunt, în general, informale; cu toate acestea, Bouquet et al. au definit un subansamblu al UML 2.1, denumit UML-MBT, care este suficient de precis pentru a genera automat cazuri de testare. UML-MBT include diagrame de clasă, mașini de stare și un subset de OCL 2.0. Bouquet et al. utilizează specificații scrise în VDM-SL pentru a genera oracole de testare.
.