| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMSL/ADTSL/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 520 B |
|
SSL CountryColouring.vdmsl
Interaktion und |
|||||||||
|
\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} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28