Determination

acm-rtre-b

Definition 69 – Determination: By domain determination we understand an operation that applies to a (projected) domain description, i.e., a requirements prescription, and yields a domain requirements prescription, where the latter has made deterministic, or specific, some function results or some behaviours of the former

s737

tt1-dd

Example 83 – Timetable System Determination: We make airline timetables more specific,

tt0-dd

more deterministic. There are given notions of departure and arrival times, and of airports, and of airline flight numbers.

s739 A timetable consists of a number of air flight journey entries. Each entry has a flight number, and a list of two or more airport visits. an airport visit consists of three parts: An airport name, and a pair of (gate) arrival and departure times.

We illustrate just one, simple form of airline timetable queries. A simple airline timetable query either just browses all of an airline timetable, or inquires of the journey of a specific flight. The simple browse

s741

query thus need not provide specific argument data, whereas the flight journey query needs to provide a flight number. A simple update query inserts a new pairing of a flight number and a journey to the timetable, whereas a delete query need just provide the number of the flight to be deleted.

s742

The result of a query is a value: the specific journey inquired, or the entire timetable browsed. The result of an update is a possible timetable change and either an “OK” response if the update could be made, or a “Not OK” response if the update could not be made: Either the flight number of the journey to be inserted was already present in the timetable, or the flight number of the journey to be deleted was not present in the timetable.

s743

That is, we assume above that simple airline timetable queries only designate simple flights, with one aircraft. For more complex air flights, with stopovers and changes of flights, see Sect. 86 on page 149.

You may skip the rest of the example, its formalisation, if your reading of this paper does not include the various formalisations. First, we formalise the syntactic and the semantic types:

schemeTI TBL 3Q= extendTI TBL 3with

class type

Query ==mk brow()|mk jour(fn:Fn)

Update ==mk inst(fn:Fn,jr:JR)| mk delt(fn:Fn) VAL=TT

RES==ok|not ok end

Then we define the semantics of the query commands:

s744

schemeTI TBL 3U= extendTI TBL 3with

class

8.6 Domain Requirements 147 value

M^q: Query→QU M^q(qu)≡

casequ of

mk brow()→λtt:TT^•tt, mk jour(fn)

→λtt:TT^• if fn∈domtt

then[fn7→tt(fn)]else [ ]end end end

And, finally, we define the semantics of the update commands: s745

schemeTI TBL 3U= extendTI TBL 3with

class

M^u: Update→UP M^u(up)≡

case quof

mk inst(fn,jr)→λtt:TT^• if fn∈domtt

then(tt,not ok)else (tt∪[fn7→jr],ok)end, mk delt(fn)→λtt:TT^•

if fn∈domtt

then(tt\ {fn},ok)else(tt,not ok)end end end

We can “assemble” the above into the timetable function — calling the new function the timetable

system, or just the system function. ^s746

Before we had:

value

tim tbl 0: TT→Unit tim tbl 0(tt)≡

(letv=client 0(tt)intim tbl 0(tt)end)

⌈⌉(let (tt^′,r)=staff 0(tt)intim tbl 0(tt^′)end) Now we get:

value

system: TT→Unit system()≡

(letq:Query in letv=M^q(q)(tt)insystem(tt)end end)

⌈⌉(let u:Updatein let (r,tt^′)=M^u(q)(tt)insystem(tt^′)end end) Or, for use in Example 99: s747

system(tt)≡client(tt)⌈⌉staff(tt) client: TT→Unit

client(tt)≡

letq:Query in letv=M^q(q)(tt)insystem(tt)end end staff: TT→Unit

staff(tt) ≡

letu:Updatein let (r,tt^′)=M^u(q)(tt)insystem(tt^′)end end

We remind the reader that the above example can be fully understood by just reading the rough-sketch texts, that is, without reading their formalisations.

This ends Example 83

s748

acm-rtre-b arms-determination

