Exercise 1 is based on one supplied by Bernhard K. Aichernig and Andreas Kerschbaumer from TU Graz in Austria. Exercise 2 is based on one supplied by Prof. Janusz Laski from Oakland University. The assistance from all of them is gratefully acknowledged.
A VDM-SL specification of the static and dynamic semantics of a typed imperative programming language is to be developed. The abstract syntax and an informal description of the semantics of the language is given. Let us first define what the meaning of static and dynamic semantics is:
The static semantics should define and check the well-formedness of programs in the given language. This includes static type checking, the complete and unambiguous definition of all variables inside program blocks, and scoping.
Below the abstract syntax of the language is given in VDM-SL. In order to keep the language simple, only Integer and Boolean types are defined. A program consists of a declaration part followed by a statement. definitions
types
Program :: decls : seq of Declaration
stmt : Stmt;
A (variable) declaration consists of an identifier, an associated type and an optional initial value.
Declaration :: id : Identifier
tp : Type
val : [Value];
An identifier is a sequence of characters. In our language two types are known, Boolean and Integer. The two types of values in the language are modeled as the corresponding VDM-SL types bool and int.
Identifier = seq1 of char;
Type = <BoolType> | <IntType> ;
Value = BoolVal | IntVal;
BoolVal :: val : bool;
IntVal :: val : int;
Our simple language only knows four kinds of statements: block statements, assignments, a conditional statement, a for-loop and a repeat-loop.
Stmt = BlockStmt | AssignStmt | CondStmt | ForStmt | RepeatStmt;
A block statement consists of local variable declarations and a non-empty sequence of statements.
BlockStmt :: decls : seq of Declaration
stmts : seq1 of Stmt;
The left-hand side of an assignment is a variable, which is simply an identifier. The right-hand side is defined as an expression.
AssignStmt :: lhs : Variable
rhs : Expr;
Variable :: id : Identifier;
An expression could be a binary expression, a value or a variable. A binary expression consists of a left-hand expression, an operator and a right-hand expression.
Expr = BinaryExpr | Value | Variable;
BinaryExpr :: lhs : Expr
op : Operator
rhs : Expr;
The numeric operators of the language are addition, subtraction, Integer-division, and multiplication. The Boolean operators are less-than, greater-then, equality, conjunction, and finally disjunction.
Operator = <Add> | <Sub> | <Div> | <Mul> | <Lt> | <Gt> | <Eq> | <And> | <Or>;
A conditional if-statement consists of a guard predicate, the then- and else-branch.
CondStmt :: guard : Expr
thenst : Stmt
elsest : Stmt;
The for-loop consists of an initial assignment to the loop-variable, followed by an expression, which defines the stop value of the loop-variable, and the statement to be repeated. It is allowed to modify the loop-variable inside the body of the loop.
ForStmt :: start : AssignStmt
stop : Expr
stmt : Stmt;
Finally, the repeat-loop consists of the statement to be repeated and its stop condition.
RepeatStmt :: repeat : Stmt
until : Expr;
For this small programming language you should now define:
wf_Program : Program -> bool
) andEvalProgram : Program -> DynEnv
where DynEnv
is defined to be DynEnv = map
Identifier to Value).The flowgraph is a version of a directed graph that provides a model of the flow of control in a subprogram, i.e. a procedure or function; it is a formal version of a flowchart that can be derived automatically from the subprogram’s source code. The essential components of the flowgraph are nodes, which correspond to instructions in the procedure. An instruction is the smallest (further nondecomposable) executable part of a programming statement. Thus, mathematically, a flowgraph is a quadruple <N,A,S,E> where N is the set of nodes, A is a set of arcs and S and E are, respectively, the Start and Exit node. An arc a in A is a pair (n m), where n,m?N with the meaning “m may be executed after n has completed execution.” Figure 1 shows a procedure in Pascal. Figure 2 shows the list of instructions in procedure Search that has been derived automatically from the code; the instructions are also listed in column 2 in Figure 1. Figure 3 shows the set of arcs. Thus, the flowgraph F=<1..21,A,1,21> where A is shown in Figure 3.
56 procedure Search
57 (* searches for pivot *)
58 (i, (* current row number *)
59 n: integer; (* # of equations *)
60 var index : ary2i; (* pivot indexes *)
61 irow, icol : integer); (* indices of
62 the old pivot *)
63
64 var
65 big : real;
66 j,k : integer;
67
68 begin
69 (* search for largest element *)
70 1 big := 0.0;
71 2-4,17 for j := 1 to n do
72 begin
73 5 if index[j, 3] <> 1 then
74 begin
75 6-8,16 for k := 1 to n do
76 begin
77 9 if index[k, 3] > 1 then
78 10 writeln('ERROR: matrix singular');
79 11 if index[k, 3] < 1 then
80 12 if abs(b[j, k]) >= big then
81 begin
82 13 irow := j;
83 14 icol := k;
84 15 big := abs(b[j, k])
85 end
86 end (* k loop *)
87 end
88 end (* j loop *);
89 18 index[icol, 3] := index[icol, 3] + 1;
90 19 index[i, 1] := irow;
91 20 index[i, 2] := icol;
92 21 end; (* search *)
93
FIGURE 1. Procedure Search.
1 big:=0.0
2 j:=1
3 _ub1:=n
4 j<=_ub1
5 index[j,3]<>1
6 k:=1
7 _ub2:=n
8 k<=_ub2
9 index[k,3]>1
10 writeln(' ERROR: matrix singular')
11 index[k,3]<1
12 abs(b[j,k])>=big
13 irow:=j
14 icol:=k
15 big:=abs(b[j,k])
16 k:=succ(k)
17 j:=succ(j)
18 index[icol,3]:=index[icol,3]+1
19 index[i,1]:=irow
20 index[i,2]:=icol
21 EXIT
FIGURE 2. Instructions in procedure Search from Figure 1 (Step 1).
1 ---> 2
2 ---> 3
3 ---> 4
4 ---> 18 5
5 ---> 17 6
6 ---> 7
7 ---> 8
8 ---> 17 9
9 ---> 11 10
10 ---> 11
11 ---> 16 12
12 ---> 16 13
13 ---> 14
14 ---> 15
15 ---> 16
16 ---> 8
17 ---> 4
18 ---> 19
19 ---> 20
20 ---> 21
FIGURE 3. Transfer of control between instructions in Figure 2. Notation “k –> list of nodes” means: control can be passed from node k to any in the list.
Flowgraph * Node -> set of Node
– returns the set of successor of node in the flowgraphFlowgraph * Node -> set of Node
– returns the set of predecessors of node in the flowgraphIs-path-in-Graph: Flowgraph * Path -> bool
– Is-path-in-Graph (G, p) = = p is a path in G.m ** k
, where k is a natural number? Test your solution.