Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot zur Agenda Produktseite wechseln Projekt Beratung

Suchen Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMSL/looseSL/ Datei vom 13.4.2020 mit Größe 3 kB

Quellcode-Bibliothek auxil.vdmsl Interaktion und
PortierbarkeitVDM

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

quality89%

¤ 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.0.13Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.