The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile


Author: Jim Woodcock

This simple bit register example has been provided in VDM by a student called Andreas Mueller from Austria. It has been translated to CML by Jim Woodcock and used for testing the Symphony tool.

This example defines the main operators you can conduct on a very simple calculator where you can have registers you can store and load values to and from, and then add and subtract. Note that it only handles bytes up to 255 so it is possible to see the effect of overflows and underflows.

Just like for the Stack example the RegisterProc process can be debugged and it is possible to load values into the register and try to add and subtract them from each other. Here the natural behaviour of the bit register (including underflow and overflow scenarios) can be exercised. Note that you also can set breakpoints and inspect the different variables when the simulation is stopped at such breakpoints.

In the current version there are a number of proof obligations generated that you will not be able to discharge. Please update the argument types for some of the operations so this can be improved.


    public Byte = int
    inv n == (n >= 0) and (n <= 255)

   oflow : Byte * Byte -> bool
   oflow(i,j) == i+j > 255

   uflow : Byte * Byte -> bool
   uflow(i,j) == i-j < 0

   init, overflow, underflow
   read, load, add, sub : Byte

  I = {| init, overflow, underflow, read, load, add, sub |}

process RegisterProc = 

  reg : Byte    

   INIT : () ==> ()
   INIT() == reg := 0

   LOAD : int ==> ()
   LOAD(i) == reg := i

   READ: () ==>  int
   READ() == return reg

   ADD: int ==> ()
   ADD(i) == reg := reg + i
   pre not oflow(reg, i)
   post reg = reg~ + i

   SUB: int ==> ()
   SUB(i) == reg := reg - i
   //frame wr reg : int
   pre not uflow(reg,i)
   post reg = reg~ - i


   REG = 
     (load?i -> LOAD(i) ; REG)
     (dcl j: int @ j := READ(); read!j -> REG)
     (add?i -> ( ([oflow(reg,i)] & overflow -> INIT(); REG)
                 ([not oflow(reg,i)] & ADD(i);REG)))
     (sub?i -> ( ([uflow(reg,i)] & underflow -> INIT(); REG)
                 ([not uflow(reg,i)] & SUB(i); REG)))
     init -> INIT(); REG