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

quality90%

¤ Dauer der Verarbeitung: 0.15 Sekunden (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.