Simple Stack (Bmethod) - Stack B - Simple Stack (Bmethod)

From LiteratePrograms
(Redirected from Stack B)
Jump to: navigation, search

This program is under development.
Please help to debug it. When debugging
is complete, remove the {{develop}} tag.

A simple stack (LIFO)

First try - Stack B - Simple Stack (Bmethod)

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
Retrieved from "https://www.literateprograms.org/Simple_Stack_%28Bmethod%29"
Views