examples/pataud/verspec.log

   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
   5 \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
  12   *)\r
  13       (* Nowy problem powstaje:\r
  14            jak rozpl\ata'c wzajemne odwo/lania operacji wymienionych\r
  15            w specyfikacji?\r
  16 \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
  20 \r
  21           Nie jestem tym zachwycony.\r
  22           Po co dwa razy pisac te sama procedure??\r
  23 \r
  24        *)\r
  25 \r
  26   (* --------------- specification of STACKS ----------------------------\r
  27 \r
  28         sorts Elem, Stack, Boolean;\r
  29 \r
  30         predicates\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
  34 \r
  35        operations\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
  39 \r
  40        axioms\r
  41           for every e in Elem, for every s in Stack\r
  42 \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
  50                                  do\r
  51                                    result := eq(top(s1), top(s2));\r
  52                                    s1 := pop(s1);\r
  53                                    s2 := pop(s2);\r
  54                                  od  (result and empty(s1) and empty(s2))\r
  55 \r
  56 \r
  57  end of specification STACKS\r
  58  *)\r
  59 \r
  60 \r
  61 (* -------------------------- Checking STACKS --------------------------- *)\r
  62 \r
  63  unit STACKS_CHECKING: class;\r
  64 \r
  65     unit Elem: class;\r
  66     end Elem;\r
  67 \r
  68     unit Stack: class;\r
  69     end Stack;\r
  70 \r
  71     unit check_Push: class(e: Elem, s: Stack);\r
  72        var res, old_s: Stack;\r
  73     begin\r
  74        (* if full(s) then raise ERR_Full fi; *)\r
  75        old_s := s;\r
  76        inner;\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
  80     end check_Push;\r
  81 \r
  82     unit virtual Push: check_Push function: Stack;\r
  83     end Push;\r
  84 \r
  85     unit virtual Ppop: function(s:Stack): Stack;\r
  86     end Ppop;\r
  87 \r
  88     unit virtual Pop: check_Pop function: Stack;\r
  89     end Pop;\r
  90 \r
  91     unit virtual Ttop: function(s: Stack): Elem;\r
  92     end Ttop;\r
  93 \r
  94     unit check_Pop: class(s: Stack);\r
  95        var res: Stack, aux: Elem;\r
  96     begin\r
  97        if empty(s) then raise ERR_Empty fi;\r
  98        inner;\r
  99        aux := Ttop(s);    \r
 100        if not equal(s, Ppush(aux,res)) then raise ERR_Axiom4 fi;    \r
 101     end check_Pop;\r
 102     \r
 103     unit virtual Ppush: function(e: Elem, s: Stack): Stack; \r
 104     end Ppush;\r
 105 \r
 106     unit virtual Top: check_Top function: Elem;\r
 107     end Top;\r
 108 \r
 109     unit check_Top: class(s: Stack);\r
 110        var res: Elem, aux: Stack;\r
 111     begin\r
 112        if empty(s) then raise ERR_Empty fi;\r
 113        inner;\r
 114        aux := Pop(s);\r
 115        if not equal(s, Ppush(res,aux)) then raise ERR_Axiom4 fi;  \r
 116     end check_Top;\r
 117     \r
 118     unit virtual Empty: function(s: Stack): Boolean;\r
 119     end Empty;\r
 120 \r
 121     unit virtual Eq: function(e1, e2: Elem): Boolean;\r
 122     end Eq;\r
 123 \r
 124     unit check_Equal: class(s1, s2: Stack);\r
 125       (* what to check and how? *)\r
 126 \r
 127     end check_Equal;\r
 128 \r
 129     unit virtual Equal: function(s1, s2: Stack): Boolean;\r
 130     \r
 131     end Equal;\r
 132 \r
 133     signal ERR_Full, ERR_Empty, ERR_Axiom1, ERR_Axiom2, ERR_Axiom3,\r
 134            ERR_Axiom4;\r
 135 \r
 136  end STACKS_CHECKING;\r
 137 \r
 138 \r
 139 \r
 140  (* ----------------------- STACKS generic ------------------------------- *)\r
 141 \r
 142  unit STACKS_Generic: STACKS_Checking class;\r
 143     hidden link;\r
 144 \r
 145     unit link: class(e: Elem);\r
 146        var next: link;\r
 147     end link;\r
 148 \r
 149     unit Stackl: Stack class;\r
 150        var top: link\r
 151     end Stackl;\r
 152 \r
 153     unit virtual Push: check_Push function: Stackl;\r
 154        var aux: link;\r
 155     begin\r
 156        aux := new Link(e);\r
 157        aux.next := s qua Stackl.top;\r
 158        result := new Stackl;\r
 159        result.top := aux;\r
 160        res := result\r
 161     end Push;\r
 162 \r
 163     unit virtual Ppush:  function(e: Elem, s: Stackl): Stackl;\r
 164        var aux: link;\r
 165     begin\r
 166        aux := new Link(e);\r
 167        aux.next := s.top;\r
 168        result := new Stackl;\r
 169        result.top := aux;\r
 170     end Ppush;\r
 171 \r
 172     unit virtual Pop: check_Pop function: Stackl;\r
 173     begin\r
 174        result := new Stackl;\r
 175        result.top := s qua Stackl.top.next;\r
 176        res := result;\r
 177     end Pop;\r
 178 \r
 179     unit virtual Ppop: function(s: Stackl): Stackl;\r
 180     begin\r
 181        result := new Stackl;\r
 182        result.top := s.top.next;\r
 183     end Ppop;\r
 184 \r
 185     unit virtual Top: check_Top function: Elem;\r
 186     begin\r
 187       result := s qua Stackl.top.e;  \r
 188       res := result\r
 189     end Top;\r
 190 \r
 191     unit virtual Ttop: function(s: Stackl): Elem;\r
 192     begin\r
 193        result := s.top.e\r
 194     end Ttop;\r
 195 \r
 196     unit virtual Empty: function(s: Stackl): Boolean;\r
 197     begin\r
 198       result := s.top = none\r
 199     end empty;\r
 200     \r
 201     unit virtual Eq: function(e1, e2: Elem): Boolean;\r
 202     end Eq;\r
 203     \r
 204     unit virtual Equal: function(s1, s2: Stackl): Boolean;\r
 205        var s3, s4: Stack;\r
 206     begin \r
 207        result := true; s3 := s1; s4 := s2;\r
 208        while not empty(s3) and not empty(s4) and result\r
 209        do\r
 210          result := eq(Ttop(s3), Ttop(s4));\r
 211          s3 := Ppop(s3);\r
 212          s4 := Ppop(s4);\r
 213        od;  \r
 214        result := (result and empty(s3) and empty(s4))\r
 215     end Equal;\r
 216 \r
 217 \r
 218 \r
 219  end STACKS_Generic;\r
 220 \r
 221 \r
 222 \r
 223 (* -------------------------  MAIN  ---------------------------------- *)\r
 224 \r
 225 begin\r
 226    pref STACKS_Generic block\r
 227 \r
 228       unit mElem: Elem class(i:integer);\r
 229       end mElem;\r
 230 \r
 231       unit virtual Eq: function(e1,e2: mElem): Boolean;\r
 232       begin\r
 233          result := e1.i = e2.i\r
 234       end Eq;\r
 235 \r
 236       var e1, e2: mElem,\r
 237           i:      integer,\r
 238           s1, s2: Stackl;\r
 239 \r
 240       handlers\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
 247       end handlers;\r
 248 \r
 249    begin\r
 250       writeln("program testing stacks and its verification environment");\r
 251       s1 := new Stackl;\r
 252       writeln("give an integer, ZERO ends");\r
 253       do\r
 254         readln(i);\r
 255         e1 := new mElem(i);\r
 256         s1 := push(e1, s1);\r
 257         if i=0 then exit fi;\r
 258       od;\r
 259       s2 := s1;\r
 260       do\r
 261          if empty(s2)\r
 262          then \r
 263             exit\r
 264          else\r
 265             e2 := top(s2);\r
 266             s2 := pop(s2);\r
 267             writeln(e2.i)\r
 268          fi\r
 269       od;\r
 270    end (* prefixed block *)\r
 271 end (* of program *)\r
 272 \r