MACHINE Counter

/* B specification of a simple counter 
   Michael Butler 16/11/06  */

CONSTANTS  maximum

PROPERTIES maximum : NATURAL

VARIABLES ctr

INVARIANT  ctr : NATURAL  &  ctr <= maximum

INITIALISATION  ctr := 0
    
OPERATIONS

inc =  PRE ctr <= maximum THEN ctr := ctr+1 END;

dec =  PRE ctr > 0 THEN ctr := ctr-1 END;

val <-- display =  val:=ctr

END