10.3_specificarea_formala_a_programelor.doc

Metode de specificare si de dezvoltare formala a programelor O specificatie este numita formala daca: -este scrisa urmând o sintaxa bine definita, cum este aceea a limbajelor de programare; -sintaxa este însotita de o semantica riguroasa.  Metodele de specificare formala se bazeaza pe notatii matematice pentru a descrie exact proprietatile pe care trebuie sa le aiba un sistem fara a constrânge modul de realizare a lor.  O specificatie formala descrie ceea CE trebuie sa faca sistemul, fara a preciza CUM.  O astfel de abstractizare este extrem de utila în procesul de dezvoltare a programelor.  O specificatie formala reprezinta un punct de referinta unic si fiabil pentru toti cei care analizeaza cerintele clientilor, cei care implementeaza programele, cei care le testeaza si care realizeaza documentatia sistemului.  Scrierea unei specificatii formale permite întelegerea aprofundata a sistemului de dezvoltat.  Ea pune în evidenta ambiguitatile existente în specificatiile neformale, al caror cost, atunci când sunt descoperite târziu, este bine cunoscut. Specificatiile formale sunt adesea însotite de explicatii în limbaj natural. Ele nu exclud metodele grafice de analiza si proiectare. Analize privind utilizarea metodelor formale în industrie arata ca in anii ’90, 31% dintre întreprinderi au combinat metodele formale cu cele semi-formale. De exemplu, în cazul unei abordari functionale, se folosesc diagrame de flux pentru a structura specificatia si limbajul Z pentru a descrie comportamentul fiecarei componente.

1

 In cazul unei conceptii orientate obiect, o specificatie bazata pe notatiile UML poate fi completata prin specificatii scrise într-un limbaj formal: OCL (Object Constraint language) Alte limbaje formale: Z++ si VDM++ (este specificata formal fiecare clasa). Proprietatile unei specificatii formale pot fi demonstrate prin metode matematice. Exista deja instrumente de demonstrare pentru câteva limbaje de specificare formala (B, VDM, VDM++).  Pornind de la o specificatie globala a sistemului, scrisa într-un limbaj formal, se poate efectua o proiectare prin rafinari succesive. Fiecare rafinare a unei specificatii produce o alta specificatie, mai detaliata si mai apropiata de limbajul de implementare. Corectitudinea fiecarei rafinari trebuie sa fie demonstrata formal: noua specificatie conserva proprietatile specificatiei din care a provenit. In acest caz se spune ca se efectueaza o dezvoltare formala a programului. Costul unei astfel de dezvoltari este foarte mare, datorita demonstratiilor de corectitudine a rafinarilor, dar se poate justifica pentru sistemele critice (utilizate în supravegherea centralelor nucleare, a mersului trenurilor, a avioanelor si navelor spatiale, în sistemele bancare).  Alte avantaje ale specificatiilor formale sunt legate de teste si de întretinere. Plecând de la o specificatie formala pot fi generate automat cazuri de test. Precizia exprimarii formale a cerintelor simplifica si reduce testele de validare. In concluzie, exista doua tipuri de utilizari ale specificatiilor formale:

2

1) Ca mijloc de specificare globala a unui program si la diferite nivele de proiectare, implementarea fiind efectuata prin translatarea "manuala" a specificatiei formale. In acest caz specificatiile formale favorizeaza: - întelegerea sistemului de dezvoltat; - comunicatia dintre cei care participa la procesul de analiza a cerintelor, de dezvoltare si de întretinere; - reducerea perioadei de dezvoltare; - fiabilitatea; - întretinerea.

2) Ca mijloc de dezvoltare, programul fiind obtinut prin rafinari succesive ale specificatiilor formale pâna la nivelul unui limbaj executabil.  Dezvoltarea formala a fost utilizata pâna în prezent numai pentru sisteme critice.  Principalul sau scop este de a se asigura fiabilitatea programului si conformitatea sa cu specificatia initiala.

Exista mai multe metode de specificare formala, fiecare fiind adaptata mai bine unei anumite clase de aplicatii. De exemplu, specificatiile algebrice sunt adecvate descrierii tipurilor de date abstracte, VDM si Z folosesc de asemenea tipuri de date abstracte dar adauga notiunea de stare, limbajul LOTOS pernite specificarea proceselor paralele. Metoda cea mai simpla de specificare, dar si cea mai incompleta, se bazeaza doar pe logica cu predicate de ordinul I.

