\section{Dynamic Semantics}
\label{dynamic}
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:
\begin{vdm_al}
module DYNSEM
imports
from AST all,
from STATSEM all
exports all
definitions
types
DynEnv = map AST`Identifier to AST`Value;
\end{vdm_al}
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
{\tt EvalProgram} is the well-formedness of the program and a
second condition which concerns the division by zero and will be
explained later on.
\begin{vdm_al}
functions
EvalProgram : AST`Program -> DynEnv
EvalProgram(mk_AST`Program(decls, stmt)) ==
EvalStmt(stmt, EvalDeclarations(decls))
pre STATSEM`wf_Program(mk_AST`Program(decls, stmt)) and
pre_EvalStmt(stmt, EvalDeclarations(decls));
\end{vdm_al}
Evaluating uninitiated variable declarations, a proper default value
is assigned: {\tt false} for Boolean values and {\tt 0} for Integer values.
\begin{vdm_al}
EvalDeclarations : seq of AST`Declaration -> DynEnv
EvalDeclarations(decls) ==
{id |-> if val <> nil
then val
elseif tp = <BoolType>
then mk_AST`BoolVal(false)
else mk_AST`IntVal(0)
| mk_AST`Declaration(id, tp, val) in seq decls};
\end{vdm_al}
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.
\begin{vdm_al}
EvalStmt : AST`Stmt * DynEnv -> DynEnv
EvalStmt(stmt, denv) ==
cases true :
(is_AST`BlockStmt(stmt)) -> EvalBlockStmt(stmt, denv),
(is_AST`AssignStmt(stmt)) -> EvalAssignStmt(stmt, denv),
(is_AST`CondStmt(stmt)) -> EvalCondStmt(stmt, denv),
(is_AST`ForStmt(stmt)) -> EvalForStmt(stmt, denv),
(is_AST`RepeatStmt(stmt)) -> EvalRepeatStmt(stmt, denv)
end
pre (is_AST`BlockStmt(stmt) => pre_EvalBlockStmt(stmt, denv)) and
(is_AST`AssignStmt(stmt) => pre_EvalAssignStmt(stmt, denv)) and
(is_AST`CondStmt(stmt) => pre_EvalCondStmt(stmt, denv)) and
(is_AST`ForStmt(stmt) => pre_EvalForStmt(stmt, denv)) and
(is_AST`RepeatStmt(stmt) => pre_EvalRepeatStmt(stmt, denv));
EvalBlockStmt : AST`BlockStmt * DynEnv -> DynEnv
EvalBlockStmt(mk_AST`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 AST`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)
measure LenStmt;
LenStmt: seq of AST`Stmt * DynEnv -> nat
LenStmt(l,-) ==
len l;
EvalAssignStmt : AST`AssignStmt * DynEnv -> DynEnv
EvalAssignStmt(mk_AST`AssignStmt(lhs, rhs), denv) ==
denv ++ {lhs.id |-> EvalExpr(rhs, denv)}
pre pre_EvalExpr(rhs, denv);
EvalCondStmt : AST`CondStmt * DynEnv -> DynEnv
EvalCondStmt(mk_AST`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 : AST`RepeatStmt * DynEnv -> DynEnv
EvalRepeatStmt(mk_AST`RepeatStmt(repeat, until), denv) ==
let denv' = EvalStmt(repeat, denv) in
if EvalExpr(until, denv').val
then denv'
else EvalRepeatStmt(mk_AST`RepeatStmt(repeat, until), denv')
pre pre_EvalStmt(repeat, denv) and
pre_EvalExpr(until, EvalStmt(repeat, denv));
\end{vdm_al}
Note that it is impossible to write a measure for this function bacause this
corresponds to the halting problem.
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:
\begin{enumerate}
\item {\it 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:
\begin{alltt}
for i := 1 to 5 do ...
\end{alltt}
After each execution of the loop's body the loop-variable is
increased.
\item {\it Boolean expression and running execution
of the assignment}. \\
The evaluation of the expression and the assignment is performed
continuously:
\begin{alltt}
i := 1;
for (i := i + 1, i = 5) do ...
\end{alltt}
The loop is executed until the Boolean expression evaluates to
'true'.
\item {\it 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.
\end{enumerate}
The most obvious approach is the specification of the expression as an
integer type and and the constraint to evaluate the assignment once.
Further questions concerning the loop-variable arise:
\begin{enumerate}
\item Is it allowed to use the loop-variable inside the
stop-expression?
\item Is it allowed to change the loop-variable inside the
body?
\item Is it allowed to change the variables, which are used in the
stop-expression, inside the body?
\end{enumerate}
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.
\begin{vdm_al}
EvalForStmt : AST`ForStmt * DynEnv -> DynEnv
EvalForStmt(mk_AST`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 : AST`Variable * AST`Value * AST`Stmt * DynEnv -> DynEnv
EvalForLoop(mk_AST`Variable(id), val, stmt, denv) ==
if denv(id).val <= val.val
then let denv' = EvalStmt(stmt, denv)
in EvalForLoop(mk_AST`Variable(id), val, stmt,
denv' ++ {id |-> mk_AST`IntVal(denv'(id).val + 1)})
else denv
pre pre_EvalStmt(stmt, denv)
measure LoopParInc;
LoopParInc: AST`Variable * AST`Value * AST`Stmt * DynEnv -> nat
LoopParInc(mk_AST`Variable(id), val, -, denv) ==
val.val - denv(id).val;
\end{vdm_al}
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.
\begin{vdm_al}
EvalExpr : AST`Expr * DynEnv -> AST`Value
EvalExpr(ex, denv) ==
cases ex :
mk_AST`BoolVal(-),
mk_AST`IntVal(-) -> ex,
mk_AST`Variable(id) -> denv(id),
mk_AST`BinaryExpr(-,-,-) -> EvalBinaryExpr(ex, denv)
end
pre is_AST`BinaryExpr(ex) => pre_EvalBinaryExpr(ex, denv);
EvalBinaryExpr : AST`BinaryExpr * DynEnv -> AST`Value
EvalBinaryExpr(mk_AST`BinaryExpr(lhs, op, rhs), denv) ==
let v1 = EvalExpr(lhs, denv).val,
v2 = EvalExpr(rhs, denv).val
in cases op :
<Add> -> mk_AST`IntVal(v1 + v2),
<Sub> -> mk_AST`IntVal(v1 - v2),
<Div> -> mk_AST`IntVal(v1 div v2),
<Mul> -> mk_AST`IntVal(v1 * v2),
<Lt> -> mk_AST`BoolVal(v1 < v2),
<Gt> -> mk_AST`BoolVal(v1 > v2),
<Eq> -> mk_AST`BoolVal(v1 = v2),
<And> -> mk_AST`BoolVal(v1 and v2),
<Or> -> mk_AST`BoolVal(v1 or v2)
end
pre op = <Div> => EvalExpr(rhs, denv).val <> 0;
end DYNSEM
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|