B := 0; H := 0;
1. There are 4 kinds of alarm that could be raised: these are Electrical, Mechanical, Biological, Chemical. Represent these using an
enumerated datatype called QUALIFICATION. [5 marks]
2. An Alarm is modelled as a class with 2 variables. One represents the qualification of the alarm, the other is
a description of the alarm represented as a string. [5 marks]
3. An Expert has several qualifications. Model this as a class with
a variable to represent the set of qualifications held by the expert. Include in your class definition a predicate function called Valid(), which re
Hint: remember to use a reads clause to ensure visibility of class variables. [10 marks]
4. The plant is modelled by a class that has a variable
to represent a set of alarms and a variable to represent a set of experts. For consistency of the whole plant, it is necessary
that each type of alarm is covered by at least one expert.
This means that for all alarms, there is an expert that includes the alarm’s qualification in their set of qualifications.
Write a class to represent the Plant and the sets of alarms and experts. Include in your class definition a
predicate function called Complete(), which returns true if and only if the alarms are covered by qualified experts as noted above.
[15 marks]
Question 4 (15 marks)
These questions in this section assess skill and understanding informal verification, weakest precondition semantics and
Floyd- Hoare logic.
Use the process of postcondition hoisting to show how a verification condition is generated for the following code
fragments, expressed as Hoare Triples. Be sure to show all steps in the derivation and refer to the rules used at each step.
a) {true} Y := 3 * X; { Y > 60 } [4 marks]
b) { X = Y } X := X – 1; Y := Y – 1; { X = Y } [5 marks]
c) {true} if C > M then M := C end if { M >= C } [6 marks]