Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: CountryColouring.vdmsl Sprache: VDM

Original von: VDM^©

\begin{vdm_al}
types

  Country = seq of char;

  Relation = set of (Country * Country);

  Colour = set of Country;

  Colouring = set of Colour;

functions

  isRelation: Relation -> bool
  isRelation(r) ==
    forall mk_(c1,c2) in set r & c1 <> c2;

  areNb: Country * Country * Relation -> bool
  areNb(cn1,cn2,r) ==
    mk_(cn1,cn2) in set r or mk_(cn2,cn1) in set r;

  CountriesRel: Relation -> set of Country
  CountriesRel(r) ==
    dunion {{c1,c2} | mk_(c1,c2) in set r};

  sameColour: Country * Country * Colouring -> bool
  sameColour(cn1,cn2,cols) ==
    exists col in set cols & cn1 in set col and cn2 in set col;

  CountriesCol: Colouring -> set of Country
  CountriesCol(cols) ==
    dunion cols;

  isColouring: Colouring -> bool
  isColouring(cols) ==
    forall col1,col2 in set cols & col1 <> col2 => col1 inter col2 = {};

  isColouringOf: Colouring * set of Country -> bool
  isColouringOf(cols,cns) ==
    CountriesCol(cols) = cns;

  nbDistinctColours: Colouring * Relation -> bool
  nbDistinctColours(cols,r) ==
    forall cn1, cn2 in set CountriesRel(r) &
           areNb(cn1,cn2,r) => not sameColour(cn1,cn2,cols);

  colMap(r: Relation) cols : Colouring
  pre isRelation(r)
  post isColouring(cols) and
       isColouringOf(cols, CountriesRel(r)) and
       nbDistinctColours(cols, r);

  canBeExtBy: Colour * Country * Relation -> bool
  canBeExtBy(col, c, r) ==
    forall c1 in set col & not areNb(c1, c, r);

  extndCol: Colouring * Country * Relation -> Colouring
  extndCol(cols,c,r) ==
    if cols = {}
    then {{c}}
    else let col in set cols
         in
           if canBeExtBy(col,c,r)
           then { {c} union col } union cols \ {col}
           else { col } union extndCol(cols \ {col}, c, r)
  measure CardColouring;

  CardColouring: Colouring * Country * Relation -> nat
  CardColouring(cols,-,-) ==
    card cols;

  colCntrs: set of Country * Relation -> Colouring
  colCntrs(cs, r) ==
    if cs = {}
    then  {}
    else let c in set cs
         in
           extndCol(colCntrs(cs\{c}, r), c, r)
  measure CardCountry;

  CardCountry: set of Country * Relation -> nat
  CardCountry(cs,-) ==
    card cs;

  colMapExpl: Relation -> Colouring
  colMapExpl(r) ==
    colCntrs(CountriesRel(r), r)
   pre isRelation(r)
\end{vdm_al}

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.