Az Alphard nyelv leglényegesebb tulajdonsága az, hogy lehetõséget ad a programozónak a program absztrakt adattípusainak megvalósítását felügyelni és ellenõrizni.
Azt mondhatjuk, hogy az Alphard verifikációs technikája arra épít,
hogy a form valóban azokkal a tulajdonságokkal bír, amit a
specifikációs részben definiál.
Ennek az igazolásához a Hoare féle technikát alkalmazza:
- - invariáns,
- - inicializáló rész,
- - elõ és utófeltételek minden eljárásra.
A teljességhez hozzátartozik az is, hogy a nyelv tervezõi egy absztrakt típusok megvalósítására és verifikálására alkalmas nyelvet szerettek volna létrehozni, az automatikus verifikációs rész azonban nem készült el. Lehetõségünk van azonban tételeket konstruálni egyszerû módon az adattípusainkhoz, és azok bizonyításával láthatjuk be azok helyességét.
Absztrakt adattípusok megvalósítása a forma segítségével
A nyelv típusspecifikációja az algebrai specifikációra épül.
Az Alphard nyelvvel kapcsolatos publikációkban a forma definíciója bizonyos
változásokon esett át. A lent leírt meghatározás ez elsõ idõszak cikkeiben
szerepel, amely cikkek elsõsorban a verifikáció témájával foglalkoznak,
ezért különbözik ez a Deklarációk részben megadott form
definíciótól.
form FormName (p0: params) is
specifications
requires B_req(p0) -> paraméterekre ad korlátozást
let FormName = < ... x ... > -> absztrakt adatszerkezet
where constr(x)
invariant I_a(FormName) -> absztrakt invariáns
initially B_init(FormName) -> inicializáló feltétel
functions
f1 (formal parameters) return formal output parameter
pre f1
post f1
...
representation
unique ... init ... -> konkrét adatszerkezetek, struktúrák
rep ... -> reprezentáló fgv
invariant I_c -> konkrét invariáns
states ... -> egyes esetekben az adatobjektumok
milyen állapotban lehetnek
implementation
body f1, in B_in, out B_out;
...
endform
A forma deklarálása után az alábbi helyességi kritériumokat tudjuk megfogalmazni:
- 1. Reprezentáció helyessége
I_c(x) => I_a(rep(x))
- 2. Kezdeti objektum képe is kezdeti objektum
{ B_req } C_init { B_init(rep(x)) ÉS I_c(x) }
- 3. A konkrét mûveletek helyessége:
Minden f konkrét mûveletre:
{ B_in(x) ÉS I_c(x) } y:=f(x) { B_out(x,y) ÉS I_c(x,y) }
- 4. Absztrakt és konkrét tér közötti kapcsolat helyes:
Minden f konkrét mûveletre:
a. (I_c(x) ÉS pre(rep(x))) => B_in(x)
b. (I_c(x) ÉS pre(rep(x')) ÉS B_out(x,y)) => post(rep(x),rep(y))
Példa:
form istack(n:integer) is
specifications
requires n>0;
let istack = < ... x ...> where x :integer;
invariant 0<=length(istack)<=n;
initially istack = nullseq;
functions
push(s:istack; x:integer) pre 0<=length(s)<n posts=s'~x;
pop(s:istack) pre 0<length(S)<=n post s=leader(s');
top(s:istack) returns x:integer pre 0<length(s)<=n post
x=last(s');
empty(s:istack) returns b:boolean post b=(s=nullseq);
representation
unique v:vector(integer,1,n), sp:integer init sp:=0;
rep (v,sp)=seq(v,1,sp);
invariant 0<=sp<=n;
states
mt when sp=0,
normal when 0<sp<n,
full when sp=n,
err otherwise;
implementation
body push out (s.sp=s.sp'+1 and s.v=alpha(s.v',s.sp,x))=
mt,normal::(s.sp:=s.sp+1; s.v[s.sp]:=x);
otherwise::FAIL;
body pop out (s.sp=s.sp'-1)=
normal,full::s.sp:=s.sp-1;
otherwise::FAIL;
body top out (x=s.v[s.sp])=
normal,full::x:=s.v[s.sp];
otherwise::FAIL;
body empty out (b=(sp=0))=
normal,full::b:=false;
mt::b:=true;
otherwise::FAIL;
endform
- 1. Reprezentáció helyessége: Áll: 0<=sp<=n --> 0<=length(rep(x))<=n Biz: length(rep(x))=length(seq(v,1,sp))=sp.
- 2. Kezdeti objektum képe kezdeti objektum: Áll: n>0 {sp:=0} rep(v,0)=nullseq ÉS 0<=sp<=n Biz: rep(v,0)=seq(v,1,0)=nullseq. Például a push függvényre:
- 3. Konkrét mûvelet helyes Áll: (0=s.sp VAGY 0<s.sp<n) ÉS 0<=s.sp<=n { s.sp:=s.sp+1; s.v[s.sp]:=x } s.sp=s.sp'+1 ÉS s.v=alpha(s.v',s.sp,x) ÉS 0<=s.sp<=n Biz: 0<=s.sp<n --> 0<=s.sp+1<=n
- 4. Absztrakt és konkrét tér közötti kapcsolat helyes
- a. B_in-re igaz az implikáció: B_in az azonosan igaz.
- b. B_post-ra igaz az implikáció: Áll: (0<=s.sp<n ÉS 0<=length(rep(s.v,s.sp'))<n ÉS s.sp=s.sp'+1 ÉS s.v=alpha(s.v',s.sp,x) --> s=s'~x Biz: s=rep(s.v,s.sp)=seq(s.v,1,s.sp'+1)=seq(s.v,1,s.sp')~s.v[s,sp]= seq(s.v',1s.sp')~x=s'~x