Quellcode-Bibliothek 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%

¤ 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.1Bemerkung: (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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.