3

1. Specificatii de intrare/iesire Vederea cea mai abstracta asupra unei componente program consta în a o considera ca o "cutie neagra". Singurele caracteristici vizibile din exterior sunt intrarile si iesirile sale. O specificatie de intrare/ iesire precizeaza constrângerile asupra intrarilor si asupra iesirilor unei componente program. Deoarece constrângerile sunt exprimate prin predicate, specificatiile de intrare/iesire mai sunt numite si specificatii de pre si post conditii.

Exemple 1.1.

Consideram o functie care primeste prin lista de parametri un tablou

de numere intregi si un numar intreg. Functia intoarce ca rezultat indicele elementului de tablou a carui valoare este egala cu numarul dat. Ea poate fi specificata astfel: int cauta(int *X, int n, int num) pre : exists i in [0..n-1] : X[i]=num post : X’’[cauta(X,n,num)] = num and X’=X’’ Notatii : X’ – tabloul X inainte de executia functiei X’’ – tabloul X dupa executia functiei Pre si post conditiile sunt predicate peste intrarile si iesirile unei functii.  Preconditia este o conditie care trebuie sa fie indeplinita de datele de intrare pentru ca rezultatul intors sa fie cel specificat de postconditie.

4

 Postconditia specifica rezultatul executiei functiei pentru date valide. In exemplul de mai sus, prima parte a postconditiei precizeaza ce reprezinta valoarea intoarsa de functie; partea a doua specifica faptul ca functia nu modifica tabloul X.  Specificatia poate fi completata cu un predicat care exprima comportarea functiei atunci când nu este indeplinita preconditia (atunci când numarul transmis ca parametru nu exista in tablou). Un astfel de predicat poate fi: error : cauta(X,num)=n In cazul de fata acest predicat este suficient pentru a preciza comportarea functiei la date de intrare eronate. In general însa, trebuie furnizate mai multe astfel de predicate. Din specificatie nu rezulta daca elementele tabloului X sunt distincte, iar daca nu sunt distincte atunci ce valoare intoarce functia in cazul in care numarul specificat se afla pe mai multe pozitii in tabloul X. O alta specificatie (mai completa) a aceleiasi functii poate fi urmatoarea:-CURS Pentru a exprima faptul ca tabloul X este ordonat crescator, se poate folosi expresia: for-all i, j in [0..nr-1] : i<j  X[i] <= X[j] In unele cazuri, pentru simplificarea expresiilor se definesc predicate. De exemplu: ordonat(int *X, int nr) = for-all i, j in [0..nr-1] : i<j  X[i] <= X[j] Atunci, preconditia se poate scrie astfel: pre : nr>0 and ordonat(X, nr) iar la postconditie se adauga de asemenea ordonat(X, nr).

5

1.2. Fie o functie care determina toate numerele prime cuprinse între doua numere, N1 si N2, date prin lista de parametri. Numerele prime sunt memorate într-un tablou, T, transmis de asemenea prin lista de parametri. Valoarea întoarsa de functie reprezinta numarul de numere prime memorate în tabloul T. int Prime (int N1, int N2, int *T) pre

: N1>2 and N2>N1

post : // toate numerele din T sunt prime for-all i in [0..Prime(N1,N2,T)-1] : prim(T[i]) and // toate numerele din T sunt diferite intre ele for-all i,j in [0..Prime(N1,N2,T)-1] : i#j  T[i] # T[j] and // T contine toate numerele prime cuprinse intre N1 si N2 for-all k in [N1..N2] : ( prim(k)  exists i in [0..Prime(N1,N2,T)-1] : k=T[i] ) error : Prime(N1,N2,T)=0 bool prim (int N) pre : N>2 post : prim = ( for-all i in [2..sqrt(N)]: N mod i #0 ) error: prim=false

6

Alt exemplu :CURS Limitari :CURS Exercitii :CURS Specificatiile de intrare/iesire pot fi folosite si pentru descrierea functiilor membre ale unei clase. In aceste cazuri, in expresiile pre si post conditiilor apar si variabilele de instantiere (câmpurile) ale clasei.

