From LiteratePrograms

A simple stack (LIFO)

First try

An abstract component, called "MACHINE" (B terminology)

Name of the component and "profile" (i.e parameter, here the size of the stack)

<<MACHINE>>=
MACHINE
        stack(stack_size)
CONSTRAINTS
        stack_size : NAT & stack_size >= 1 & stack_size <= MAXINT

Few definitions that can be seen as expandable macros

<<DEFINITIONS>>=
DEFINITIONS
        empty == (stack_top = 0)
;       full  == (stack_top >= stack_size)
CONCRETE_VARIABLES
        the_stack, stack_top
INVARIANT
        the_stack : (1..stack_size)-->NAT &
        stack_top : NAT &
        stack_top >= 0 &
        stack_top <= stack_size
INITIALISATION
        the_stack :: (1..stack_size) --> NAT || stack_top := 0
OPERATIONS
/* store == push ; remove == pop ; read = top */
store(value) = PRE      not(full)
                      & value : NAT
               THEN
                        stack_top := stack_top + 1
                     || the_stack(stack_top + 1) := value
               END;
remove =   PRE not (empty)
        THEN
          stack_top := stack_top -1
        END;
top <-- read = PRE not (empty)
                 THEN
                     top := the_stack(stack_top)
                 END
END /* OF MACHINE */

<<stack.mch>>=
MACHINE
DEFINITIONS

Download code