|
\section{The Environment Context}
In order for the loose evaluation to take place, the context in
which the expression is to be evaluated must be
initialized and maintained. This is taken care of by the definitions
presented in this section.
\subsection{The Evaluation Stack}
The semantic domains describe the type of the structure which will be
used for specifying the operational (loose) semantics for the abstract
syntax.
\begin{vdm_al}
types
ENVL = seq of ENV;
\end{vdm_al}
The main structure in the semantic domains is the environment, {\it
ENVL} which is organized as a stack of so-called function application
environments {\it ENV}. When a function is called, it must establish a
local environment containing its own definitions such as the formal
parameters.
\begin{vdm_al}
ENV = seq of BlkEnv;
\end{vdm_al}
Expressions can define a local environment called a block environment
$BlkEnv$. For example a let expression will produce a local
environment for which the scope is the body of the let-expression. The
function application environment is therefore organized as a stack of
block environments where the first block environment pushed on the
stack contains the instantiation of the formal parameters. When the
value of an identifier is looked up this will happen in a top-down
manner down through the block environments.
\begin{vdm_al}
BlkEnv = seq of NameVal;
\end{vdm_al}
Finally a block environment is a sequence of {\it NameVal}s, each
containing a unique identifier and its associated value. A {\it BlkEnv}
could alternatively be modelled as a map. We have chosen to use a sequence
in order to keep it in line with the operational dynamic semantics
presented in \cite{Larsen&91}.
\begin{vdm_al}
NameVal = UniqueId * VAL;
UniqueId = (Name * Position * ([Name * VAL]));
\end{vdm_al}
The unique names which are used here deserve a little additional explanation.
The unique name contains the actual name (from a pattern identifier),
the position (of the pattern identifier\footnote{As already mentioned
this could in principle simply be any other unique identification of
the occurence of the name.}) and if the binding takes
place inside the body of a function, the function name and the argument (value) to
the function are added (otherwise \kw{nil} is used).
This corresponds to the dynamic tagging
information used in \cite{Larsen93b}.
\subsection{Semantic Values}\label{semantic}
\begin{vdm_al}
LVAL = set of (VAL * Model);
\end{vdm_al}
The ``loose values'' returned by the loose expression evaluation functions
is a set of pairs. The first element of such a pair is the value of
the expression in the model described by the second element of the
pair. Thus, one gets information about both external looseness (where
different models yields different results) and internal looseness
(where each model yield the same result).
\begin{vdm_al}
Model = map UniqueId to VAL;
\end{vdm_al}
A model contains a precise description of all the choices made
underway in the loose evaluation of an expression. In this paper the
values considered are simply numerical values, Boolean values and set
values.
\begin{vdm_al}
VAL = NUM | BOOL | SET;
NUM :: v : int;
BOOL :: v : bool;
SET :: v : set of VAL
\end{vdm_al}
\subsection{The State Definition}
The state of this specification contains the environment described
above, $env-l$, and additionally some information about the context of the
expression (i.e.\ the value definitions, $val-m$, and function
definitions, $fn-m$ it
may make use of). The {\it curfn} component indicates whether we
are currently evaluating an expression in the body of some
function\footnote{Note that we could also be evaluating a value expression.}.
If this is the case, information about the function name and the
argument value needs to be added to the unique identifiers which are
created when new pattern identifiers are encountered. Finally the {\it
fnparms} component contains the unique identification of the parameters
of the functions. This information is important because the binding of
these formal parameters do not constitute any input to the models.
Thus, the binding of the formal parameters must {\bf not} be taken
into account in the choices taken in a given model. The reason for
this will be clear at the end of the next section.
\begin{vdm_al}
state Sigma of
env_l: ENVL
val_m: map UniqueId to LVAL
fn_m: map Name to (Pattern * Expr)
curfn: seq of (Name * VAL)
fnparms: set of UniqueId
init s ==
s = mk_Sigma([[]],
{|->},
{|->},
[],
{})
end
\end{vdm_al}
\subsection{Creation of Context}
In order to be able to use value and function definitions in the
expressions we would like to analyse this subsection contains a small
operation which create the context and thereby initialize the state
components accordingly.
\begin{vdm_al}
operations
CreateContext: Definitions ==> ()
CreateContext(mk_Definitions(valuem,fnm)) ==
(InstallValueDefs(valuem);
InstallFnDefs(fnm));
\end{vdm_al}
\subsection{Value Definitions handling}
For value definitions it is taken into account that looseness can
arise both on the right hand side expression and on the left hand side
pattern (matching). This is done below and the state component {\it
val\_l} is initialized.
\begin{vdm_al}
InstallValueDefs: seq of ValueDef ==> ()
InstallValueDefs(val_l) ==
for mk_ValueDef(pat,expr) in val_l do
let lval = LooseEvalExpr(expr)
in
for all mk_(val,model) in set lval do
let env_s = PatternMatch(pat,val)
in
val_m := Extend(val_m,
{id |-> {mk_(Look(env,id),model)|env in set env_s}
| id in set dinter {SelDom(env)| env in set env_s}});
\end{vdm_al}
\subsection{Function Definitions handling}
This subsection contains functions which manipulate the state
components which are affected by function definitions.
\begin{vdm_al}
InstallFnDefs: map Name to ExplFnDef ==> ()
InstallFnDefs(fn_marg) ==
fn_m := {nm |-> mk_(fn_marg(nm).pat,fn_marg(nm).body)
| nm in set dom fn_marg};
InstallCurFn: Name * VAL * set of UniqueId ==> ()
InstallCurFn(nm,val,patids) ==
(curfn := [mk_(nm,val)] ^ curfn;
fnparms := fnparms union patids);
LeaveCurFn: () ==> ()
LeaveCurFn() ==
curfn := tl curfn
pre curfn <> []
\end{vdm_al}
\subsection{Stack Manipulating Functions}
This subsection contains a number of simple auxiliary operations which
manipulate the environment. These are mainly operations for popping
and pushing various kinds of environments, but also operations for
manipulating environments and looking up bindings in environments.
\begin{vdm_al}
operations
PopEnvL: () ==> ()
PopEnvL() ==
env_l := tl env_l;
TopEnvL : () ==> ENV
TopEnvL () ==
return hd env_l;
PushEmptyEnv : () ==> ()
PushEmptyEnv () ==
env_l := [ [] ] ^ env_l;
PopBlkEnv : () ==> ()
PopBlkEnv () ==
env_l := [ tl hd env_l ] ^ tl env_l;
PushBlkEnv : BlkEnv ==> ()
PushBlkEnv (benv) ==
env_l := [ [ benv ] ^ hd env_l ] ^ tl env_l;
MkEmptyBlkEnv: () ==> BlkEnv
MkEmptyBlkEnv() ==
return [];
CombineBlkEnv : BlkEnv * BlkEnv ==> BlkEnv
CombineBlkEnv ( env1,env2) ==
return env1 ^ env2;
MkBlkEnv : (Name * Position) * VAL ==> BlkEnv
MkBlkEnv (mk_(nm,pos), val_v ) ==
let fninfo = FnInfo()
in
return [ mk_(mk_(nm, pos, fninfo), val_v)];
pure FnInfo: () ==> [Name * VAL]
FnInfo() ==
if len curfn = 0
then return nil
else return hd curfn;
LooseLookUp: Name ==> LVAL
LooseLookUp(nm) ==
(let topenv = TopEnvL()
in
for env in topenv do
for mk_(id,val) in env do
if SelName(id) = nm
then return {mk_(val, if id in set fnparms
then {|->}
else {id |-> val})}
else skip;
LookUpValueDefs(nm));
LookUpValueDefs: Name ==> LVAL
LookUpValueDefs(nm) ==
(for all id in set dom val_m do
if SelName(id) = nm
then return {mk_(v,m munion {id |-> v}) | mk_(v,m) in set val_m(id)};
error);
LookUpFn: Name ==> Pattern * Expr
LookUpFn(nm) ==
return fn_m(nm)
pre nm in set dom fn_m
functions
SelName: UniqueId +> Name
SelName(mk_(nm,-,-)) ==
nm;
SelNameAndPos: UniqueId +> Name * Position
SelNameAndPos(mk_(nm,pos,-)) ==
mk_(nm,pos);
SelDom: BlkEnv +> set of UniqueId
SelDom(blkenv) ==
{id| mk_(id,-) in seq blkenv};
Look: BlkEnv * UniqueId +> VAL
Look(env,id) ==
if env = []
then undefined
else let mk_(nm,val) = hd env
in
if nm = id
then val
else Look(tl env, id)
pre exists mk_(nm,-) in seq env & nm = id;
Extend: (map UniqueId to LVAL) * (map UniqueId to LVAL) +>
(map UniqueId to LVAL)
Extend(val_m,upd_m) ==
val_m ++ {id |-> if id in set dom val_m
then val_m(id) union upd_m(id)
else upd_m(id)
| id in set dom upd_m}
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.25 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.
|