“Design by contract”, limbajul Eiffel  CURS 2. Specificatii algebrice Au fost introduse ca metoda de specificare a tipurilor de date abstracte. Ulterior ele s-au folosit si pentru descrierea claselor de obiecte.  O specificatie algebrica defineste un tip de obiecte prin operatiile care pot fi aplicate obiectelor din exterior.  Operatiile sunt definite exclusiv prin relatiile dintre ele, care se pastreaza pentru orice reprezentare concreta a obiectelor clasei.  Specificatia algebrica nu precizeaza nici reprezentarea prin date a obiectelor, nici modul de implementare a operatiilor. Exemplu: Clasa Tipuri:

stiva stiva; Importa: X, Boolean;

Functii: empty(stiva)  Boolean new()  stiva push(X,stiva)  stiva pop(stiva) ─| stiva top(stiva) ─| X Axiome: empty(new()) 7

not empty(push(x,s)) pop(push(x,s)) = s top(push(x,s))=x Preconditii: pop(s) : not empty(s) top(s) : not empty(s) end stiva Specificatia este alcatuita din patru sectiuni: 1) Tipuri, în care sunt listate tipurile folosite în cadrul specificatiei: tipul obiectelor clasei si tipurile definite în alte specificatii, numite si tipuri importate. 2) Functii, numita si semnatura clasei, contine declaratiile operatiilor clasei, fiecare prin domeniul sau de definitie si domeniul rezultatului; se folosesc notatii de forma: nume-operatie : AxB  C sau nume-operatie (A,B)  C 3) Axiome, in care sunt definite relatiile dintre operatii. Aceasta sectiune reprezinta partea semantica a specificatiei. Doua specificatii algebrice pot avea aceeasi semnatura, deosebindu-se prin partea semantica (proprietatile semantice ale operatiilor). 4) Preconditii. Aceasta sectiune este necesara atunci cand unele dintre operatiile clasei sunt functii partiale, adica functii care nu sunt definite pentru toate obiectele clasei. De exemplu, functiile top si pop nu sunt definite pentru o stiva goala. Sunt trei tipuri de operatii. Astfel, daca T este tipul obiectelor clasei specificate, atunci: f(…..)  T se numeste constructor f(…, T,…)  r unde r este un atribut al obiectelor clasei, se numeste operatie de interogare

8

f(…,T,…)  T se numeste operatie de transformare (creaza un obiect nou pornind de la unul existent) In concluzie : 

Specificatia algebrica a unei clase defineste obiectele clasei independent de orice reprezentare structurala a lor.



Operatiile asociate obiectelor sunt descrise într-o maniera abstracta, printr-un set de axiome, care sunt satisfacute pentru orice reprezentare concreta a obiectelor. Specificatiile algebrice sunt declarative, ceea ce le confera caracterul abstract.



Exercitiu : Sa se adauge la specificatie o operatie Replace (stiva, X), care inlocuieste elementul din varful stivei. Alte exercitii :CURS Exista mai multe limbaje de specificare algebrica pentru care s-au construit medii de specificare dedicate. Mediile de specificare contin instrumente de:  editare a specificatiilor;  prototipare;  demonstrare a teoremelor;  generare a cazurilor de test si altele.

3. Notatia Z Notatia Z se bazeaza pe teoria multimilor si logica cu predicate de ordinul I. Astfel, obiectele sunt modelate prin tipuri de date matematice iar efectul operatiilor este descris abstract folosind predicate. Specificatia unui sistem este descompusa în parti mici numite “scheme”(in engleza, “schemas”). Schemele sunt utilizate pentru a descrie atât aspectele statice cât si cele dinamice ale unui sistem. 9

    

Aspectele statice cuprind: starile în care se poate afla sistemul specificat; relatiile de invarianta care se pastreaza la trecerea dintr-o stare în alta. Aspectele dinamice sunt: operatiile potentiale; relatiile dintre intrarile si iesirile lor; modificarile de stare pe care le produc.

