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

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMSL/recursiveSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

Quelle labgraphs.vdmsl Sprache: VDM

types

LabGraph = map NodeId to (map ArcId to NodeId)
inv g ==
  UniqueArcIds(g) and
  forall m in set rng g & rng m subset dom g;

AcyclicLabGraph = LabGraph
inv acg ==
  not exists id in set dom acg &
     id in set AllLabDesc(acg,id);

NodeId = nat;

ArcId = nat

functions

AllLabDesc: LabGraph * NodeId -> set of NodeId
AllLabDesc(g,id) ==
  dunion {LabDescendents(g,c,{})| c in set rng g(id)}
pre id in set dom g;

measureLabGraphReached : LabGraph * Id * set of Id -> nat
measureLabGraphReached(g,-,reached) ==
  card dom g - card reached;

LabDescendents: LabGraph * NodeId * set of NodeId -> set of NodeId
LabDescendents(g,id,reached) ==
  if id in set reached
  then {}
  else {id} union
       dunion {LabDescendents(g,c,reached union {id})
              | c in set rng g(id)}
pre id in set dom g
measure measureLabGraphReached;

UniqueArcIds: map NodeId to (map ArcId to NodeId) -> bool
UniqueArcIds(g) ==
  let m = {nid |-> dom g(nid) | nid in set dom g}
  in
    forall nid1, nid2 in set dom m &
       nid1 <> nid2 => m(nid1) inter m(nid2) = {}

values

  lgraph : LabGraph = {1 |-> {1 |-> 2,2 |-> 3},
                       2 |-> {3 |-> 4},
                       3 |-> {4 |-> 5},
                       4 |-> {5 |-> 6},
                       5 |-> {6 |-> 6},
                       6 |-> {|->}}

quality96%

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