package ASM_Int_Stack2
   --# own State;
   --# initializes State;
is
   function Full return Boolean;
   --# global in State;

   procedure Push(X: in Integer);
   --# global in out State;
   --# derives State from X, State;

end ASM_Int_Stack2;