Concrete applicative harbour - The RAISE Development Method

A natural concrete type to use forHarbour is the product of a set of waiting ships and a map from indices of berths to their occupancy.

Extending TYPES

We could then model the type Berth as equal to the subtype of integers from mintomax, but it is more general to leaveBerthas a sort and say there is a function indx fromBerth to this subtype: eectively the index of a berth is an attribute of it. We then leave open the possibility of other attributes. Presumably there will need to be some others (and some attributes of ships) to enable us to eventually computets.

We therefore add the following denitions to the type module TYPES:

type

Index =^fji :

Int

imin^{^}maxi^jg

value

min, max :

Int

, indx : Berth^!Index

axiom

[index not empty] maxmin, [berths indexable]

8b1, b2 : Berth indx(b1) = indx(b2)⁾b1 = b2

The axiomberths indexableensures that indexes identify berths uniquely.

Note that we choose just to add these denitions to the type module directly rather than develop it to a new module TYPES1, say. This is the most convenient way to develop type modules. As here, the extensions to them are typically con-servative and making formal developments of them would be more eort than is appropriate.

Developing the system module

From the abstract applicative module A HARBOUR0 we develop a concrete ap-plicative moduleA HARBOUR1by the following method:

Give a concrete denition for the type of interest.

Give explicit denitions of constants and functions.

Remove axioms.

This gives the concrete applicative module A HARBOUR1:

scheme

A HARBOUR1 =

class

type

Harbour = T^:Ship

-set

fjbs : T^:Index ^!_m T^:Occupancy (⁸ idx : T^:Index idx²

dom

bs)

value

=generators⁼

arrives : T^:ShipHarbour^! Harbour

