Quelle statsem.vdmsl Sprache: VDM

\section{Static Semantics}

In order to check, if a program is well-formed,  a static environment
which maps identifiers to types has to be introduced.
\begin{vdm_al}
module STATSEM

imports from AST all

exports all

definitions

types

  StatEnv = map AST`Identifier to AST`Type;
\end{vdm_al}
Using the static environment, a top-down definition of well-formed
program constructs can be given. In the following definitions the prefix
{\tt wf-} stands for {\it well-formed}.
\begin{vdm_al}
functions

  wf_Program : AST`Program -> bool
  wf_Program(mk_AST`Program(decls, stmt)) ==
    wf_Declarations(decls) and wf_Stmt(stmt, get_Declarations(decls));
\end{vdm_al}
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:
\begin{enumerate}
\item {\it 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.

\item {\it 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.

\item {\it 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 {\tt undefined}, e.g. the expression
{\tt true <AND> undefined} could then be evaluated to {\tt true}.

\item {\it Generating runtime errors}. \\
  The dynamic semantics generates runtime errors, if uninitiated
variables are used in expressions.
\end{enumerate}
In this specification the second solution will be chosen, where
all variables without initiations are initiated with default values.

\begin{vdm_al}
wf_Declarations : seq of AST`Declaration -> bool
wf_Declarations(decls) ==
  (forall i1, i2 in set inds decls &
    i1 <> i2 => decls(i1).id <> decls(i2).id) and
  (forall d in seq decls &
    d.val <> nil =>
    ((is_AST`BoolVal(d.val) and d.tp = <BoolType>) or
     (is_AST`IntVal(d.val) and d.tp = <IntType>)));

get_Declarations : seq of AST`Declaration -> StatEnv
get_Declarations(decls) ==
  {id |-> tp | mk_AST`Declaration(id, tp, -) in seq decls};
\end{vdm_al}
The specification of the static semantics of statements is made by
a simple case distinction.

\begin{vdm_al}
wf_Stmt : AST`Stmt * StatEnv -> bool
wf_Stmt(stmt, senv) ==
  cases true :
    (is_AST`BlockStmt(stmt))  -> wf_BlockStmt(stmt, senv),
    (is_AST`AssignStmt(stmt)) -> let mk_(wf_ass, -) =
                                     wf_AssignStmt(stmt, senv)
                                 in wf_ass,
    (is_AST`CondStmt(stmt))   -> wf_CondStmt(stmt, senv),
    (is_AST`ForStmt(stmt))    -> wf_ForStmt(stmt, senv),
    (is_AST`RepeatStmt(stmt)) -> wf_RepeatStmt(stmt, senv),
    others                -> false
  end;

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

wf_Stmts : seq of AST`Stmt * StatEnv -> bool
wf_Stmts(stmts, senv) ==
  forall stmt in seq stmts & wf_Stmt(stmt, senv);
\end{vdm_al}

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.

\begin{vdm_al}
wf_AssignStmt : AST`AssignStmt * StatEnv -> bool * [AST`Type]
wf_AssignStmt(mk_AST`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);
\end{vdm_al}
In the conditional statement and the repeat-loop a boolean expression
is required:
\begin{vdm_al}
wf_CondStmt : AST`CondStmt * StatEnv -> bool
wf_CondStmt(mk_AST`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 : AST`RepeatStmt * StatEnv -> bool
wf_RepeatStmt(mk_AST`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);
\end{vdm_al}

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 Section \ref{dynamic}. For the static semantics
the most obvious design decision has been made that the stop-expression
should be of type Integer.

\begin{vdm_al}
wf_ForStmt : AST`ForStmt * StatEnv -> bool
wf_ForStmt(mk_AST`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);
\end{vdm_al}

Handling expressions and variables, it is necessary to return the
type in addition to the well-formedness predicate.
\begin{vdm_al}
wf_Expr : AST`Expr * StatEnv -> bool * [AST`Type]
wf_Expr(ex, senv) ==
  cases true :
    (is_AST`BoolVal(ex))    -> mk_(true, <BoolType>),
    (is_AST`IntVal(ex))     -> mk_(true, <IntType>),
    (is_AST`Variable(ex))   -> wf_Variable(ex, senv),
    (is_AST`BinaryExpr(ex)) -> wf_BinaryExpr(ex, senv),
    others                  -> mk_(false, <IntType>)
  end;

wf_Variable : AST`Variable * StatEnv -> bool * [AST`Type]
wf_Variable(mk_AST`Variable(id), senv) ==
  if id in set dom senv
  then mk_(true, senv(id))
  else mk_(false, nil);
\end{vdm_al}

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.

\begin{vdm_al}
wf_BinaryExpr : AST`BinaryExpr * StatEnv -> bool * [AST`Type]
wf_BinaryExpr(mk_AST`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;

end STATSEM
\end{vdm_al}

quality91%

¤ Dauer der Verarbeitung: 0.15 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.