Example 84 – Determination: A Road Maintenance System: We continue Example 81.We shall, in this example, claim that the following items constitute issues of more determinate nature of the ‘Road Management System’ under development. fixing the states of links and hubs; endowing links and hubs with such attributes as road surface material (concrete, asphalt, etc.), state of road surface wear-and-tear, hub and link areas, say inm², time units needed for and cost of ordinary cleaning of m²s of hub and link surface; time units needed for and cost of ordinary repairs ofm²s of hub and link surface; etcetera.

s749

18. The two links of a road segment are open for traffic in one direction and in opposite directions only.

19. Hubs are always in the same state, namely one that allows traffic from incoming links to continue onto all outgoing links.

20. Hubs and Links have a number of attributes that allow for the monitoring and planning of hub and link surface conditions, i.e., whether in ordinary or urgent need of cleaning and/or repair.

s750

20 Surface, WearTear, Area, OrdTime, OrdCost, RepTime, RepCost,...

value

Example 85 –Determination: A Toll-road System: We continue Example 82. We single out only two ’determinations’:The link state spaces. There is only one link state: the set of all paths through the link, thus any link state space is the singleton set of its only link state.The hub state spaces are the singleton sets of the “current” hub states which allow these crossings: (i) from terminal link back to terminal link, (ii) from terminal link to emanating tollway link, (iii) from incident tollway link to terminal link, and (iv) from incident tollway link to emanating tollway link. Special provision must be made for expressing the entering from the outside and leaving toll plazas to the outside.

s752

8.6 Domain Requirements 149

∀j:Nat^•{j,j+1,j+2}⊆indshll⇒

let(,(hj,ljj,lj^′j))=hll(j),((thj^′,tlj^′),(hj^′,ljj^′,lj^′j^′))=hll(j+1)in wf Plaza(thj^′,tlj^′,hj^′)∧wf Interm(ljj,lj^′j,hj^′,tlj^′,ljj^′,lj^′j^′)end end wf Plaza(th,tl,h) ≡

obs HΣ(th)= [crossings at toll plazas] {(external,obs HI(th),obs LI(tl)),

(obs LI(tl),obs HI(th),external), (obs LI(tl),obs HI(th),obs LI(tl))} ∧ obs HΩ(th)={obs HΣ(th)} ∧

obs LΩ(tl)={obs LΣ(tl)}

s753

wf End(h,tl,l,l^′)≡

obs HΣ(h) = [crossings at 3−link end hubs]

{(obs LI(tl),obs HI(h),obs LI(tl)),(obs LI(tl),obs HI(h),obs LI(l)), (obs LI(l^′),obs HI(h),obs LI(tl)),(obs LI(l^′),obs HI(h),obs LI(l))} ∧ obs HΩ(h) ={obs HΣ(h)} ∧

obs LΩ(l)={obs LΣ(l)} ∧obs LΩ(l^′)={obs LΣ(l^′)} wf Interm(ul 1,dl 1,h,tl,ul,dl)≡

obs HΣ(h) ={[crossings at properly intermediate, 5−link hubs]

(obs LI(tl),obs HI(h),obs LI(tl)),(obs LI(tl),obs HI(h),obs LI(dl 1)), (obs LI(tl),obs HI(h),obs LI(ul)),(obs LI(ul 1),obs HI(h),obs LI(tl)), (obs LI(ul 1),obs HI(h),obs LI(ul)),(obs LI(ul 1),obs HI(h),obs LI(dl 1)), (obs LI(dl),obs HI(h),obs LI(tl)),(obs LI(dl),obs HI(h),obs LI(dl 1)), (obs LI(dl),obs HI(h),obs LI(ul))} ∧

obs HΩ(h)={obs HΣ(h)} ∧obs LΩ(tl)={obs LΣ(tl)} ∧ obs LΩ(ul)={obs LΣ(ul)} ∧ obs LΩ(dl)={obs LΣ(dl)}

Not all determinism issues above have been fully explained. But for now we should — in principle —

be satisfied. This ends Example 85

In document From Domains to Requirements The Triptych Approach to Software Engineering (Sider 168-172)