Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Modelling Systems: Answers to Additional General Exercises

Dynamic and static semantics for a small language (hard)

Static Semantics

In order to check, if a program is well-formed, a static environment which maps identifiers to types has to be introduced. types

  StatEnv = map Identifier to Type; 

Using the static environment, a top-down definition of well-formed program constructs can be given. In the following definitions the prefix wf_ stands for well-formed.


  wf_Program : Program -> bool 
  wf_Program(mk_Program(decls, stmt)) == 
    wf_Declarations(decls) and wf_Stmt(stmt, get_Declarations(decls)); 

The incomplete informal description of the declarations raises several questions, which force to make design decisions. A declaration with an initial value contains two type informations, one in the type and one in the value. The two types must be the same. An open question is, what happens with uninitialized variables when they are evaluated inside an expression without having a value associated. This problem concerns both the static and dynamic semantics. If the value is not checked in the static semantics, the dynamic semantics has to take over this task. The following solutions are possible:

In this specification the second solution will be chosen, where all variables without initiations are initiated with default values.

  wf_Declarations : seq of Declaration -> bool 
  wf_Declarations(decls) == 
    (forall i1, i2 in set inds decls & 
      i1 <> i2 => decls(i1).id <> decls(i2).id) and 
    (forall i in set inds decls & 
      decls(i).val <> nil => 
      ((is_BoolVal(decls(i).val) and decls(i).tp = <BoolType>) or 
       (is_IntVal(decls(i).val) and decls(i).tp = <IntType>))); 

  get_Declarations : seq of Declaration -> StatEnv 
  get_Declarations(decls) == 
    {id |-> tp | mk_Declaration(id, tp, -) in set elems decls}; 

The specification of the static semantics of statements is made by a simple case distinction.

  wf_Stmt : Stmt * StatEnv -> bool 
  wf_Stmt(stmt, senv) == 
    cases true : 
      (is_BlockStmt(stmt))  -> wf_BlockStmt(stmt, senv), 
      (is_AssignStmt(stmt)) -> let mk_(wf_ass, -) = wf_AssignStmt(stmt, senv) 
                               in wf_ass, 
      (is_CondStmt(stmt))   -> wf_CondStmt(stmt, senv), 
      (is_ForStmt(stmt))    -> wf_ForStmt(stmt, senv), 
      (is_RepeatStmt(stmt)) -> wf_RepeatStmt(stmt, senv), 
      others                -> false 

  wf_BlockStmt : BlockStmt * StatEnv -> bool 
  wf_BlockStmt(mk_BlockStmt(decls, stmts), senv) == 
    wf_Declarations(decls) and wf_Stmts(stmts, senv ++ get_Declarations(decls)); 

  wf_Stmts : seq of Stmt * StatEnv -> bool 
  wf_Stmts(stmts, senv) == 
    forall stmt in set elems stmts & wf_Stmt(stmt, senv); 

The types of the left-hand and right-hand side of an assignment must be the same. In addition the type of the assignment which is needed in the context of the for-loop is returned.

  wf_AssignStmt : AssignStmt * StatEnv -> bool * [Type] 
  wf_AssignStmt(mk_AssignStmt(lhs, rhs), senv) == 
    let mk_(wf_var, tp_var) = wf_Variable(lhs, senv), 
        mk_(wf_ex, tp_ex) = wf_Expr(rhs, senv) 
    in mk_(wf_ex and wf_var and tp_var = tp_ex, tp_var); 

In the conditional statement and the repeat-loop a boolean expression is required:

  wf_CondStmt : CondStmt * StatEnv -> bool 
  wf_CondStmt(mk_CondStmt(guard, thenst, elsest), senv) == 
    let mk_(wf_ex, tp_ex) = wf_Expr(guard, senv) 
    in wf_ex and tp_ex = <BoolType> and 
       wf_Stmt(thenst, senv) and wf_Stmt(elsest, senv); 

  wf_RepeatStmt : RepeatStmt * StatEnv -> bool 
  wf_RepeatStmt(mk_RepeatStmt(repeat, until), senv) == 
    let mk_(wf_ex, tp_ex) = wf_Expr(until, senv) 
    in wf_ex and tp_ex = <BoolType> and wf_Stmt(repeat, senv); 

