/CVS_Hangout1

Construction and Verification of Software

Hangout 1

Your mission is to complete the method XorSet.

Completely specify the methods by writing the weakest pre-condition and the strongest post-condition possible. Implement and verify the methods according to that same specification.

Consider the given functions unique, contains, and isSet.

- Specify and implement method XorSet below. The functionality of this method
it to return the array (and the corresponding number of elements) containing 
the elements that are in one of the arrays (a or b) but not in both. The arrays
are given as parameters together with their number of elements (na or nb).

- Both arrays are considered "sets", having no repetitions. The resulting array
should also be a "set".

- In the specification, define the weakest preconditions and the strongest 
postconditions you can think of. Implement and verify the method so that it
satisfies the post-conditions assuming the pre-conditions.

The due date is Friday, 12 of April, 23h59m.