OoasTools

types

  SmallInt = int [0..3];

  Stack = autocons system

  |[

  var

        my_stack : list [10] of SmallInt = [0]

  actions

        obs top (a : SmallInt) = requires (a = hd my_stack) :

                skip

                end ;

        obs pop = requires (len my_stack > 0) :

                my_stack := tl my_stack

                end;

        obs push (a : SmallInt) = requires len my_stack < 10 :

                my_stack := [a] ^ my_stack

                end

  do

        var A : SmallInt : push(A) []  pop() [] var B : SmallInt : top(B)

  od

  ]|

system

  Stack