The for-loop is underspecified and raises the question, which kind of loop is really intended. It is not clear if the stop expression should be of type Integer or Bool, which leads to two different loop concepts. For a detailed discussion on the possibilities to interpret the semantics of the for-loop see below. For the static semantics the most obvious design decision has been made that the stop-expression should be of type Integer.

  wf_ForStmt : ForStmt * StatEnv -> bool 
  wf_ForStmt(mk_ForStmt(start, stop, stmt), senv) == 
    let mk_(wf_ass, tp_ass) = wf_AssignStmt(start, senv), 
        mk_(wf_ex, tp_ex) = wf_Expr(stop, senv) 
    in wf_ass and wf_ex and tp_ass = <IntType> and tp_ex = <IntType> and 
       wf_Stmt(stmt, senv); 

Handling expressions and variables, it is necessary to return the type in addition to the well-formedness predicate.

  wf_Expr : Expr * StatEnv -> bool * [Type] 
  wf_Expr(ex, senv) == 
    cases true : 
      (is_BoolVal(ex))    -> mk_(true, <BoolType>), 
      (is_IntVal(ex))     -> mk_(true, <IntType>), 
      (is_Variable(ex))   -> wf_Variable(ex, senv), 
      (is_BinaryExpr(ex)) -> wf_BinaryExpr(ex, senv), 
      others              -> mk_(false, <IntType>) 

  wf_Variable : Variable * StatEnv -> bool * [Type] 
  wf_Variable(mk_Variable(id), senv) == 
    if id in set dom senv then 
      mk_(true, senv(id)) 
      mk_(false, nil); 

