program VerifyingSpecification;
  (* This is an example showing how to proceed in order to
     make a dynamic verification of an implementation of 
     a specification of a data structure.

     In our example we shall give three components:
     1) a specification of stacks,
     2) a class that ensures the dynamic verification of
        correctness of an implementing module,
     3) an implementation of stacks as a class which inherits
        from the previous class.
  *)
      (* Nowy problem powstaje:
           jak rozpl\ata'c wzajemne odwo/lania operacji wymienionych
           w specyfikacji?

           Zrobilem tak:   kazda operacja posiada dwie wersje np. Push i Ppush
                  1sza wersja jest otoczona pre- i post- conditions
                  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

          Nie jestem tym zachwycony.
          Po co dwa razy pisac te sama procedure??

       *)

  (* --------------- specification of STACKS ----------------------------

        sorts Elem, Stack, Boolean;

        predicates
           empty: Stack {SYMBOL 174 \f "Symbol"} Boolean
           eq:    Elem {SYMBOL 180 \f "Symbol"} Elem {SYMBOL 174 \f "Symbol"} Boolean
           equal: Stack {SYMBOL 180 \f "Symbol"} Stack {SYMBOL 174 \f "Symbol"} Boolean

       operations
           push:  Elem {SYMBOL 180 \f "Symbol"} Stack  {SYMBOL 174 \f "Symbol"} Stack
           pop:   Stack  {SYMBOL 174 \f "Symbol"} Stack
           top:   Stack  {SYMBOL 174 \f "Symbol"} Elem

       axioms
          for every e in Elem, for every s in Stack

      A1)  not empty(push(e,s))
      A2)  eq(e, top(push(e,s)))
      A3)  equal(s, pop(push(e,s)))
      A4)  not empty(s) ==> equal(s, push(top(s), pop(s)))
      A5)  while not empty(s) do s := pop(s) od true
      A6)  equal(s, s') <=> begin result := true; s1 := s; s2 := s';
                             while not empty(s1) and not empty(s2) and result
                                 do
                                   result := eq(top(s1), top(s2));
                                   s1 := pop(s1);
                                   s2 := pop(s2);
                                 od  (result and empty(s1) and empty(s2))


 end of specification STACKS
 *)


