Author

Purpose and content of the specification

Program     ::=   skip
                | Statement @ Program
Statement   ::=   Assignment
                | Conditional
                | Loop
Assignment  ::= Variable := Expression
Conditional ::= IF Condition THEN Program ELSE Program FI 
Loop        ::= WHILE Condition DO Program OD 
...

The tutorial includes a stepwise development of the specification submitted to this repository. The slides of my tutorial are available at http://www.informatik.uni-bremen.de/~roba/tutorial.ps.

Specifying an interpreter for an imperative programming language was also an exercise for students in a course on Algebraic Specification at the University of Bremen. The students liked this exercise and gave good solutions to it.

Tool Support

With HOL-CASL it is possible to execute simple programs on the specified interpreter, for example the goal

forall n: Nat .
eval(a, execute 
        (    (a:=conv(15)) @
             (b:=conv(9)) @
             WHILE NOT (a==b) 
             DO
               IF  a < b
                 THEN (b:=(b-a)) @ skip 
                 ELSE (a:=(a-b)) @ skip 
               FI @ skip         
             OD  
        @ 
           skip, [] ))
= n

3 = n

The simplifier sets for such computations in HOL-CASL are available on request.

Possible Improvements

• use Nat and FiniteMap (in States) from the Basic Datatypes
• separate specifications of Nat on the syntactic and the semantic level in order to get rid of the operation conv: Nat
• Expression.
• in Nat: relate the operational definition of the total __-__ (x-y = 0 iff y >= x) with the common partial operation and it's non-operational definition
• introduce a syntax for variables

Specification