Exemplu: un sistem “asistent” Asistentul trebuie sa tina evidenta studentilor care fac parte dintr-o clasa si sa le atribuie note. Numarul de studenti dintr-o clasa este limitat. Studentii trebuie sa efectueze un anumit numar de teme. Fie NTEME acest numar. Fiecare tema este predata asistentului separat. Asistentul trebuie sa marcheze numarul de teme pe care le-a predat fiecare student. Atunci cand un student paraseste clasa, asistentul trebuie sa-I comunice nota obtinuta, carese calculeaza cu formula: nota=(NPRED/NTEME) x 10, unde NPRED reprezinta numarul de teme predate. Sistemul va permite urmatoarele operatii: 1. Adaugarea unui student nou pe lista studentilor unei clase; 2. Marcarea unui student care preda o tema; 3. Aflarea situatiei curente a unui student; sistemul va afisa câte teme a predat studentul; 4. Stergerea unui student din lista studentilor unei clase; sistemul va afisa nota obtinuta de student. In universul problemei specificate neformal mai sus exista studenti. Pentru moment nu este necesar sa se dea o reprezentare studentilor. Vom introduce multimea STUDENT ca un tip de baza al specificatiei. Nu s-a precizat numarul de teme (numarul NTEME) si nici numarul maxim de studenti dintr-o clasa. Putem sa le specificam ca fiind niste constante de tip “Numar întreg”: N, ceea ce în Z se declara astfel: | NTEME : N | MAXST : N Primul aspect al unui sistem, care trebuie descris într-o specificatie Z, este spatiul sau de stari. Pentru aceastase foloseste o schema. Astfel, schema

10

”Asistent” de mai jos reprezinta starile abstracte ale sistemului pe care vrem sa-l specificam: Asistent Inregistrati : PSTUDENT Predate : STUDENT ─| 0..NTEME # Inregistrati <= MAXST Inregistrati = dom Predate

Schema contine o parte declarativa, deasupra liniei orizontale centrale, si o parte care exprima constrângerile asupra valorilor variabilelor declarate. Aceste constrângeri trebuie sa fie satisfacute pentru orice stare a sistemului. Ele constituie invariantul sistemului. “Inregistrati” este multimea studentilor care fac parte din clasa. Notatia PSTUDENT specifica “multimea tuturor sub-multimilor multimii STUDENT”. Orice multime de obiecte ale carei elemente sunt toate de tip t este ea insasi un obiect de tip multime Pt. Marcile asociate studentilor, care indica numarul de teme predate de fiecare student, sunt numere cuprinse între 0 si NTEME. Corespondenta între un student si marca sa este reprezentata prin functia “Predate”. Ea este o functie partiala (ceeace este specificat prin simbolul ─|) deoarece nu este definita pentru orice student, ci numai pentru cei care fac parte din multimea “Inregistrati”. Domeniul sau este deci restrâns la aceasta multime, ceea ce este specificat prin predicatul Inregistrati = dom Predate. I figura de mai jos este ilustrata o stare posibila a sistemului. Ea cuprinde trei studenti în multimea “Inregistrati” si marcile lor, asociate prin functia “Predate”: Inregistrati ={Maria, Ana, Gigel} Predate = {Maria | 1, Ana |2, Gigel |1}

STUDENT Inregistrati

MARCA

11

Maria Ana Gigel

1 2

Starea initiala a sistemului este de asemenea descrisa printr-o schema: Init Asistent Inregistrati = Specificam in continuare operatiile cerute. Fiecare operatie este specificata prin: intrarile si iesirile sale, relatiile dintre intrari si iesiri, modificarile de stare pe care le produce. De regula, efectul unei operatii este dependent de starea curenta a sistemului. De exemplu, efectul operatiei “Adauga” depinde de numarul de studenti deja inregistrati. Daca acest numar este mai mic decât cel maxim, atunci studentul este inregistrat si asociat cu marca zero. Operatia este descrisa in schema de mai jos: Adauga  Asistent e? : STUDENT e?  Inregistrati   Inregistrati <MAXST Predate’ = Predate  { e? | 0}

