联系方式

  • QQ:99515681
  • 邮箱:99515681@qq.com
  • 工作时间:8:00-23:00
  • 微信:codinghelp

您当前位置:首页 >> Python编程Python编程

日期:2020-08-07 10:04

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

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]


版权所有:留学生编程辅导网 2020 All Rights Reserved 联系方式:QQ:99515681 微信:codinghelp 电子信箱:99515681@qq.com
免责声明:本站部分内容从网络整理而来,只供参考!如有版权问题可联系本站删除。 站长地图

python代写
微信客服:codinghelp