It is not explicitly stated if the equality operator should also be defined for Boolean values. For simplicity the decision is made to define equality only for Integers.

  wf_BinaryExpr : BinaryExpr * StatEnv -> bool * [Type] 
  wf_BinaryExpr(mk_BinaryExpr(lhs, op, rhs), senv) == 
    let mk_(wf_lhs, tp_lhs) = wf_Expr(lhs, senv), 
        mk_(wf_rhs, tp_rhs) = wf_Expr(rhs, senv) 
    in cases op : 
       <Add>, <Sub>, <Div>, <Mul> -> 
         mk_(wf_lhs and wf_rhs and tp_lhs = <IntType> and tp_rhs = <IntType>, 
       <Lt>, <Gt>, <Eq> -> 
         mk_(wf_lhs and wf_rhs and tp_lhs = <IntType> and tp_rhs = <IntType>, 
       <And>, <Or> -> 
         mk_(wf_lhs and wf_rhs and tp_lhs = <BoolType> and tp_rhs = <BoolType>, 
       others -> mk_(false, nil) 

Dynamic Semantics

In order to define the dynamic semantics of a program the dynamic environment is defined. For this simple language it is sufficient to model it as a mapping from identifiers to values. Thus the storage is not taken into account. Since the decision has been made, to instantiate all variables the value of the dynamic environment is not optional:


  DynEnv = map Identifier to Value; 

As in the definition of the static semantics, a top-down approach is used. The result of the dynamic semantics function is the global dynamic environment consisting of the global variables. The pre-condition of the dynamic semantics function !EvalProgram is the well-formedness of the program and a second condition which concerns the division by zero and will be explained later on.


  EvalProgram : Program -> DynEnv 
  EvalProgram(mk_Program(decls, stmt)) == 
    EvalStmt(stmt, EvalDeclarations(decls)) 
  pre wf_Program(mk_Program(decls, stmt)) and 
      pre_EvalStmt(stmt, EvalDeclarations(decls)); 
Evaluating uninitiated variable declarations, a proper default value is assigned: false for Boolean values and 0 for Integer values.
  EvalDeclarations : seq of Declaration -> DynEnv 
  EvalDeclarations(decls) == 
    {id |-> if val <> nil 
            then val 
            elseif tp = <BoolType> 
            then mk_BoolVal(false) 
            else mk_IntVal(0) 
    | mk_Declaration(id, tp, val) in set elems decls}; 

The evaluation of the statements is rather simple to specify. Only for the block statement the scoping rules have to be considered: The statements in the block are evaluated in the global environment overridden by the local environment. The returning environment contains the updated global variables.

  EvalStmt : Stmt * DynEnv -> DynEnv 
  EvalStmt(stmt, denv) == 
    cases true : 
      (is_BlockStmt(stmt))  -> EvalBlockStmt(stmt, denv), 
      (is_AssignStmt(stmt)) -> EvalAssignStmt(stmt, denv), 
      (is_CondStmt(stmt))   -> EvalCondStmt(stmt, denv), 
      (is_ForStmt(stmt))    -> EvalForStmt(stmt, denv), 
      (is_RepeatStmt(stmt)) -> EvalRepeatStmt(stmt, denv) 
  pre (is_BlockStmt(stmt)   => pre_EvalBlockStmt(stmt, denv)) and 
      (is_AssignStmt(stmt)  => pre_EvalAssignStmt(stmt, denv)) and 
      (is_CondStmt(stmt)    => pre_EvalCondStmt(stmt, denv)) and 
      (is_ForStmt(stmt)     => pre_EvalForStmt(stmt, denv)) and 
      (is_RepeatStmt(stmt)  => pre_EvalRepeatStmt(stmt, denv)); 

  EvalBlockStmt : BlockStmt * DynEnv -> DynEnv 
  EvalBlockStmt(mk_BlockStmt(decls, stmts), denv) == 
    let ldenv = EvalDeclarations(decls) in 
      let denv' = EvalStmts(stmts, denv ++ ldenv) in 
        denv ++ dom ldenv <-: denv' 
  pre let ldenv = EvalDeclarations(decls) 
      in pre_EvalStmts(stmts, denv ++ ldenv); 

  EvalStmts : seq of Stmt * DynEnv -> DynEnv 
  EvalStmts(stmts, denv) == 
    cases stmts : 
      [] -> denv, 
      others -> EvalStmts(tl stmts, EvalStmt(hd stmts, denv)) 
  pre stmts <> [] => pre_EvalStmt(hd stmts, denv); 

  EvalAssignStmt : AssignStmt * DynEnv -> DynEnv 
  EvalAssignStmt(mk_AssignStmt(lhs, rhs), denv) == 
    denv ++ {lhs.id |-> EvalExpr(rhs, denv)} 
  pre pre_EvalExpr(rhs, denv); 

  EvalCondStmt : CondStmt * DynEnv -> DynEnv 
  EvalCondStmt(mk_CondStmt(guard, thenst, elsest), denv) == 
    if EvalExpr(guard, denv).val 
    then EvalStmt(thenst, denv) 
    else EvalStmt(elsest, denv) 
  pre pre_EvalExpr(guard, denv) and 
      if EvalExpr(guard, denv).val 
      then pre_EvalStmt(thenst, denv) 
      else pre_EvalStmt(elsest, denv); 

  EvalRepeatStmt : RepeatStmt * DynEnv -> DynEnv 
  EvalRepeatStmt(mk_RepeatStmt(repeat, until), denv) == 
    let denv' = EvalStmt(repeat, denv) in 
    if EvalExpr(until, denv').val 
      then denv' 
      else EvalRepeatStmt(mk_RepeatStmt(repeat, until), denv') 
  pre pre_EvalStmt(repeat, denv) and 
      pre_EvalExpr(until, EvalStmt(repeat, denv)); 

As indicated above, the dynamic semantics of the for-loop is underspecified. The informal description allows the interpretation of the stop-expression to be of type integer or Boolean, which leads to two different loop concepts and raises further questions about the dynamic semantics of for-loops:

	 for i := 1 to 5 do ... 
	i := 1; 
     for (i := i + 1, i = 5) do ... 

Unwanted effects could arise, if the expression is computed continuously and if the loop-variable is allowed inside the expression or the variables inside the expression are allowed inside the body. Therefore, the design decision is made that the stop-expression is only evaluated once. Furthermore, no restrictions in the usage of variables are made.

 EvalForStmt : ForStmt * DynEnv -> DynEnv 
  EvalForStmt(mk_ForStmt(start, stop, stmt), denv) == 
    let denv' = EvalAssignStmt(start, denv) in 
    EvalForLoop(start.lhs, EvalExpr(stop, denv'), stmt, denv') 
  pre pre_EvalAssignStmt(start, denv) and 
      pre_EvalExpr(stop, EvalAssignStmt(start, denv)); 

  EvalForLoop : Variable * Value * Stmt * DynEnv -> DynEnv 
  EvalForLoop(mk_Variable(id), val, stmt, denv) == 
    if denv(id).val <= val.val 
      then let denv' = EvalStmt(stmt, denv) 
           in EvalForLoop(mk_Variable(id), val, stmt, 
                          denv' ++ {id |-> mk_IntVal(denv'(id).val + 1)}) 
      else denv 
  pre pre_EvalStmt(stmt, denv); 

The evaluation of binary expressions is straightforward. An exception is the binary expression where the problem of division by zero may occur. A pre-condition states that the right-hand side must not be zero. This pre-condition has to be added to every function on a higher level in the definition hierarchy.

  EvalExpr : Expr * DynEnv -> Value 
  EvalExpr(ex, denv) == 
    cases ex : 
      mk_IntVal(-)         -> ex, 
      mk_Variable(id)      -> denv(id), 
      mk_BinaryExpr(-,-,-) -> EvalBinaryExpr(ex, denv) 
  pre is_BinaryExpr(ex) => pre_EvalBinaryExpr(ex, denv); 

  EvalBinaryExpr : BinaryExpr * DynEnv -> Value 
  EvalBinaryExpr(mk_BinaryExpr(lhs, op, rhs), denv) == 
    let v1 = EvalExpr(lhs, denv).val, 
        v2 = EvalExpr(rhs, denv).val 
    in cases op : 
       <Add> -> mk_IntVal(v1 + v2), 
       <Sub> -> mk_IntVal(v1 - v2), 
       <Div> -> mk_IntVal(v1 div v2), 
       <Mul> -> mk_IntVal(v1 * v2), 
       <Lt> ->  mk_BoolVal(v1 < v2), 
       <Gt> ->  mk_BoolVal(v1 > v2), 
       <Eq> ->  mk_BoolVal(v1 = v2), 
       <And> -> mk_BoolVal(v1 and v2), 
       <Or> ->  mk_BoolVal(v1 or v2) 
  pre op = <Div> => EvalExpr(rhs, denv).val <> 0; 

Program Flowgraphs (hard)

Node = nat1; 

Nodes = set of Node; -- any subset of Node 

GraphNodes = set of Node 
inv N == forall i in set {1,...,card N} & i in set N; 
-- sets of form {1,...,K}, for arbitrary K 

Arc = Node * Node; 
Arcs = set of Arc; -- family of binary relations on Node 

 N: GraphNodes 
 A: Arcs 
 S: Node 
 E: Node 
inv mk_Flowgraph(N,A,S,E) == 
 (card N >1) and 
 (S in set N) and 
 (E in set N) and 
 let G=mk_Flowgraph(N,A,S,E) in 
 (Successors(G,E) = {}) and -- exit has no successors 
 (Predecessors(G,S) = {}) and  -- entry has no predecessor 
 let All = {mk_(x,y)| x,y in set N} in -- all possible arcs on N 
 (A subset All); -- arcs in A come from N * N 

Path = seq of Node; 


Successors: Flowgraph * Node -> Nodes 
Successors(mk_Flowgraph(N,A,S,E),n) == 
  {x| x in set N & mk_(n,x) in set A} 
pre n in set N; 

Predecessors: Flowgraph * Node -> Nodes 
Predecessors(G,n) == {x| x in set G.N & mk_(x,n) in set G.A} 
pre n in set G.N; 

-- NOTE: Th eabove definitions are OK without dynamic invariant checking 
-- However, if you turn the latter on, infinitie recursion will occur, 
-- since the functions Predecessors and Successors will try again 
-- to check the invariant. Solution? 

-- Redefine the signature of Predec- and Succs-essors to avoid explicitly 
-- referring to type Flowgraph, e.g. 
-- Successors: Arcs * Nodes * Node -> Nodes 
-- called as Successors (A,N,N) 

IsPathInGraph: Flowgraph * Path -> bool 
IsPathInGraph(mk_Flowgraph(N,A,S,E), p) == 
  forall i in set {1,...,len p -1} & mk_(i,i+1) in set A; 

a: Node * Node -> Arc 
-- returns arc (i,j), to build arc values easier 
a(i,j) == mk_(i,j); 


V: GraphNodes = {1,...,10}; -- one set for all flow graphs 

-- various sets of arcs for different kinds of graphs 
AllArcs: Arcs ={mk_(x,y)| x,y in set V}; -- all potential arcs 
A0: Arcs = {}; --empty graph 
A1: Arcs = {a(i,j)| i, j in set V & j=i+1};  -- linear graph 
A2: Arcs = A1 union {a(4,6)}; -- one IF at 4 
A3: Arcs = A2 union {a(8,3),a(3,9)}; -- IF and loop at3 
A4: Arcs = A3 union {a(9,2)}; -- nested loops 

g1v: Flowgraph= mk_Flowgraph(V,A0,1,10); --valid empty graph 
-- g1i: Flowgraph= mk_Flowgraph(V,A0,1,20); -- invalid empty graph, 
-- initialization error IF dynamic invariant checking on 

g2v: Flowgraph = mk_Flowgraph(V,A1,1,10); -- valid linear 
--g2i: Flowgraph = mk_Flowgraph(V,A1,1,20); --invalid linear