1. Basic Exercises

1. Evaluate the following expressions:
1. {x | x in set {2,...,5} & x > 2}
2. {x | x in set {2,...,5} & x*x > 22}
3. dunion{ {1,2},{1,5,6},{3,4,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.
2. The class of even integers.
3. The set of even integers less than 30.
4. The sets s1 and s2 are non-empty and disjoint (i.e. they have no elements in common).
5. The elements contained in both s1 and s2 are also in s3.
3. Write an explicit function definition for the set difference operator.
4. If s is of type set of (set of nat), write an expression which says that all the sets in s are disjoint.

2. Connected Sets

1. A ConSet is a non-empty collection of distinct, non-empty collections of values of type A. Define a type ConSet to represent ConSets.
2. A "tightly connected" ConSet is a set of sets such that every set element shares at least one A-value with every other set element. Define a Boolean function TC which tests a ConSet to see if it is tightly connected or not.
3. An "n-connected" ConSet is a set of sets such that every set share at least one object with exactly n other set elements. Define a Boolean function NC which tests a ConSet for "n-connectedness"
4. A non-trivial "ring-connected" ConSet is a set of sets such that there is a cyclic ordering of all the elements such that only pairs of adjacent sets share A values. Define a Boolean function RC which tests for the above property. (Hint: use recursion).

3. Equivalence recordings

1. An equivalence class recording is a non-empty set of non-empty distinct, non-overlapping sets of elements. The representation of elements is immaterial.

 

 
 
 

Define the type of such partitionings and, if needed, an appropriate invariant.

Define a value belonging to this type which puts 1 and 2 in one equivalence class, 3 alone in another equivalence class and 4, 5 and 6 in the last equivalence class.

2. A marked partitioning is a non-empty set of pairs, each pair consists of a distinct object and a set of objects such that the first object is not a member of any (second) set of the marked partitioning, and such that all such sets have no elements in common.

 

 
 
 

Define the type of such marked partitionings and, if needed, an appropriate invariant.

3. Define two functions: one which given a well-formed marken partitioning produces a "corresponding" equivalence class recording, and one which given a well-formed equivalence recording generates the set of all possible "correspondig" marked partitions. In order to define the second function it is neccesary to use a match value pattern and set patterns. No examples have been given for this in the book but these kind of patterns are described in the appendix.

4. A thesaurus

formal, aloof, ceremonious, civil, dignified, distant, dress, dressy, icy, impersonal, literary, nominal, official, outward, perfunctory, priggish, polite, ...

Define functions to effect the following commands:

• Add a word to a grouping in the thesaurus. The user will supply a word already in the thesaurus and a new word with a similar meaning. Remember to ensure that the invariant is respected.
• Remove a word form the thesaurus. The user will supply the word to be removed.
• Return the words which have a similar meaning to a given word.
• Return the number of words which have a similar meaning to a given word.

5. Store manager for chemical waste

types

   Vessel :: vid      : VId
             material : MaterialType
             quantity : real;

   MaterialType = <Hot> | <Warm> | <Cold>;

Rack ::    rid      : Rid
           contents : set of Vessel
           capacity : nat;

   Store = set of Rack;

  Vid = token;

    Rid = token

1. Record the following restrictions in the storage model:
1.  No two racks in a store have the same identifier.
2.  No two vessels in a store have the same identifier.
3. No rack has more vessels in it that its capacity allows.
4. At most one vessel in a rack contains hot material.
2. We need some way of finding places for vessels in the store so that the restrictions above continue to be respected.  Define the following functions:
1. Create an empty store.
2. Get the identifiers of all the vessels in a store.
3. Given a rack, return true if the rack is full up, false otherwise.
4. A rack is "viable" for storage of a vessel if the restrictions in 2.1 (c) and (d) will be respected if the vessel is   added to the rack. Define a boolean function "viable" that returns true if a given rack is viable for storage of a  given vessel and and returns false otherwise.
5. Define a function "safe-place" which, given a store and a vessel, returns a viable rack from the store for the  vessel. The function should return the value nil if no viable rack exists in the store.
6. Define a function "place" which places a vessel in a given rack in the store. Use a pre-condition to ensure that  the rack is viable and that no other vessel with the same identifier already exists in the store.