1 program VerifyingSpecification;
\r
2 (* This is an example showing how to proceed in order to
\r
3 make a dynamic verification of an implementation of
\r
4 a specification of a data structure.
\r
6 In our example we shall give three components:
\r
7 1) a specification of stacks,
\r
8 2) a class that ensures the dynamic verification of
\r
9 correctness of an implementing module,
\r
10 3) an implementation of stacks as a class which inherits
\r
11 from the previous class.
\r
13 (* Nowy problem powstaje:
\r
14 jak rozpl\ata'c wzajemne odwo/lania operacji wymienionych
\r
17 Zrobilem tak: kazda operacja posiada dwie wersje np. Push i Ppush
\r
18 1sza wersja jest otoczona pre- i post- conditions
\r
19 2ga wersja nie zawiera takiego sprawdzania - druga wersja jest uzywana w pre- i post-conditions i wewnatrz equal ktore odwoluje sie do top i pop
\r
21 Nie jestem tym zachwycony.
\r
22 Po co dwa razy pisac te sama procedure??
\r
26 (* --------------- specification of STACKS ----------------------------
\r
28 sorts Elem, Stack, Boolean;
\r
31 empty: Stack {SYMBOL 174 \f "Symbol"} Boolean
\r
32 eq: Elem {SYMBOL 180 \f "Symbol"} Elem {SYMBOL 174 \f "Symbol"} Boolean
\r
33 equal: Stack {SYMBOL 180 \f "Symbol"} Stack {SYMBOL 174 \f "Symbol"} Boolean
\r
36 push: Elem {SYMBOL 180 \f "Symbol"} Stack {SYMBOL 174 \f "Symbol"} Stack
\r
37 pop: Stack {SYMBOL 174 \f "Symbol"} Stack
\r
38 top: Stack {SYMBOL 174 \f "Symbol"} Elem
\r
41 for every e in Elem, for every s in Stack
\r
43 A1) not empty(push(e,s))
\r
44 A2) eq(e, top(push(e,s)))
\r
45 A3) equal(s, pop(push(e,s)))
\r
46 A4) not empty(s) ==> equal(s, push(top(s), pop(s)))
\r
47 A5) while not empty(s) do s := pop(s) od true
\r
48 A6) equal(s, s') <=> begin result := true; s1 := s; s2 := s';
\r
49 while not empty(s1) and not empty(s2) and result
\r
51 result := eq(top(s1), top(s2));
\r
54 od (result and empty(s1) and empty(s2))
\r
57 end of specification STACKS
\r
61 (* -------------------------- Checking STACKS --------------------------- *)
\r
63 unit STACKS_CHECKING: class;
\r
71 unit check_Push: class(e: Elem, s: Stack);
\r
72 var res, old_s: Stack;
\r
74 (* if full(s) then raise ERR_Full fi; *)
\r
77 if empty(res) then raise ERR_Axiom1 fi;
\r
78 if not eq(e, Ttop(res)) then raise ERR_Axiom2 fi;
\r
79 if not equal(old_s, Ppop(res)) then raise ERR_Axiom3 fi;
\r
82 unit virtual Push: check_Push function: Stack;
\r
85 unit virtual Ppop: function(s:Stack): Stack;
\r
88 unit virtual Pop: check_Pop function: Stack;
\r
91 unit virtual Ttop: function(s: Stack): Elem;
\r
94 unit check_Pop: class(s: Stack);
\r
95 var res: Stack, aux: Elem;
\r
97 if empty(s) then raise ERR_Empty fi;
\r
100 if not equal(s, Ppush(aux,res)) then raise ERR_Axiom4 fi;
\r
103 unit virtual Ppush: function(e: Elem, s: Stack): Stack;
\r
106 unit virtual Top: check_Top function: Elem;
\r
109 unit check_Top: class(s: Stack);
\r
110 var res: Elem, aux: Stack;
\r
112 if empty(s) then raise ERR_Empty fi;
\r
115 if not equal(s, Ppush(res,aux)) then raise ERR_Axiom4 fi;
\r
118 unit virtual Empty: function(s: Stack): Boolean;
\r
121 unit virtual Eq: function(e1, e2: Elem): Boolean;
\r
124 unit check_Equal: class(s1, s2: Stack);
\r
125 (* what to check and how? *)
\r
129 unit virtual Equal: function(s1, s2: Stack): Boolean;
\r
133 signal ERR_Full, ERR_Empty, ERR_Axiom1, ERR_Axiom2, ERR_Axiom3,
\r
136 end STACKS_CHECKING;
\r
140 (* ----------------------- STACKS generic ------------------------------- *)
\r
142 unit STACKS_Generic: STACKS_Checking class;
\r
145 unit link: class(e: Elem);
\r
149 unit Stackl: Stack class;
\r
153 unit virtual Push: check_Push function: Stackl;
\r
156 aux := new Link(e);
\r
157 aux.next := s qua Stackl.top;
\r
158 result := new Stackl;
\r
163 unit virtual Ppush: function(e: Elem, s: Stackl): Stackl;
\r
166 aux := new Link(e);
\r
168 result := new Stackl;
\r
172 unit virtual Pop: check_Pop function: Stackl;
\r
174 result := new Stackl;
\r
175 result.top := s qua Stackl.top.next;
\r
179 unit virtual Ppop: function(s: Stackl): Stackl;
\r
181 result := new Stackl;
\r
182 result.top := s.top.next;
\r
185 unit virtual Top: check_Top function: Elem;
\r
187 result := s qua Stackl.top.e;
\r
191 unit virtual Ttop: function(s: Stackl): Elem;
\r
196 unit virtual Empty: function(s: Stackl): Boolean;
\r
198 result := s.top = none
\r
201 unit virtual Eq: function(e1, e2: Elem): Boolean;
\r
204 unit virtual Equal: function(s1, s2: Stackl): Boolean;
\r
207 result := true; s3 := s1; s4 := s2;
\r
208 while not empty(s3) and not empty(s4) and result
\r
210 result := eq(Ttop(s3), Ttop(s4));
\r
214 result := (result and empty(s3) and empty(s4))
\r
219 end STACKS_Generic;
\r
223 (* ------------------------- MAIN ---------------------------------- *)
\r
226 pref STACKS_Generic block
\r
228 unit mElem: Elem class(i:integer);
\r
231 unit virtual Eq: function(e1,e2: mElem): Boolean;
\r
233 result := e1.i = e2.i
\r
241 when ERR_Empty: writeln("stack is empty");
\r
242 when ERR_Full: writeln("stack is full");
\r
243 when ERR_Axiom1: writeln("Axiom1");
\r
244 when ERR_Axiom2: writeln("Axiom2");
\r
245 when ERR_Axiom3: writeln("Axiom3");
\r
246 when ERR_Axiom4: writeln("Axiom4");
\r
250 writeln("program testing stacks and its verification environment");
\r
252 writeln("give an integer, ZERO ends");
\r
255 e1 := new mElem(i);
\r
256 s1 := push(e1, s1);
\r
257 if i=0 then exit fi;
\r
270 end (* prefixed block *)
\r
271 end (* of program *)
\r