1. Dynamic and static semantics for a small language (hard)

Static Semantics

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.

functions

  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:

• Required initial values:

All declarations must be declared with initial values. This is the simplest solution. The static semantics checks the consistency of both types. In the dynamic semantics neither types nor uninitiated values have to be considered.
• Default initialization:

In this solution the static semantics checks the types of initiated variables. In the dynamic semantics the appropriate default initial values have to be set for variables which are not initialized explicitly. Hence the dynamic semantics has to take type information into account.
• Consideration of missing values:

This is the most complicated solution. Again the static semantics checks both types in the declarations. However, the dynamic semantics has to consider possible uninitiated variables in every construct containing expressions. It would be possible to extend the logic to a three valued logic containing the value undefined, e.g. the expression true <AND> undefined could then be evaluated to true.
• Generating runtime errors:

The dynamic semantics generates runtime errors, if uninitiated variables are used in expressions.

  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
    end;

  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>)
    end;

  wf_Variable : Variable * StatEnv -> bool * [Type]
  wf_Variable(mk_Variable(id), senv) ==
    if id in set dom senv then
      mk_(true, senv(id))
    else
      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>,
             <IntType>),
       <Lt>, <Gt>, <Eq> ->
         mk_(wf_lhs and wf_rhs and tp_lhs = <IntType> and tp_rhs = <IntType>,
             <BoolType>),
       <And>, <Or> ->
         mk_(wf_lhs and wf_rhs and tp_lhs = <BoolType> and tp_rhs = <BoolType>,
             <BoolType>),
       others -> mk_(false, nil)
       end;

Dynamic  Semantics

Since the decision has been made, to instantiate all variables the value of the dynamic environment is not optional:

types

  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.

functions

  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)
    end
  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))
    end
  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:

• Integer-expression:

The assignment is evaluated once when the loop is entered. The expression could either be evaluated once at the beginning or at each repetition. The loop is finished if the loop-variable is greater than the value:

After each execution of the loop's body the loop-variable is increased.
• Boolean expression and running execution of the assignment:

The evaluation of the expression and the assignment is performed continuously:

The loop is executed until the Boolean expression evaluates to 'true'.
• Boolean expression with evaluating the assignment once:

The assignment is evaluated once at the beginning of the loop. The Boolean expression is again evaluated continuously. Here the loop variable must be increased (changed) inside the loop.

• Is it allowed to use the loop-variable inside the stop-expression?
• Is it allowed to change the loop-variable inside the body?
• Is it allowed to change the variables, which are used in the stop-expression, inside the body?

  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_BoolVal(-),
      mk_IntVal(-)         -> ex,
      mk_Variable(id)      -> denv(id),
      mk_BinaryExpr(-,-,-) -> EvalBinaryExpr(ex, denv)
    end
  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)
    end
  pre op = <Div> => EvalExpr(rhs, denv).val <> 0;

2. 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

Flowgraph::
 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;

functions

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);
 

values

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