Notatia “ Asistent” semnaleaza faptul ca schema descrie o schimbare de stare. Ea introduce patru variabile: Inregistrati, Predate, Inregistrati’ si Predate’. Primele doua reprezinta starea sistemului inainte de modificare iar ultimele doua, dupa modificare. Fiecare pereche de variabile este in mod implicit constrânsa sa satisfaca invariantul - el trebuie sa fie adevarat atât inainte cât si dupa operatie. Intrarea operatiei este reprtezentata prin variabila e?. Prin conventie, numele intrarilor sunt urmate de semnul de întrebare iar numele iesirilor de semnul de exclamare.

12

Prima linie a specificatiei de sub linia orizontala centrala este o preconditie a succesului operatiei. Daca preconditia este satisfacuta, atunci linia urmatoare indica extensia functiei Predate pentru a se lua în considerare noul student. Dupa operatie, multimea Inregistrati va contine un nou element: Inregistrati’=Inregistrati  {e?} Aceasta specificatie nu este inclusa in schema, ea rezultând din extensia functiei Predate. Inregistrati’ = dom Predate’ = dom (Predate  {e? |0}) = dom Predate  dom { e? |0} = dom Predate  {e?} = Inregistrati  {e?} Demonstrarea unor proprietati ca cea de mai sus ne permite sa stabilim daca specificatia este corecta. Specificatiile celorlalte operatii cerute sunt urmatoarele: Marcheaza  Asistent e? : STUDENT e?  Inregistrati Predate’=Predate  { e? | Predate(e?) + 1} Aici preconditia specifica faptul ca studentul trebuie sa fie inregistrat. Daca este atunci se adauga1 la numarul sau de teme. Notatia Predate(e?) specifica marca (numarul de teme) pusa in corespondenta studentului e? de functia Predate. Efectul operatiei  este urmatorul: se elimina din relatia Predate perechea având e? la stânga apoi se adauga larelatie perechea {e? | Predate(e?) + 1}. Sterge  Asistent 13

e? : STUDENT nota! : 0..10 e?  Inregistrati nota!=Predate(e?)/NTEME*10 Inregistrati’ = Inregistrati \ {e?} Interogheaza  Asistent e? : STUDENT teme! : 0..NTEME e?  Inregistrati teme! = Predate(e?) Simbolul  , pronuntat Xi, declara ca operatia nu schimba starea sistemului. Specificatiile scrise pânaacum stabilesc într-o maniera concisasi clara comportamentul sistemului atunci când intrarile operatiilor satisfac preconditiile. Schemele operatilor pot fi extinse pentru adescrie comportamentul la intrari nevalide. De exemplu: Interogare  Asistent e? : STUDENT teme! : 0..NTEME r! : RASPUNS (e? Inregistrati  teme! =Predate(e?)  r! =Succes  (e?  Inregistrati  r! = NeInregistrat ) Variabila de iesire va furniza raspunsul sistemului oricare ar fi intrarea operatiei. O alta alternativa este de a descrie separat (prin scheme diferite) comportamentul fiecarei operatii la intrari valide, respectiv nevalide. Apoi, prin compunerea schemelor vom obtine specificatiile complete. Adaugam iesirea suplimentara r!, de tip RASPUNS, fiecareia dintre

14

operatiile sistemului. Atunci când o operatie se termina cu succes aceasta variabila va lua valoarea Succes. Altfel, va lua o valoare particulara ( NeInregistrat, DejaInregistrat, ClasaOcupata) indicând cauza insuccesului. Tipul RASPUNS se defineste astfel: RASPUNS :: = Succes | NeInregistrat | DejaInregistrat | ClasaOcupata Definim schema Succes, specificând ca rezultatul corespunde unei intrari valide, fara a descrie cum se schimba starea:

Succes r! : RASPUNS r! = Succes Se definesc schemele care descriu cazurile de eroare. De exemplu: Ne-Inregistrat  Asistent e? : STUDENT r! : RASPUNS e?  Inregistrati r! = NeInregistrat

Specificatiile complete (“robuste”) ale operatiilor cerute vor fi: Adaugare (Adauga  Succes )  Deja-Inregistrat  Clasa-Ocupata Marcare  (Marcheaza  Succes )  Ne-Inregistrat Stergere  (Sterge  Succes )  Ne-Inregistrat

15

Interogare  (Interogheaza  Succes )  Ne-Inregistrat

16