(* -------------------------- Checking STACKS --------------------------- *)

 unit STACKS_CHECKING: class;

    unit Elem: class;
    end Elem;

    unit Stack: class;
    end Stack;

    unit check_Push: class(e: Elem, s: Stack);
       var res, old_s: Stack;
    begin
       (* if full(s) then raise ERR_Full fi; *)
       old_s := s;
       inner;
       if empty(res) then raise ERR_Axiom1 fi;
       if not eq(e, Ttop(res)) then raise ERR_Axiom2 fi;
       if not equal(old_s, Ppop(res)) then raise ERR_Axiom3 fi;
    end check_Push;

    unit virtual Push: check_Push function: Stack;
    end Push;

    unit virtual Ppop: function(s:Stack): Stack;
    end Ppop;

    unit virtual Pop: check_Pop function: Stack;
    end Pop;

    unit virtual Ttop: function(s: Stack): Elem;
    end Ttop;

    unit check_Pop: class(s: Stack);
       var res: Stack, aux: Elem;
    begin
       if empty(s) then raise ERR_Empty fi;
       inner;
       aux := Ttop(s);    
       if not equal(s, Ppush(aux,res)) then raise ERR_Axiom4 fi;    
    end check_Pop;
    
    unit virtual Ppush: function(e: Elem, s: Stack): Stack; 
    end Ppush;

    unit virtual Top: check_Top function: Elem;
    end Top;

    unit check_Top: class(s: Stack);
       var res: Elem, aux: Stack;
    begin
       if empty(s) then raise ERR_Empty fi;
       inner;
       aux := Pop(s);
       if not equal(s, Ppush(res,aux)) then raise ERR_Axiom4 fi;  
    end check_Top;
    
    unit virtual Empty: function(s: Stack): Boolean;
    end Empty;

    unit virtual Eq: function(e1, e2: Elem): Boolean;
    end Eq;

    unit check_Equal: class(s1, s2: Stack);
      (* what to check and how? *)

    end check_Equal;

    unit virtual Equal: function(s1, s2: Stack): Boolean;
    
    end Equal;

    signal ERR_Full, ERR_Empty, ERR_Axiom1, ERR_Axiom2, ERR_Axiom3,
           ERR_Axiom4;

 end STACKS_CHECKING;



 (* ----------------------- STACKS generic ------------------------------- *)

 unit STACKS_Generic: STACKS_Checking class;
    hidden link;

    unit link: class(e: Elem);
       var next: link;
    end link;

    unit Stackl: Stack class;
       var top: link
    end Stackl;

    unit virtual Push: check_Push function: Stackl;
       var aux: link;
    begin
       aux := new Link(e);
       aux.next := s qua Stackl.top;
       result := new Stackl;
       result.top := aux;
       res := result
    end Push;

    unit virtual Ppush:  function(e: Elem, s: Stackl): Stackl;
       var aux: link;
    begin
       aux := new Link(e);
       aux.next := s.top;
       result := new Stackl;
       result.top := aux;
    end Ppush;

    unit virtual Pop: check_Pop function: Stackl;
    begin
       result := new Stackl;
       result.top := s qua Stackl.top.next;
       res := result;
    end Pop;

    unit virtual Ppop: function(s: Stackl): Stackl;
    begin
       result := new Stackl;
       result.top := s.top.next;
    end Ppop;

    unit virtual Top: check_Top function: Elem;
    begin
      result := s qua Stackl.top.e;  
      res := result
    end Top;

    unit virtual Ttop: function(s: Stackl): Elem;
    begin
       result := s.top.e
    end Ttop;

    unit virtual Empty: function(s: Stackl): Boolean;
    begin
      result := s.top = none
    end empty;
    
    unit virtual Eq: function(e1, e2: Elem): Boolean;
    end Eq;
    
    unit virtual Equal: function(s1, s2: Stackl): Boolean;
       var s3, s4: Stack;
    begin 
       result := true; s3 := s1; s4 := s2;
       while not empty(s3) and not empty(s4) and result
       do
         result := eq(Ttop(s3), Ttop(s4));
         s3 := Ppop(s3);
         s4 := Ppop(s4);
       od;  
       result := (result and empty(s3) and empty(s4))
    end Equal;



 end STACKS_Generic;



(* -------------------------  MAIN  ---------------------------------- *)

begin
   pref STACKS_Generic block

      unit mElem: Elem class(i:integer);
      end mElem;

      unit virtual Eq: function(e1,e2: mElem): Boolean;
      begin
         result := e1.i = e2.i
      end Eq;

      var e1, e2: mElem,
          i:      integer,
          s1, s2: Stackl;

      handlers
         when ERR_Empty:   writeln("stack is empty");
         when ERR_Full:    writeln("stack is full");
         when ERR_Axiom1:  writeln("Axiom1");
         when ERR_Axiom2:  writeln("Axiom2");
         when ERR_Axiom3:  writeln("Axiom3");
         when ERR_Axiom4:  writeln("Axiom4");
      end handlers;

   begin
      writeln("program testing stacks and its verification environment");
      s1 := new Stackl;
      writeln("give an integer, ZERO ends");
      do
        readln(i);
        e1 := new mElem(i);
        s1 := push(e1, s1);
        if i=0 then exit fi;
      od;
      s2 := s1;
      do
         if empty(s2)
         then 
            exit
         else
            e2 := top(s2);
            s2 := pop(s2);
            writeln(e2.i)
         fi
      od;
   end (* prefixed block *)
end (* of program *)