|
\section{Auxiliary Functions}
This section contains a number of auxiliary functions and operations.
\begin{vdm_al}
operations
SeqOfSetOf2SetOfSeqOf : seq of set of (VAL | BlkEnv) ==>
set of seq of (VAL | BlkEnv)
SeqOfSetOf2SetOfSeqOf(seq_ls) ==
( dcl res_s : set of seq of (VAL | BlkEnv) := { [] } ,
tmpres_s : set of seq of (VAL | BlkEnv) ;
for tmp_s in seq_ls do
( tmpres_s := {} ;
for all tmp_l in set res_s do
for all e in set tmp_s do
tmpres_s := tmpres_s union { tmp_l ^ [ e ] } ;
res_s := tmpres_s
);
return res_s
)
\end{vdm_al}
$SeqOfSetOf2SetOfSeqOf$ transforms a sequence of sets to a set of
sequences.
\begin{vdm_al}
functions
Consistent: LVAL * Model -> LVAL
Consistent(lval,bind) ==
{mk_(val,b munion bind)
| mk_(val,b) in set lval &
forall id in set (dom b inter dom bind) &
b(id) = bind(id)};
\end{vdm_al}
The $Consistent$ function is very important because it precisely
specifies which parts of a loose value are ``consistent'' with a
given model. The point is that when one are not taking the binding of
the formal parameters of functions into the model then the consistency
check is simply that those unique identifiers which are present in a
loose value pair and also in the given model must match the same
chosen value (i.e.\ the choices may not be inconsistent). This is a
sufficient condition because the identifiers uniquely identify in
which context the choice is made.
\begin{vdm_al}
SetToSeq: set of VAL +> seq of VAL
SetToSeq(s) ==
if s = {}
then []
else let e in set s
in
[e] ^ SetToSeq(s\{e})
post s = elems RESULT;
\end{vdm_al}
$SetToSeq$ transforms a set of values to a sequence of values (in
an arbitrary order).
\begin{vdm_al}
Permute: seq of VAL -> set of seq of VAL
Permute(l) ==
cases l:
[],
[-] -> { l },
others -> dunion { { [ l(i) ] ^ j | j in set Permute(RestSeq(l, i))} |
i in set inds l }
end;
RestSeq: seq of VAL * nat1 -> seq of VAL
RestSeq(l,i) ==
[ l(j) | j in set (inds l \ { i }) ];
\end{vdm_al}
$Permute$ and $RestSeq$ takes care of generating a set of all
permutations of the given sequence of values.
\begin{vdm_al}
PatternIds: Pattern +> set of UniqueId
PatternIds(pat) ==
cases pat:
mk_PatternName(mk_(nm,pos)) -> {mk_(nm,pos,FnInfo())},
mk_MatchVal(-) -> {},
mk_SetEnumPattern(els) -> dunion {PatternIds(elem)
|elem in set elems els},
mk_SetUnionPattern(lp,rp) -> PatternIds(lp) union
PatternIds(rp)
end
\end{vdm_al}
This auxiliary function is used to find the set of unique identifiers
from a pattern.
\section{Test Coverage}
The specification have been tested. The coverage of the tests which
have been used can be presented as:
%\begin{rtinfo}[LooseEvalSetEnumerationExpr]
%{loose}[DefaultMod]
%\end{rtinfo}
Notice that all constructs in the entire specification have been
covered. This would not have been the case if the test suite have not
been run with pre and post condition checking switched on. Thus, we
feel that we can have a reasonable amount of confidence in the
correctness of the specification. Under ``normal'' circumstances (at
least in our own work) this would be the place where one would explain
about why certain parts of the specification had not been fully
covered.
¤ Dauer der Verarbeitung: 0.21 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.
|
