| products/sources/formale Sprachen/VDM/VDMSL/DigraphSL/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Relations.vdmsl Sprache: VDMOriginal von: VDM© |
|
||||||
|
------------------------------------------------------------------
-- Module relations -- Author: Janusz Laski -- Purpose: Exports functions for manipulating binary relations -- Version 2.0 (January 10, 2010) ----------------------------------------------------------------- module relations exports all definitions types Node=nat1; BinRel = set of (nat1 * nat1); values A0: BinRel = {}; -- empty relation A1: BinRel={mk_(1,2)}; -- singleton relation A2: BinRel={mk_(1,2), mk_(2,3), mk_(3,4)}; -- linear relation A3: BinRel=A1 union {mk_(4,5), mk_(4, 1), mk_(5, 6), mk_(6, 7), mk_(7, 8), mk_(8, 9), mk_(9, 10), mk_(2,3)}; -- binary tree rooted at 4 A4: BinRel={mk_(1,2), mk_(2,3), mk_(2,4), mk_(3,5), mk_(4,5), mk_(5,6)}; -- acyclic relation A5: BinRel={mk_(1,2), mk_(2,3), mk_(2,4), mk_(3,5), mk_(4,6), mk_(6,5), mk_(5,7)}; -- acyclic relation A6: BinRel={mk_(1,1), mk_(2,2), mk_(3,3), mk_(4,4), mk_(5,5)}; --sling relation A7: BinRel={mk_(1,2), mk_(2,3), mk_(2,4), mk_(3,5), mk_(4,6), mk_(6,5), mk_(5,7), mk_(5,2)}; -- cyclic relation A8: BinRel=A7 union {mk_(6,1)}; -- nested cycle functions -- TESTING PROPERTIES OF RELATIONS IsReflexive:BinRel-> bool IsReflexive(R)== forall x in set field(R) & mk_(x,x) in set R; IsSymmetrical:BinRel-> bool IsSymmetrical(R)== forall x,y in set field(R) & ((mk_(x,y) in set R) => (mk_(y,x) in set R)); IsTransitive:BinRel-> bool IsTransitive(R)== forall x,y,z in set field(R) & (((mk_(x,y) in set R) and (mk_(y,z) in set R))=> (mk_(x,z) in set R)); IsEquivalence:BinRel-> bool IsEquivalence(R)== IsReflexive(R) and IsSymmetrical(R) and IsTransitive(R); -- OPERATIONS ON RELATIONS domain:BinRel -> set of nat1 domain(R) == { x | mk_(x,-) in set R}; domain1:BinRel -> set of nat1 -- can't be interpreted 'cause of type binds domain1(R) == {x|x:nat1 & exists y:nat1 & mk_(x,y) in set R}; range:BinRel -> set of nat1 range(R) == { y | mk_(-,y) in set R}; field:BinRel -> set of nat1 field(R) == domain(R) union range(R); inverse_rel:BinRel -> BinRel inverse_rel(R) == {mk_(y,x)|mk_(x,y) in set R}; -- or x in set domain(R),y in set range(R) & mk_(x,y) in set R}; id_rel: BinRel -> BinRel -- Returns the identity relation of R id_rel(R) == {mk_(x,x)| x in set field(R)}; Composition:BinRel * BinRel -> BinRel Composition(R,Q) == {mk_(a,c)|mk_(a,b1) in set R, mk_(b2,c) in set Q & b1=b2}; -- or{mk_(a,c)| a in set domain(R), c in set range(Q) & -- exists b in set (range(R) inter domain(Q)) & -- mk_(a,b) in set R and mk_(b,c) in set Q}; power_of:BinRel * nat1 -> BinRel --returns the xth power of R power_of(R,x) == if (x = 1) then R else Composition(R, power_of(R, x-1)) pre x>0; Power_rel: BinRel * nat -> BinRel -- Returns the kth power of R. Power_rel(R,k) == if k=0 then id_rel(R) elseif k=1 then R else Composition(R,Power_rel(R, k-1)); -- RELATIONAL CLOSURES Reflexive_cl: BinRel -> BinRel -- Returns the reflexive closure of R Reflexive_cl(R) == (R union id_rel(R)); Symmetric_cl: BinRel -> BinRel -- Returns the symmetric closure of R Symmetric_cl(R) == R union inverse_rel(R); Transitive_cl: BinRel -> BinRel -- Returns the transitive irreflexive closure of R -- Identical to formal definition of closure. -- Very inefficient interpretation: for every k,k>1, ALL -- lower powers of R are computed from scratch Transitive_cl(R) == dunion{Power_rel(R,k) | k in set {1,...,card field(R)}}; TransitiveRefl_cl: BinRel -> BinRel -- Returns the transitive reflexive closure of R TransitiveRefl_cl(R) == dunion{Power_rel(R,k) | k in set {0,...,card field(R)}}; PowerList: BinRel -> seq of BinRel PowerList(R) == BuildList(R, card field(R)) pre R<>{}; BuildList: BinRel * nat1 -> seq of BinRel -- BuildList(R,n) == sequence of powers of relation R, of maximal length n, -- i.e. RESULT = [Power_rel(R,1),...,Power_rel(R,n)], n>0. -- Thus RESULT(i)=Power_rel(R,i), 0<i<=n. -- For ACYCLIC R, only NONEMPTY powers of R are computed, i.e. -- in that case the length of the result list may be less than n. -- If R = {} the result is [{}] for any n>0. -- The function derives each power of R only once. BuildList(R,n) == if n=1 then [R] else let M= BuildList(R,n-1), C=Composition(M(len M),R) in if C={} --empty higher powers of R then M else M ^ [C] pre n>0; maxset: set1 of int -> int -- returns maximum of set maxset(S) == let x in set S in if card S = 1 then x else max2(x,maxset(S\ {x})); max2: int * int -> int max2(a,b) == if a>= b then a else b; operations pure Warshall: BinRel ==> BinRel -- efficiently computes transitive closure of Q Warshall(Q) == (dcl i: nat1, j: nat1, k: nat1, R: BinRel; R := Q; let n = maxset (field(R)) in for k = 1 to n do for i = 1 to n do for j = 1 to n do if mk_(i,j) not in set R then if mk_(i,k) in set R and mk_(k,j) in set R then R := R union {mk_(i,j)}; return R; ); -- Testing functions&operations functions test_PowerList: BinRel -> bool -- tests PowerList using a simpler albeit inefficient -- Power_Rel as an automatic test oracle, to avoid manual test evaluation test_PowerList(R)== let L = PowerList(R), n = card field(R) in (forall i in set inds L & L(i)=Power_rel(R,i)) and len L<n => Power_rel(R, len L +1) ={}; -- For "normal" applications pre_PowerList(R) <=> R<>{} should be observed. -- However, PowerList should also be tested for R={}. -- Such a STRESS TEST shows the function's behaviour for invalid data. end relations ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
