Read the following report and then answer both the
questions which follow it.
Your company has been awarded a contract to design software
to control the movement and storage of containers on cargo
ships. To improve understanding of the requirements for the
software, a model in VDM-SL has been partially developed.
The excerpt from the model shown below focuses on the
storage of containers on a ship. The ship must remain balanced
at all times. On the ship, containers are placed in one of two
equally sized cargo decks (the front, or fore, deck, and the
back, or aft, deck). The state variable maxSize gives the
capacity of each deck, and the state variable tolerance will
be used in assessing whether the ship is balanced.
state Ship of
fore : Deck
aft: Deck
maxSize: nat
tolerance: nat
inv mk_Ship(fore,aft,maxSize,tolerance)==
len fore <= maxSize and
len aft <= maxSize and
elems fore inter elems aft = {}
end;
types
Container :: id : token
weight: nat;
Deck = seq of Container;
Each Deck is a sequence of containers, identified by the id
field. The need for balance affects the way in which containers can be loaded and unloaded, which requires us to know the
weight of individual containers.
Question 1
a) In examining the model, a colleague suggests that it will be
necessary to ensure that each Deck has uniquely identified
containers (i.e. no 2 containers in a Deck have the same
identifier).
Suggest an invariant to be defined on the Deck datatype to
record this restriction.
[10 marks]
b) A ship is balanced if the difference between the total
weights of containers in the fore and aft decks is less
than a specified tolerance value. This tolerance value
varies between ships and is represented by a state
variable, tolerance. An auxiliary function, Balanced, is
used to show whether the ship is balanced:
Balanced: Deck * Deck * nat -> bool
Balanced(fore, aft, tolerance) ==
abs(TotalWeight(fore) –
TotalWeight(aft)) <= tolerance
The operator abs is used to calculate the absolute
(positive) value of an expression.
i) Complete the following function definition for the
function TotalWeight, to calculate the total weight of
the full sequence of containers on a deck.
TotalWeight: Deck -> nat
TotalWeight(d) == ??
ii) Show how the state invariant can be modified, making
use of the Balanced function, to capture the
requirement that the ship is balanced at all times.
[5 marks]
c) The behaviour to load a container to a Ship will be
described using an implicit operation. The new container
will be loaded onto either the fore or aft deck, ensuring
that the ship is balanced. Describe in plain, concise English
the conditions that need to be expressed in the
postcondition (and any precondition) of the implicit
operation.
[20 marks]
Question 2
a) Explain the limitations of testing which verification by proof
of correctness is intended to overcome.
[15 marks]
b) Briefly explain the proof obligations that must be satisfied
by a valid data refinement.
[15 marks]
c) Development of the ship system now proceeds by data
refinement. The datatype Deck is currently represented as
a sequence of containers. A developer suggests that this
type could be represented as a set of containers:
NewDeck = set of Container
with the Container datatype defined as before. The
proposed retrieve function,
retr-Deck: NewDeck -> Deck
would create a sequence in ascending order of the weights
of the containers.
Explain why NewDeck is not a valid data refinement of
Deck.
[20 marks]