arrives(s^;(ws^;bs))(ws ^[^fs^{g ;}bs)

pre

can arrive(s^;(ws^;bs))^; docks : T^:ShipT^:BerthHarbour^! Harbour

docks(s^;b^; (ws^;bs))

(ws ⁿ^fs^g;bs ^y[T^:indx(b)^7!T^:occupied by(s)])

pre

can dock(s^; b^;(ws^;bs))^;

leaves : T^:ShipT^:BerthHarbour^! Harbour leaves(s^; b^;(ws^;bs))

(ws^;bs^y [T^:indx(b)^7!T^:vacant])

pre

can leave(s^;b^;(ws^;bs))^;

=observers ⁼

waiting : T^:ShipHarbour^!

Bool

waiting(s^;(ws^;bs))s²ws^;

occupancy : T^:BerthHarbour^!T^:Occupancy occupancy(b^; (ws^;bs))bs(T^:indx(b))^;

=invariant⁼

consistent : Harbour ^!

Bool

consistent((ws^; bs)) (

8 s : T^:Ship

(waiting(s^;(ws^;bs))^{^}is docked(s^;(ws^; bs))) ^{^} (

8b1^;b2 : T^:Berth

occupancy(b1^;(ws^; bs)) = T^:occupied by(s)^{^} occupancy(b2^;(ws^; bs)) = T^:occupied by(s)⁾ b1 = b2

)^{^} (

8b : T^:Berth

occupancy(b^;(ws^;bs)) = T^:occupied by(s)⁾T^:ts(s^; b) )^; )

is docked : T^:ShipHarbour^!

Bool

is docked(s^;(ws^; bs))

(⁹b : T^:Berthoccupancy(b^; (ws^; bs)) = T^:occupied by(s))^;

=guards⁼

can arrive : T^:Ship Harbour^!

Bool

can arrive(s^;(ws^;bs))

waiting(s^;(ws^;bs))^{^}is docked(s^; (ws^;bs))^; can dock : T^:ShipT^:BerthHarbour^!

Bool

can dock(s^;b^; (ws^;bs)) waiting(s^;(ws^; bs))^{^}

is docked(s^;(ws^;bs))^{^}

occupancy(b^; (ws^;bs)) = T^:vacant^{^}T^:ts(s^; b)^; can leave : T^:ShipT^:BerthHarbour^!

Bool

can leave(s^; b^;(ws^; bs))occupancy(b^; (ws^;bs)) = T^:occupied by(s)

end

3.7.1 Verication

We formulate the development relation A HARBOUR0 1, which asserts that A -HARBOUR1 implements A HARBOUR0:

development relation

[A HARBOUR0 1] A HARBOUR1A HARBOUR0 A development relation is a named statement of a relation between modules. This one takes the most simple form of the statement of an implementation relation () between two versions of the harbour module.

Justication of this relation shows that the development step is correct. We use a justication editor to rst check the static implementation relation and to generate implementation conditions to be proved (cf. section 2.2). In this case (and typically) the implementation conditions are the axioms from the abstract specication, A HARBOUR0. Each of the implementationconditions has as context the more concrete specication, A HARBOUR1.

For instance, we get from the axiomwaiting arrivesthe implementation condi-tion

8h : Harbour, s1, s2 : T.Ship

waiting(s2, arrives(s1, h))s1 = s2 ^_waiting(s2, h)

pre

can arrive(s1, h) The justication of this condition is done by a series of steps in which RSL proof rules are applied transforming the condition to new conditions whose truth ensure the truth of the original condition. The conditions, also calledgoals, are enclosed by the brackets and , and the names of the applied proof rules are written between the goals.

An example of a proof rule is [is annihilation]

e e ^'

true

It has the nameis annihilationand states that any value expression of the forme eis equivalent to

true

. This rule can be used in a proof to replace a value expression eewith

true

or vice versa. In the handbook [7] there is a collection of proof rules for RSL. From the denitions and axioms in the context of a justication additional proof rules can be derived. These rules are calledcontext rules. The context of the condition above, A HARBOUR1, gives, for example, unfold rules for functions with dened bodies. For instance

[waiting def]

waiting(s, (ws, bs))^'s²ws A justication of the condition is

8h : Harbour, s1, s2 : T.Ship

waiting(s2, arrives(s1, h)) s1 = s2^_waiting(s2, h)

pre

can arrive(s1, h) all name change :

8(ws, bs) : Harbour, s1, s2 : T.Ship

waiting(s2, arrives(s1, (ws, bs)))s1 = s2^_waiting(s2, (ws, bs))

pre

can arrive(s1, (ws, bs)) all assumption inf :

waiting(s2, arrives(s1, (ws, bs)))s1 = s2^_waiting(s2, (ws, bs))

pre

can arrive(s1, (ws, bs)) pre deduction inf :

[assump] can arrive(s1, (ws, bs))^`

waiting(s2, arrives(s1, (ws, bs)))s1 = s2^_waiting(s2, (ws, bs)) arrives def :

waiting(s2, (ws^[^fs1^g, bs))s1 = s2 ^_waiting(s2, (ws, bs))

since

can arrive(s1, (ws, bs)) assump :

qed true

waiting def :

end

s2²ws^[^fs1^gs1 = s2^_waiting(s2, (ws, bs)) waiting def :

s2²ws^[^fs1^gs1 = s2^_s2²ws isin union :

s2²ws^_s2²^fs1^gs1 = s2^_s2 ²ws isin singleton :

s2²ws^_s2 = s1s1 = s2^_s2²ws or commutativity :

s2 = s1^_s2² wss1 = s2^_s2²ws is annihilation :

qed true

In the rst step we rename the binding to match better the context rules like waiting def. In the second step we assume we have a xed but arbitrary harbour (ws, bs) and xed but arbitrary ships s1 and s2. In the third step we remove the precondition from the equivalence and instead assume that it is true. We give the assumption the name assumpso that we can refer to it later in the proof. In the fourth step we unfold the application of the function arrives(remembering we are in the context of A HARBOUR1). This gives a new goal with the application replaced with the body of the function denition, with actual parameters replacing the formal ones. As the function has a precondition it also gives a side condition (can arrive(s1, (ws, bs))) which expresses that the precondition is satised. The proof of the side condition is placed between the keywords

since

and

end

. The side condition is proved using the assumptionassump. In the fth and sixth steps we unfold the applications of the functionwaiting. In the next steps we use various

proofrules for sets, and nally, in the last step, we apply the rule is annihilationby which the proof is completed.

In document The RAISE Development Method (Sider 13-17)