Quelle dynsem.vdmsl Sprache: VDM

\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}

quality90%

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.