Quelle  Relations.vdmsl   Sprache: 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