1. Basic Exercises

1. Evaluating
1. {x | x in set {2,...,5} & x > 2} = {3,4,5}
2. {x | x in set {2,...,5} & x*x > 22} = {5}
3. dunion{ {1,2},{1,5,6},{3,4,6}} = {1,...,6}
4. dinter{ {1,2},{1,5,6},{3,4,6}} = {}
2. Express the following in VDM-SL:
1. The set s has less than 5 elements: card s < 5
2. The class of even integers: this has to be a type rather than a set, because the class of values could be infinitely large. We therefore use a type definition with an invariant to capture the limitation:

     Evens = int
     inv n == exists h : int & h*2=n

3. The set of even integers less than 30: this is a finite set, so it can be defined by a set comprehension:

        { x | x:int & (exists h:int & h*2=n) and x < 30}

4. The sets s1 and s2 are non-empty and disjoint (i.e. they have no elements in common).

        s1 <> {} and s2 <> {} and s1 inter s2 = {}

5. The elements contained in both s1 and s2 are also in s3.

        s1 inter s2 subset s3

3. Write an explicit function definition for the set difference operator.

        diff: set of X * set of X -> set of X
        diff(s1,s2) == { x | x in set s1 & not x in set s2}

        -- Alternatively, use a type binding in the comprehension:

        diff2: set of X * set of X -> set of X
        diff2(s1,s2) == { x | x : X & x in set s1 and not x in set s2}

4. If s is of type set of (set of nat), write an expression which says that all the sets in s are disjoint.

        forall s1,s2 in set s & s1 <> s2 => s1 inter s2 = {}

Notice that the following is incorrect:

        forall s1,s2 in set s & s1 inter s2 = {}

because s1 and s2 could evaluate to the same set in s. The erroneaous expression above is going to be false for any s except the set containing only the empty set (i.e. the case where s = { {} }

2. Connected Sets

types

  ConSet = set of set of A
  inv cs == 
    cs <> {} and 
    forall s in set cs & s <> {};

  A = token;

functions

  TC: ConSet -> bool
  TC(cs) ==
    forall s1, s2 in set cs & s1 inter s2 <> {};

  NC: ConSet * nat -> bool
  NC(cs,n) ==
    forall s1 in set cs &
      card {s | s in set cs & s inter s1 <> {}} = n + 1;

  RC: ConSet -> bool
  RC(cs) ==
    NC(cs,2) and
    let s1 in set cs 
    in
      let s2 in set cs \ {s1} be st s1 inter s2 <> {}
      in
        CheckOrder(cs \ {s1,s2}, s1, s2);

  CheckOrder: set of set of A * set of A * set of A -> bool
  CheckOrder(cs,sfirst,snext) ==
    if card cs < 2
    then forall s in set cs & s inter sfirst <> {}
    else if exists s in set cs & s inter snext <> {}
         then let s in set cs be st s inter snext <> {} 
              in
                CheckOrder(cs \ {s}, sfirst, s)
         else false;

values

  s1: set of A = {mk_token(1),mk_token(2),mk_token(3)};
  s2: set of A = {mk_token(3),mk_token(4)};
  s3: set of A = {mk_token(4),mk_token(5),mk_token(2)};
  s4: set of A = {mk_token(6),mk_token(7)};
  s5: set of A = {mk_token(7),mk_token(8)};
  s6: set of A = {mk_token(8),mk_token(6)};

  cs1: ConSet = {s1,s2,s3};
  cs2: ConSet = {s1,s2,s3,s4,s5,s6};

3. Equivalence recordings

-- solution for part 1
types

  Equiv = set of set of Elem
  inv equiv == 
    equiv <> {} and
    forall es1,es2 in set equiv &
      es1 <> es2 => es1 inter es2 = {} and
      es1 <> {};

  Elem = token;

values

  eq: Equiv = {{mk_token(1),mk_token(2)},
               {mk_token(3)},
               {mk_token(4),mk_token(5),mk_token(6)}};

-- solution for part 2
types

  MarkedParts = set of Pair
  inv mps ==
    mps <> {} and
    forall p1,p2 in set mps &
      not p1.elem in set p1.parti union p2.parti and
      p1 <> p2 => (p1.elem <> p2.elem and
                   p1.parti inter p2.parti = {});

  Pair ::
    elem : Elem
    parti: set of Elem;

-- solution for part 3

functions

  Marked2Equiv: MarkedParts -> Equiv
  Marked2Equiv(mps) ==
    {{elem} union parti | mk_Pair(elem,parti) in set mps};

  Equiv2Markeds: Equiv -> set of MarkedParts
  Equiv2Markeds(equiv) ==
    {{mk_Pair(elem,parti)|{(elem)} union parti in set equiv}
    | elem in set dunion equiv}

  -- note that the (elem) is a math value pattern meaning that 
  -- the value of "elem" in this context is used rather than a 
  -- new identifier being intruduced. The set union pattern
  -- between a singleton set with elem and the rest (parti) 
  -- is used to make an arbitrary split between them.

4. A thesaurus