|
\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}
¤ Dauer der Verarbeitung: 0.16 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.
|
