exam in discrete math

Chapter 11

Schemas

In the Z notation there are two languages: the mathematical language and the schema language. The mathematical language is used to describe various as- pects of a design: objects, and the relationships between them. The schema language is used to structure and compose descriptions: collating pieces of information, encapsulating them, and naming them for re-use.

Re-usability is vital to the successful application of a formal technique. By identifying and sharing common components, we keep our descriptions both flexible and manageable. In the schema language, we see specifications shar- ing parts, proofs sharing arguments, theories sharing abstractions, problems sharing common aspects.

We believe that the use of schemas helps to promote a good specification style. However, as with any notation, the language of schemas requires careful and judicious application if it is not to be abused. We should take care to develop simple theories and to use schemas to present them in an elegant and comprehensible fashion.

This chapter is an informal introduction to schemas: their appearance, and the information they contain. We see how they may be used as types, as declarations, and as predicates. In subsequent chapters, we present a language of schema operators, and show how schemas may be used in reasoning about formal descriptions.

11.1 The schema

The mathematical language of Z is powerful enough to describe most aspects of system behaviour. However, the unstructured application of mathematics soon results in descriptions that are difficult to understand. To avoid this, we

148 11 / Schemas

must present mathematical descriptions in a sympathetic fashion, explaining small parts in the simplest possible context, and then showing how to fit the pieces together to make the whole.

One of the most basic things that we can do to help the reader—or indeed the writer—of a specification is to identify commonly used concepts and fac- tor them out from the mathematical description of a system. In this way, we can encapsulate an important concept and give it a name, thus increasing our vocabulary—and our mental power.

In formal specifications, we see a pattern occurring over and over again: a piece of mathematical text which is a structure describing some variables whose values are constrained in some way. We call this introduction of variables under some constraint a schema.

Example 11.1 The set comprehension term, lambda expression, and quantified predicates below each exhibit this pattern of introduction and constraint:

{m,n : N | n = 2×m • m ! n}

(λ s : seq X | s ≠ ⟨⟩ • (tail s)⌢ ⟨head s⟩ )

∀ x,y : N | x ≠ y • x > y ∨ y > x

∃ z : N | z ≠ 1 • z < 2

#

Example 11.2 A concert hall uses a software system to keep track of bookings for performances. Inside the hall is a certain amount of seating, some or all of which may be made available to customers for a given performance. At this level of abstraction, we have no need to consider the representation of seats and customers, so we introduce them as given sets:

[Seat ,Customer]

The box office maintains a record of which seats have been sold, and to whom. This relationship should be functional: that is, no seat can be sold to two dif- ferent customers:

sold ∈ Seat (→ Customer To allow for the possibility that seats may be added to or removed from the hall, we introduce a set seating, a subset of Seat , to represent the seating allocated for the performance.

11.1 / The schema 149

It should not be possible to book seating that has not been allocated; the following predicate should be true at all times

dom sold ⊆ seating

That is, the domain of sold should be a subset of seating. This property, to- gether with the declarations of sold and seating, forms a schema which we shall call BoxOffice. #

A schema consists of two parts: a declaration of variables; and a predicate constraining their values. We can write the text of a schema in one of two forms: horizontally

[declaration | predicate]

or vertically

declaration

predicate

In the horizontal form, the declaration and predicate are separated by a vertical bar, and the schema text is delimited by brackets. In the vertical form, the declaration and predicate are separated by a horizontal bar, and the schema text is delimited by a broken box.

Example 11.3 We can write the box office schema in horizontal form, as

[seating : P Seat ; sold : Seat (→ Customer | dom sold ⊆ seating]

or in vertical form, as

seating : P Seat ; sold : Seat (→ Customer dom sold ⊆ seating

#

In the declaration part of a schema, the order in which variables are intro- duced is unimportant. In the above example, it would make no difference if sold were to be declared before seating.

150 11 / Schemas

The schema language includes a special operator for associating names with schemas. We may name a schema by writing

Name =̂ [declaration | predicate]

or by embedding the name in the top line of the schema box

Name declaration

predicate

In either case, we are introducing a syntactic equivalence between Name and the schema text. We may use Name to refer to this text in the remainder of a formal description.

Example 11.4 We can name the box office schema text by writing

BoxOffice =̂ [seating : P Seat ; sold : Seat (→ Customer | dom sold ⊆ seating]

or by writing

BoxOffice seating : P Seat ; sold : Seat (→ Customer dom sold ⊆ seating

#

Two schemas are equivalent if they introduce the same variables, and place the same constraints upon them. When considering equivalence, remember that some constraints may be hidden in the declaration part.

Example 11.5 The declaration part of the box office schema includes the con- straint that the relation sold between Seat and Customer must be functional. The following schema, in which this constraint appears as part of the predicate, is entirely equivalent:

seating : P Seat ; sold : Seat↔ Customer dom sold ⊆ seating ∧ sold ∈ Seat (→ Customer

#

11.1 / The schema 151

To make a schema more readable, we may put each declaration on a new line, and leave out the semicolons. Similarly, we may put each conjunct on a new line, and leave out the conjunction symbols. For example, the predicate

a ⇒ b c ∨ d

is another way of writing (a ⇒ b) ∧ (c ∨ d). Of course, this is not the case where the line is broken with another operator: for example, the predicate

∃y : T • x < y ∨ y < x

means ∃y : T • x < y ∨ y < x.

Example 11.6 The schema of Example 11.5 could be written in the following form:

seating : P Seat sold : Seat↔ Customer dom sold ⊆ seating sold ∈ Seat (→ Customer

#

If the schema text introduces components, but places no constraints upon them, then we may omit the predicate part.

Example 11.7 The following schema text has a single component, a set of seats called stalls, with no constraints:

stalls : P Seat

This is equivalent to the text

stalls : P Seat

true

#

152 11 / Schemas

11.2 Schemas as types

In our mathematical language, there are four ways of introducing a type: as a given set, as a free type, as a power set, or as a Cartesian product. If we require a composite type, one with a variety of different components, then the schema language offers a useful alternative. The schema below corresponds to a composite data type with two components: an integer called a, and a set of integers called c .

SchemaOne a : Z c : PZ

We may introduce elements of this type in the usual way: the declaration s : SchemaOne introduces an object s of schema type SchemaOne.

To write an object of schema type in extension, we list the component names and the values to which they are bound. This requires a new piece of notation:

⟨|a $ 2, c $ {1,2,3}|⟩

is a binding in which a is bound to 2 and c is bound to the set {1,2,3}. The schema type SchemaOne is the set of all bindings in which a and c are bound to an integer and a set of integers, respectively.

Example 11.8 The declaration b : BoxOffice introduces an object b with two components: a set called seating and a relation called sold . The type of b is a schema type:

[seating : P Seat ; sold : Seat↔ Customer] The schema BoxOffice appears as a subrange type; it describes only those bind- ings in which sold is a partial function, and the domain of sold is a subset of seating. #

Example 11.9 A date is an object consisting of two named components: the name of a month and the number of a day. We may define Month as a free type with twelve constants:

Month ::= jan | feb | mar | apr | may | jun | jul | aug | sep | oct | nov | dec

11.2 / Schemas as types 153

The set of all valid dates may be represented as a schema type:

Date month : Month day : 1 . . 31

month ∈ {sep,apr , jun,nov}⇒ day ≤ 30 month = feb ⇒ day ≤ 29

A binding ⟨|month $ m,day $ d|⟩ is a valid date provided that there are at least d days in month m. #

A schema type differs from a Cartesian product in that the components are stored not by position but by name. To refer to a particular component, we employ a selection operator ‘ . ’. For example, if s is an object of schema type SchemaOne, we may write s.a and s.c to denote the integer component and set component of s, respectively.

Example 11.10 In a token ring or Ethernet network, information is transmitted in the form of data frames. Each frame has a source address, a destination, and a data component. The type of all frames is a schema type:

Frame source,destination : Address data : Data

where Address is the set of all addresses in the network, and Data is the set of all possible data components. If f is an object of type Frame, then we write f .source to denote its source, f .destination to denote its destination, and f .data to denote its data component. #

Example 11.11 We may declare an object of subrange type Date to represent Fleur’s birthday:

Fleur’s birthday : Date

Following such a declaration, we may refer to name of the month in which Fleur was born as fleur’s birthday .month, and to the day on which she was born as fleur’s birthday .day . #

154 11 / Schemas

11.3 Schemas as declarations

A schema may be used whenever a declaration is expected: in a set comprehen- sion, in a lambda expression, or following a logical quantifier. The effect is to introduce the variables mentioned in the declaration part of the schema, under the constraint of the predicate part.

To illustrate this, we introduce a second schema with the same components as SchemaOne, but under some constraint:

SchemaTwo a : Z c : PZ

a ∈ c ∧ c ≠∅

This describes a subset of the bindings described by SchemaOne: number a must be an element of set c .

The following set consists of those sets of integers c that contain the integer 0:

{ SchemaTwo | a = 0 • c }

The same effect could be achieved by replacing SchemaTwo with a list of dec- larations and a constraint:

{a : Z; c : PZ | a ∈ c ∧ c ≠∅ ∧ a = 0 • c }

or by declaring an object of subrange type SchemaTwo and selecting the two components:

{ s : SchemaTwo | s.a = 0 • s.c }

The first expression, in which SchemaTwo is used as a declaration, is both more concise and more readable.

Example 11.12 If Date is the schema named in Example 11.9, then the set com- prehension

{Date | day = 31 • month }

describes the set of all months that have 31 days:

{jan,mar ,may , jul,aug,oct ,dec}

#

11.3 / Schemas as declarations 155

If a set comprehension has no term part, then the type of objects in the set depends upon the characteristic tuple of the declaration. For example, in the set

{a : Z; c : PZ | a ∈ c ∧ a = 0 }

the characteristic tuple is the pair (a, c), and the type of objects in the set is Z× PZ. The set consists of every pair (a, c) that meets the stated constraint.

In a schema, the order in which components are declared is unimportant, so the characteristic tuple of

{ SchemaTwo | a = 0 }

is quite different from (a, c). A typical element of this set is a binding associat- ing a with 0 and c with some set containing 0; the characteristic tuple has one component: the binding ⟨|a $ a, c $ c|⟩.

This is a binding in which component a is bound to the value of variable a, and component c is bound to the value of variable c :

⟨| a $ a , c︸︷︷︸ component name

$ variable value︷︸︸︷

c |⟩

Such a binding, in which each component of a schema is bound to a value of the same name, is called a characteristic binding.

If S is the name of a schema, then we write θS to denote the characteristic binding of components from S . For example,

θSchemaTwo = ⟨|a $ a, c $ c|⟩

Whenever this expression is used, variables a and c must already have been declared. Furthermore, the types of these variables must match those given in the declaration part of SchemaTwo, although any predicate information in the schema is ignored.

Example 11.13 If Date is the schema named in Example 11.9, then θDate de- notes the characteristic binding

⟨|month $ month,day $ day|⟩

Whenever this expression is used, variables month and day must be in scope, and their types must match those given in the declaration part of Date. #

156 11 / Schemas

There is a close relationship between our use of schemas as types and our use of the θ notation. As an illustration of this, consider the schema

SchemaThree a : Z c : PZ

c ≠∅ ∧ a ∈ c c ⊆ {0,1}

This introduces the same variables as SchemaOne and SchemaTwo, but under a more restrictive set of constraints.

If we use SchemaThree to describe a set of bindings, then this set will have exactly four elements:

SchemaThree = {⟨|a $ 0, c $ {0}|⟩, ⟨|a $ 0, c $ {0,1}|⟩, ⟨|a $ 1, c $ {1}|⟩, ⟨|a $ 1, c $ {0,1}|⟩}

The same set of bindings is described by the set comprehension

{a : Z; c : PZ | c ≠∅ ∧ a ∈ c ∧ c ⊆ {0,1} • ⟨|a $ a, c $ c|⟩ }

which is equal to { SchemaThree • θSchemaThree }. When a schema name is used where a set or type would be expected, we

take it to represent the corresponding set of bindings. For any schema S , the declaration a : S is an abbreviated form of

a : { S • θS }

The variable a is declared to be a binding of appropriate type that meets the constraint part of schema S . Thus we see that bindings, not schema types, are the primitive notion.

Example 11.14 When used in a variable declaration, the schema name Date rep- resents the set of all valid dates: bindings in which there are at least day days in month month. This set of bindings could also be written as a set compre- hension:

{Date • θDate }

Notice that, although θDate is the default term of this set comprehension, we include it here to avoid confusion. It is not immediately obvious that the ex- pression {Date} denotes a set comprehension. #

11.3 / Schemas as declarations 157

A schema may be used as the declaration part of a lambda expression. If SchemaOne is as defined above, then

FunctionOne == (λ SchemaOne • a2 )

introduces a function defined upon objects of schema type, mapping any bind- ing of a and c to the square of the value of a. For example,

FunctionOne ⟨|a $ 2, c $ {1,2,3}|⟩ = 4

As in Section 8.2, the source type of a lambda expression is given by the char- acteristic tuple of the declaration. In this case, the characteristic tuple has a single component: θSchemaOne.

Example 11.15 An object of schema type BoxOffice has two components: a set of seats allocated for the performance, and a record of which seats have been sold, and to whom. Given such an object, we may be interested in the set of seats that have yet to be sold. The function

free == (λBoxOffice • #(seating \ dom sold) )

maps an object of type BoxOffice to the number of unsold seats, calculated as the size of the set difference between seating and dom sold . #

A schema may be used as the declaration part of a quantified expression; this has the effect of introducing the components of the schema and then con- straining them. For example,

∃ SchemaTwo • a = 0 % ∃a : Z; c : PZ | c ≠∅ ∧ a ∈ c • a = 0

In such expressions, the order in which the components are declared is unim- portant: there are no characteristic tuples to consider.

These expressions may be used to make statements about objects of the corresponding schema type. For example, the following predicate states that, for any object of type SchemaOne, the a component must be an element of the c component:

∀ SchemaOne • a ∈ c

This predicate is false, as the binding ⟨|a $ 1, c $ {2,3}|⟩ is an object of type SchemaOne. On the other hand, the predicate

∀ SchemaTwo • a ∈ c

158 11 / Schemas

is true, as any binding of subrange type SchemaTwo must satisfy precisely this constraint.

Example 11.16 The following predicate states that there is an object of schema type Date such that the value of month is feb and the value of day is 29:

∃Date • month = feb ∧ day = 29

This is true: there can be 29 days in February. #

Example 11.17 The following predicate states that, for any object of schema type Date, the value of day must be less than or equal to 30:

∀Date • day ≤ 30

This is false, as the binding ⟨|month $ mar ,day $ 31|⟩ satisfies the predicate part of Date. March is a month with 31 days. #

Whenever a schema appears as the declaration part of a quantified expres- sion, the same result could be achieved by declaring an object of schema type. For example, the quantified predicate

∀ SchemaTwo • a ∈ c

is logically equivalent to

∀ s : SchemaTwo • s.a ∈ s.c

Both predicates insist that there is a binding of type SchemaTwo such that a is an element of c .

11.4 Schemas as predicates

A schema may be used as a predicate, provided that each component of the schema has already been declared as a variable of the correct type. The effect is to introduce a constraint equivalent to the predicate information stored in the schema. The following quantified expression states that any integer a and set of integers c satisfying the predicate SchemaThree must also satisfy the predicate SchemaTwo.

∀a : Z; c : PZ | SchemaThree • SchemaTwo

11.4 / Schemas as predicates 159

This is logically equivalent to the following statement:

∀a : Z; c : PZ | c ̸∈ ∅ ∧ a ∈ c ∧ c ⊆ {0,1} • c ̸∈ ∅ ∧ a ∈ c

The declaration parts are discarded; only the constraints remain.

Example 11.18 If A is an element of type Address, the set of all addresses within a network, then the following schema represents the set of all frames whose source address is A:

FromA source,destination : Address data : Data

source = A

Used as a predicate, this schema asserts that the value of source is A. #

When we use a schema as a predicate, we should remember that the dec- laration part may include some constraint information. At first glance, the following schema appears equivalent to SchemaTwo:

SchemaFour a : N c : PN

a ∈ c ∧ c ≠∅

but this is not the case: an additional constraint upon a and c has been imposed by the declarations a : N and c : PN.

To avoid confusion, we may choose to rewrite a schema so that all of the constraint information appears in the predicate part. This process is called normalisation; the declaration part has been reduced to a unique, canonical form. For example, the above schema may be rewritten as

SchemaFourNormalised a : Z c : PZ

a ∈ N c ∈ PN a ∈ c ∧ c ≠∅

160 11 / Schemas

It is now obvious that this schema contains strictly more information than SchemaTwo. When used as a predicate, it will insist that a, and every element of c , is greater than or equal to 0.

Example 11.19 At first glance, it might seem that any set seating of seats, and any relation sold between seats and customers, such that

dom sold ⊆ seating

would meet the constraint of schema BoxOffice. We would expect to be able to show that

∀ seating : P Seat ; sold : Seat↔ Customer • dom sold ⊆ seating ⇒ BoxOffice

However, this is not the case. The declaration part of BoxOffice includes the additional requirement that sold is a partial function. #

Example 11.20 The schema Date introduces two variables, month and day , in such a way that they correspond to a date in the Gregorian calendar. Using this schema as a predicate, we can show that

∀month : Month; day : Z • Date ⇒ day ∈ 1 . . 31

The necessary constraint upon the range of day is included in the declaration part of the schema. If we consider the normalised form of Date,

DateNormalised month : Month day : Z

day ∈ 1 . . 31 month ∈ {sep,apr , jun,nov}⇒ day ≤ 30 month = feb ⇒ day ≤ 29

then the truth of the implication becomes obvious. #

11.5 Renaming

It is sometimes useful to rename the components of a schema; in this way, we are able to introduce a different collection of variables with the same pattern

11.5 / Renaming 161

of declaration and constraint. If Schema is a schema, then we write

Schema[new/old]

to denote the schema obtained from Schema by replacing component name old with new . For example, we might wish to introduce variables q and s under the constraint of SchemaTwo: the schema

SchemaTwo[q/a, s/c]

is equivalent to the schema

q : Z s : PZ

s ≠∅ ∧ q ∈ s

The new predicate part is obtained by systematically substituting q and s for free occurrences of a and c .

Example 11.21 The variables start month and start day represent the month and the day on which a contract of employment is due to start. The requirement that this should be a valid date can be encapsulated by an appropriate renaming of the schema Date:

Date[start month/month, start day/day]

This is equivalent to the following schema:

StartDate start month : Month start day : 1 . . 31

start month ∈ {sep,apr , jun,nov}⇒ start day ≤ 30 start month = feb ⇒ start day ≤ 29

The types of the variables, and the constraints upon them, are unaffected by the renaming operation. #

Renaming the components of a schema produces a new schema type. For example, the schema type

SchemaOne[q/a, s/c]

162 11 / Schemas

consists of all bindings of q and s to values in Z and PZ. This is quite different from the schema type SchemaOne, which consists of bindings of a and c . In a schema type, component names are important.

Example 11.22 We may use another renaming to describe the set of all valid finish dates for our contract:

FinishDate =̂ Date[finish month/month,finish day/day]

A start date and a finish date are quite different objects, although each has a component of type Month and another of type Z. If s ∈ StartDate and f ∈ FinishDate, then the value of s = f is undefined: these are variables of different types. However, it still makes sense to state that

s.start day = f .finish day

as both expressions are of type Z. #

11.6 Generic schemas

Although we may rename the components of a schema, we cannot change their types. If we wish to use the same structure for a variety of different types, we may define a generic schema: a schema with one or more formal parameters. The following schema introduces two variables, a and c , under the constraint that a is an element of c :

SchemaFive[X ] a : X c : PX

a ∈ c

The types of a and c are parameterised by formal parameter X , which may be instantiated with any set.

This schema may be used whenever we wish to introduce two objects that are related in this way. If we choose Z to be the actual parameter, we obtain a schema that is equivalent to SchemaTwo:

a : Z c : PZ

a ∈ c

11.6 / Generic schemas 163

and if we choose N, we obtain a schema that is equivalent to SchemaFour .

Example 11.23 The booking system could be generalised to describe a system which monitors the sale of unspecified items to a client base.

System[Items,Client] seating : P Items sold : Items (→ Client dom sold ⊆ seating

We may obtain the familiar BoxOffice system by instantiating Items with Seat and Client with Customer .

System [Seat ,Customer] = BoxOffice

#

Chapter 12

Schema Operators

In this chapter we see how the information contained in schemas may be com- bined in a variety of different ways. We introduce a language of logical schema operators: conjunction, disjunction, negation, quantification, and composition. To illustrate the use of this language, we explain how schemas may be used to describe the behaviour of a computing system.

This application of the schema language revolves around the concept of an abstract data type: a collection of variables, and a list of operations that may change their values. We encapsulate these variables within a schema, so that an object of the corresponding schema type represents a state of the system.

An operation that affects the state can be seen as a relation upon objects of schema type: bindings of the state variables. The schema notation provides a convenient way of describing such a relation: we may use a schema to express the relationship between the state before and the state after an operation.

12.1 Conjunction

We may combine the information contained in two schemas in a variety of ways: the simplest of these is conjunction. Suppose that S and T are the schemas introduced by

S a : A b : B

P

T b : B c : C

Q

166 12 / Schema Operators

where P and Q are predicates upon the corresponding variables. We write S ∧ T to denote the conjunction of these two schemas: a new

schema formed by merging the declaration parts of S and T and conjoining their predicate parts:

a : A b : B c : C

P ∧ Q

If the same variable is declared in both schemas, as with b above, then the types must match, or the schema S ∧ T will be undefined.

The result of a schema conjunction is a schema that introduces both sets of variables and imposes both constraints. Schema conjunction allows us to specify different aspects of a specification separately, and then combine them to form a complete description. This makes for simple, well-structured descrip- tions, in which each individual component can be easily understood.

Example 12.1 Our theatre company presents premieres: special performances of new productions. Only those customers who have signed up as friends of the theatre may buy seats for these shows. To include this information in our formal description, we add a new variable of type Status:

Status ::= standard | premiere

A show may be a standard performance, or it may be a premiere. We require also a set friends, to represent the set of all customers who are currently registered as friends of the theatre.

The necessary enhancement to the box office system is described by the following schema:

Friends friends : PCustomer status : Status sold : Seat (→ Customer status = premiere ⇒ ran sold ⊆ friends

If the current performance is a premiere, then seats may be sold only to friends of the theatre.

12.1 / Conjunction 167

To describe the enhanced box office, we have only to conjoin this schema with the original:

FriendlyBoxOffice =̂ BoxOffice ∧ Friends

The same effect could have been achieved by defining:

FriendlyBoxOffice status : Status friends : PCustomer sold : Seat (→ Customer seating : P Seat

dom sold ⊆ seating status = premiere ⇒ ran sold ⊆ friends

In such a small example, there is little to be gained from the separate description of different features. In larger, more realistic examples, such a separation of concerns is essential if we are not to be overwhelmed by complexity. #

We may also conjoin two schemas by including one in the declaration part of the other. This has the same effect as schema conjunction, in that the dec- larations are merged and the predicates conjoined, but suggests a more hierar- chical structure. This is particularly useful if we wish to describe an enhanced state.

Example 12.2 The friendly box office could have been introduced by including BoxOffice in the declaration part of a schema:

FriendlyBoxOffice BoxOffice status : Status friends : PCustomer

status = premiere ⇒ ran sold ⊆ friends

or by including both BoxOffice and Friends:

FriendlyBoxOffice BoxOffice Friends

#

168 12 / Schema Operators

Example 12.3 An alternative enhancement to the box office provides a variable available, which represents the number of seats available for the current per- formance. If we take free to be the function defined in Example 11.15, then this enhancement is described by

EnhancedBoxOffice BoxOffice available : N

available = free θBoxOffice

To obtain the number of seats available, we have only to apply free to the bind- ing θBoxOffice, representing the values of seating and sold . #

12.2 Decoration

Suppose that the state of a system is modelled by a schema State with two components a and b, and that these are introduced under a constraint P .

State a : A b : B

P

Each object of schema type State represents a valid state: a binding of a and b in which predicate P is satisfied. We say that P forms part of the state invariant for the system: a constraint that must always be satisfied.

Example 12.4 The set of all valid states of our box office system is described by the schema type BoxOffice, where

BoxOffice seating : P Seat sold : Seat (→ Customer dom sold ⊆ seating

Each state is a binding of variables seating and sold ; the state invariant insists that only allocated seats are sold, and that the relationship between seats and customers remains functional. #

12.2 / Decoration 169

To describe an operation upon the state, we use two copies of State: one representing the state before the operation; the other representing the state afterwards. To distinguish between the two, we decorate the components of the second schema, adding a single prime to each name: that is,

State′

a′ : A b′ : B

P[a′/a,b′/b]

The predicate part of the schema is modified to reflect the new names of the state variables.

Example 12.5 To describe the state of the box office system after some opera- tion, we could use the following schema:

BoxOffice′

seating′ : P Seat sold′ : Seat (→ Customer dom sold′ ⊆ seating′

This introduces two variables, seating′ and sold′, corresponding to the seat seating and the sales record after the operation has been performed. #

We may describe an operation by including both State and State′ in the declaration part of a schema. For example,

Operation State State′

. . .

This is a schema with four components, two of them primed. The inclusion of State and State′ indicates that a and b constitute a valid state of the system, and that the same is true of a′ and b′.

The predicate part of such a schema characterises the operation: it de- scribes its effect upon the values of the state variables; it states what must be true of the state if the effect of the operation is to be fully defined. In the above example, we would expect the predicate part of Operation to include free occurrences of a, a′, b and b′.

170 12 / Schema Operators

Example 12.6 One operation upon the state of the box office system is the purchasing of a single seat for the current performance. Suppose that this seat is denoted by s?, and that the customer buying it is c?. If the operation is to be a success, then s? must be available for sale beforehand:

s? ∈ seating \ dom sold

Afterwards, the sold relation should be modified to indicate that s? has been sold to customer c?:

sold′ = sold ∪ {s? ! c?}

Finally, the collection of seats allocated for this performance should be un- changed by the operation.

We may encapsulate all of this information in a single schema Purchase0, representing the successful purchasing of seat s? by customer c?:

Purchase0 BoxOffice BoxOffice′

. . .

s? ∈ seating \ dom sold sold′ = sold ∪ {s? ! c?} seating′ = seating

#

Some operations, such as the one described in the example above, involve either input to the system or output from it. To model such operations, we include additional components in the declaration part of the operation schema. The predicate part can then relate the values of these components to the states before and after the operation. For example, the schema

Operation State State′

i? : I o! : O

. . .

includes an input component of type I and an output component of type O.

12.2 / Decoration 171

There is a simple convention concerning input and output. If a component represents an input, then its name should end with a query (?); if it represents output, then its name should end with a shriek (!). It should be emphasised that these are not decorations, but part of the component name.

Example 12.7 The operation of purchasing a seat requires two inputs: the name of the seat, and the name of the customer. We model these as two input components s? and c?, of types Seat and Customer , respectively. The operation of successfully purchasing a seat is described by

Purchase0 BoxOffice BoxOffice′

s? : Seat c? : Customer

s? ∈ seating \ dom sold sold′ = sold ∪ {s? ! c?} seating′ = seating

The effect of this operation is defined only when input s?, the seat requested, is available for sale. #

Example 12.8 We may add an output to our description of the purchasing op- eration, corresponding to the response offered to the customer. This response will be drawn from a free type of responses:

Response ::= okay | sorry

and may be declared in a separate schema:

Success r ! : Response

r ! = okay

The effect of a successful purchase may now be modelled as

Purchase0 ∧ Success

This produces a schema with two inputs and a single output r !, whose value will be okay . #

172 12 / Schema Operators

There is a convention for including two copies of the same schema, one of them decorated with a prime. If Schema describes the state of a system, then ∆Schema is a schema including both Schema and Schema′: that is,

∆Schema Schema Schema′

This schema could be included whenever we wish to describe an operation that may change the state.

Example 12.9 The operation schema Purchase0 could include ∆BoxOffice in place of BoxOffice and BoxOffice′:

Purchase0 ∆BoxOffice . . .

. . .

#

The inclusion of a schema name in a declaration introduces a combination of components. An important advantage of the schema notation is that it allows us to refer to this combination as a single entity. This can be done using the characteristic binding operator defined in Chapter 11.

Recall that the characteristic binding of Schema, written θSchema, is a binding in which each component of Schema is associated with the value of the variable with the same name. If Schema is included in a declaration, then we may use θSchema to refer to the combination of component values.

If the state of a system is described by schema State, then—within an op- eration schema—the binding θState corresponds to the before state. We can describe properties of this binding, apply functions to it, or even equate it to another object of the same schema type. Frequently, we will wish to equate it to the after state, thereby insisting that nothing has changed.

To do this, we use a decorated version of the same binding, rather than the characteristic binding of the decorated schema, which would have a different schema type (since the components have different names). The decorated bind- ing (θState)′ associates the components of State with the values of decorated variables. For example, if θState were ⟨|a ! a, c ! c|⟩ then θState′ would be ⟨|a ! a′, c ! c′|⟩. Note that θ binds more closely than decoration (′).

12.2 / Decoration 173

Two bindings are equal if they bind their component names to equivalent values: the two bindings above will be equal if and only if a = a′ and c = c′. Equating decorated and undecorated bindings of State is thus a way of insisting that the before state is equal to the after state: each component has been left with the same value.

Again, there is a convention: we write ΞSchema to denote the schema that includes Schema and Schema′ and equates their bindings:

ΞSchema ∆Schema

θSchema = θSchema′

This schema could be included whenever we wish to describe an operation that does not change the state of the system.

Example 12.10 We may interrogate the box office system to determine the number of seats that are still available for the current performance. This oper- ation may be described by

QueryAvailability ΞBoxOffice available! : N

available! = freeθBoxOffice

The output component available! is obtained by applying the function free to the box office state: see Example 11.15. The inclusion of ΞBoxOffice confirms that this operation leaves the state unchanged: there are no side effects. #

When we use an abstract data type to model the behaviour of a system, we should include a description of the initial state. This may be seen as the result of an operation, some form of initialisation, that does not refer to the state beforehand. The initial state of a system may be described by a decorated copy of the state schema, representing the state after initialisation.

StateInit State′

. . .

The predicate part of this schema describes the initial constraints upon the components of the state.

174 12 / Schema Operators

Example 12.11 If we assume that the initial allocation of seats for the current performance has been declared as a global variable,

initial allocation : P Seat

then the initial state of the box office system is described by the following decorated schema:

BoxOfficeInit BoxOffice′

seating′ = initial allocation sold′ =∅

In the initial state, no seats have been sold. #

12.3 Disjunction

Schema disjunction allows us to describe alternatives in the behaviour of a system. We may describe a variety of ways in which a system may evolve, and then combine them to produce a complete description. If S and T are the schemas introduced by

S a : A b : B

P

T b : B c : C

Q

then S ∨ T is the schema

a : A b : B c : C

P ∨ Q

As with conjunction, the declaration parts are merged. This time, however, the predicate parts are disjoined.

12.3 / Disjunction 175

If the same variable is declared in both schemas, as with b above, then the types must match. Any constraint information that is present in just one of the declarations should be moved into the predicate part before combination: for example, if set A in the above example is a proper subset of type T , then the constraint a ∈ A should be conjoined with P , and the declaration a : A should be replaced with a : T .

Example 12.12 If a customer attempts to purchase a seat from the box office, but the seat requested is not available, then the schema Purchase0 does not apply. To specify what happens in this case, we introduce another schema:

NotAvailable ΞBoxOffice s? : Seat

s? ̸∈ seating \ dom sold

This schema applies whenever the seat requested has not been allocated, or has already been sold. The inclusion of ΞBoxOffice confirms that the state of the system is unchanged.

To indicate that the seat could not be sold, we specify a different response for the customer:

Failure r ! : Response

r ! = sorry

We may then combine the various schemas to produce a complete description of the purchasing operation:

Purchase =̂ (Purchase0 ∧ Success) ∨ (NotAvailable ∧ Failure)

If the seat requested is available, then the effect of the operation is described by the first disjunct; if it is not, then the second disjunct applies. #

If an operation schema places no constraints upon the state of the system beforehand, then we say that the operation it describes is total. Otherwise, the operation is said to be partial.

This nomenclature corresponds exactly to the notion of partial and total functions introduced in Chapter 8. The effect of a partial operation may be

176 12 / Schema Operators

undefined for some combinations of before states and inputs; the effect of a total operation is defined for all combinations.

Example 12.13 Having purchased a seat, a customer may decide not to attend the performance. In this case, they may return the seat to the box office. The operation of successfully returning a seat is described by

Return0 ∆BoxOffice s? : Seat c? : Customer

s? ! c? ∈ sold sold′ = sold \ {s? ! c?} seating′ = seating

This is a partial operation upon the state of the box office. Its effect is defined only if the seat has been sold to the customer in question: that is, if

s? ! c? ∈ sold

If this seat has not been sold, or if it has been sold to another customer, then the schema tells us nothing about the consequences of this customer attempting to return it to the box office. The state after this attempt could be any state of the system.

To model the effect of an unsuccessful attempt, we introduce another par- tial operation schema. This will apply only if the seat has not been sold to the customer in question:

NotPossible ΞBoxOffice s? : Seat c? : Customer

s? ! c? ̸∈ sold

The inclusion of ΞBoxOffice tells us that the state of the box office system is not changed by this operation.

We may combine these partial operations using schema disjunction. The result is a total operation upon the box office state:

Return =̂ (Return0 ∧ Success) ∨ (NotPossible ∧ Failure)

12.4 / Negation 177

This describes the effect of attempting to return a seat whatever the current state of the box office. #

12.4 Negation

The negation of a schema introduces the same set of components under a negated constraint. If S is a normalised schema, then its negation ¬S may be obtained by negating the predicate part. For example, if A and B are types and S is introduced by

S a : A b : B

P

then ¬S is the schema

a : A b : B

¬P

However, this procedure applies only to normalised schemas. If the declaration part of a schema contains constraints upon the com-

ponents, then these constraints must also be negated. Consider the case of SchemaFour , a schema introduced in the previous chapter:

SchemaFour a : N c : PN

a ∈ c ∧ c ≠∅

This schema has not been normalised: the declaration part includes the con- straint that a ∈ N and c ∈ PN. The negation ¬SchemaFour has a different declaration part:

a : Z c : PZ

¬(a ∈ N ∧ c ∈ PN ∧ a ∈ c ∧ c ≠∅)

178 12 / Schema Operators

This schema is more easily recognised as the negation of the normalised form:

SchemaFourNormalised a : Z c : PZ

a ∈ N ∧ c ∈ PN ∧ a ∈ c ∧ c ≠∅

Where there is constraint information in the declaration part, it is advisable to normalise a schema before calculating its negation.

Example 12.14 The schema Date was used to characterise the set of all valid dates in the Gregorian calendar. Its negation, ¬Date, describes the set of all bindings of day and month that do not correspond to a valid date:

month : Month day : Z

day ̸∈ 1 . . 31 ∨ (month ∈ {sep,apr , jun,nov} ∧ day > 30) ∨ (month = feb ∧ day > 29)

#

Example 12.15 If the box office is no longer in the initial state, then its state may be characterised by the conjunction

BoxOffice′ ∧ (¬BoxOfficeInit)

Notice that it is not enough to simply negate the initialisation schema. The schema ¬BoxOfficeInit describes the set of all bindings of seating and sold that do not match the initial state: this includes bindings that are not valid states of the system. #

12.5 Quantification and hiding

We may quantify over some of the components of a schema while retaining the declarations of the others. If Q is a quantifier and dec is a declaration, then the quantified schema

Qdec • Schema

12.5 / Quantification and hiding 179

may be obtained from Schema by removing those components that are also declared in dec and quantifying them with Q in the predicate part. For this schema to be properly defined, every variable declared in dec must appear in Schema as a component of the same type.

For example, if S is the schema with components a and b of types A and B, introduced under the constraint P ,

S a : A b : B

P

then ∀b : B • S is the schema

a : A

∀b : B • P

and ∃b : B • S is the schema

a : A

∃b : B • P

Example 12.16 The friendly box office records the status of the current perfor- mance: if the show is a premiere, then seats are sold only to customers who are registered friends of the theatre:

FriendlyBoxOffice status : Status friends : PCustomer sold : Seat (→ Customer seating : P Seat

dom sold ⊆ seating status = premiere ⇒ ran sold ⊆ friends

If we precede this schema with a universal quantification of the variable status, then we obtain a schema that no longer records the status of the current perfor- mance. The result is not the same as if this component had never been present:

180 12 / Schema Operators

the system behaves as if it is still there, universally quantified, in the predicate part of the schema.

To see why, consider the quantified schema:

∀ status : Status • FriendlyBoxOffice

The predicate part insists that

∀ status : Status • dom sold ⊆ seating status = premiere ⇒ ran sold ⊆ friends

If this quantified expression is to be an invariant of the system, then tickets may be sold only to friends of the theatre, for else the subexpression status = premiere ⇒ ran sold ⊆ friends would be false for one of the values of status.

The quantification over status has produced a cautious version of the box office system:

CautiousBoxOffice friends : PCustomer sold : Seat (→ Customer seating : P Seat

dom sold ⊆ seating ran sold ⊆ friends

It is as if the universal quantification over status has forced the system to take a pessimistic view as to the status of the performance: it caters for both possibilities—standard and premiere—by selling only to friends. #

Example 12.17 The operation of successfully returning a ticket to the box office required the name of a customer. We may dispense with this requirement by existentially quantifying over the input component c?. The result is an anony- mous version of the return operation:

∃ c? : Customer • Return0

The predicate part of the new schema states that

∃ c? : Customer • s? ! c? ∈ sold ∧ sold′ = sold \ {s? ! c?} ∧ seating′ = seating

12.5 / Quantification and hiding 181

With care, we may rewrite this predicate to make the results of the operation more obvious:

∆BoxOffice s? : Seat r ! : Response

∃ c? : Customer • s? ! c? ∈ sold ∧ sold′ = sold \ {s? ! c?} ∧ seating′ = seating

It is as if the existential quantification has forced the system to take an opti- mistic view as to the identity of the customer. By the one-point rule and the properties of functions, this schema is equivalent to

AnonymousReturn0 ∆BoxOffice s? : Seat r ! : Response

s? ∈ dom sold sold′ = {s?}−▹ sold seating′ = seating

For this operation to be properly defined, it is necessary only that the input s? is an element of the domain of sold . #

Schema existential quantification is also called hiding: the quantified com- ponents are no longer visible in the declaration, yet the predicate tells us that they exist. This provides a powerful mechanism for abstraction in the schema language: we may hide any components that are not required at the current level of specification.

This mechanism has its own operator: if list is a list of component names, then the schema Schema\ list may be obtained by existentially quantifying each component in list within Schema. For example, if S is the schema introduced by

S a : A b : B

P

182 12 / Schema Operators

then S \(a) is the schema

b : B

∃a : A • P

Thus hiding is no more than a quick way of writing (and pronouncing) existential quantification over schema components.

Example 12.18 The enhanced box office system included a component that recorded the number of seats available for the current performance. We may abstract away this information by hiding available within the schema:

EnhancedBoxOffice \ (available)

The result is a schema with the same components as BoxOffice:

BoxOffice

∃available : N • available = free θBoxOffice

Since free is a total function, the number of seats available is always uniquely determined by the values of seating and sold . This schema is equivalent to the original box office description. #

12.6 Composition

The use of schemas to describe operations begs an interesting question: how does one describe the effect of one operation followed by another? Alterna- tively, we might ask: if an operation schema characterises a relation between states of the system, then how does one represent the composition of two such relations? The answer in both cases is schema composition.

If OpOne and OpTwo are operation schemas, each including primed and unprimed copies of a state schema State, then the composition OpOne o9 OpTwo describes the change in state that results when operation OpOne is followed by operation OpTwo.

In OpOne, the components of State′ represent the state of the system im- mediately after the operation. In the composition above, this is also the state of the system immediately before OpTwo. We introduce a new schema to rep- resent this intermediate state: State′′.

12.6 / Composition 183

The schema composition relates the state immediately before OpOne to the state immediately after OpTwo, and State′′ is hidden:

OpOne o9 OpTwo = ∃ State′′ • ∃ State′ • [OpOne; State′′ | θState′ = θState′′] ∧ ∃ State • [OpTwo; State′′ | θState = θState′′]

The relationship between the before state and the intermediate state—θState and θState′′—is described by schema OpOne; the relationship between the intermediate state and the after state—θState′′ and θState′—is described by schema OpTwo.

For the composition to be defined, both schemas must refer to the same state. For any primed component in OpOne, there must be an unprimed com- ponent of the same name in OpTwo. For example, suppose that OpOne and OpTwo are introduced by

OpOne a,a′ : A b,b′ : B

P

OpTwo a,a′ : A b,b′ : B

Q

The state components in each operation are the same, so their schema compo- sition will be well defined.

The composition of OpOne and OpTwo may be calculated using schema existential quantification, as above, or by renaming the state components cor- responding to the intermediate state:

OpOne o9 OpTwo = (OpOne[a′′/a′,b′′/b′] ∧ OpTwo[a′′/a,b′′/b]) \ (a′′,b′′)

The components representing the intermediate state, a′′ and b′′ are then hid- den. If we were to expand this schema, we would see that the composition is equivalent to:

a,a′ : A b,b′ : B

∃a′′,b′′ • P[a′′/a′,b′′/b′] ∧ Q [a′′/a,b′′/b]

184 12 / Schema Operators

Example 12.19 If a customer successfully purchases a seat, and then returns it immediately to the box office, then the state of the system should be unaffected. The combined operation is described by

Purchase0 o9 Return

where Purchase0 and Return are as defined above. The result that we might hope to establish can be expressed as

Purchase0 o9 Return ΞBoxOffice

This is an inference in which the composition is used as a declaration: intro- ducing a collection of components under the stated constraint. The schema ΞBoxOffice is used only as a predicate. #

Chapter 13

Promotion

In this chapter we describe an important technique for structuring formal de- scriptions. It is called promotion, and it allows us to compose and factor spec- ifications. It has also been called framing, because it is evocative of placing a frame around part of a specification: only what is inside the frame may change; what is outside must remain unaffected.

We begin the chapter with three different examples of the technique: a game, a mail system, and a data array. We then give a formal definition of promotion, and distinguish between two varieties: free and constrained. The chapter ends with two further examples of promotion: a free promotion of a booking system, and a constrained promotion within a priority stack.

13.1 Factoring operations

Large software systems often contain multiple, indexed instances of the same component. A database may contain a number of records, a computer system may have several users, a data network may consist of a number of switching nodes. If this is the case, then there will exist a uniform relationship between the system state and the state of each indexed component.

This relationship allows us to link certain changes in system state to changes in the state of indexed components. We may factor a global operation into a local operation and a mixed operation, the latter expressing the relationship between local and global state. This is a useful separation of concerns; the two factors may be specified and analysed in isolation. We have used the structur- ing information in the design of the system to simplify our formal description.

186 13 / Promotion

global score

local score

Figure 13.1 A game in progress

Example 13.1 In the game of Trivial PursuitTM, the players collect tokens of various colours—red, green, yellow, blue, brown, and pink—the aim being to collect one token of each colour. There are no teams: each player maintains an individual score. A player’s score may be modelled using a schema type

LocalScore s : PColour

where Colour is the set of colours mentioned above. The overall state of play at any point during the game is given by a binding

of the following schema type:

GlobalScore score : Players (→ LocalScore

Here, a partial function called score associates each player with an object of type LocalScore. Figure 13.1 shows a situation in which one of the players has collected exactly two tokens.

13.1 / Factoring operations 187

Players are awarded tokens if and when they provide correct answers to questions on various subjects; the colour awarded depends upon the choice of subject. If a player p? earns a token of colour c?, then the effect upon the state of play is described by the following operation schema:

AnswerGlobal ∆GlobalScore p? : Player c? : Colour

p? ∈ dom score {p?}−▹ score′ = {p?}−▹ score (score′ p?).s = (score p?).s ∪ {c?}

Provided that p? is indeed part of the current game, the function score is up- dated to reflect the new score associated with p?.

An alternative approach would involve factoring this operation into a local operation—

AnswerLocal ∆LocalScore c? : Colour

s′ = s ∪ {c?}

—and a schema expressing the relationship between global and local states—

Promote ∆GlobalScore ∆LocalScore p? : Player

p? ∈ dom score θLocalScore = score p? score′ = score⊕ {p? ! θLocalScore′}

—in which a change in GlobalScore and a change in LocalScore are linked by the identity of the player involved.

If we conjoin the AnswerLocal and Promote schemas, then we obtain a schema that describes an operation upon the global state:

∃∆LocalScore • AnswerLocal ∧ Promote

188 13 / Promotion

The local state is uniquely determined by the function score, so there is no need to record this information at the global level. The existential quantification hides it, yielding a predicate part

∃∆LocalScore • p? ∈ dom score θLocalScore = score p? score′ = score⊕ {p? ! θLocalScore′} s′ = s ∪ {c?}

We may rewrite this as

∃ s, s′ : PColour • p? ∈ dom score ⟨|s $ s|⟩ = score p? score′ = score⊕ {p? ! ⟨|s $ s′|⟩} s′ = s ∪ {c?}

and hence as

∃ s : PColour • p? ∈ dom score (score p?).s = s score′ = score⊕ {p? ! ⟨|s $ s ∪ {c?}|⟩}

to obtain a schema equivalent to AnswerGlobal :

∆GlobalScore p? : Player c? : Colour

p? ∈ dom score {p?}−▹ score′ = {p?}−▹ score (score′ p?).s = (score p?).s ∪ {c?}

#

In the above example, there is little to choose between the two approaches, although the factored description makes it easier to see the effect of the op- eration upon the local state. However, as we define more operations, and add more information to the local state, the advantages of the factored approach become obvious.

13.1 / Factoring operations 189

The relationship between the global state and the collection of local states need not be functional. There may be several components with the same index, in which case the association between indices and components can be modelled as a relation.

Example 13.2 An electronic mail system consists of several instances of the component MailBox. Each instance may be associated with one or more ad- dresses from the set Address. A user of the system may have more than one address, and an address may be associated with more than one user.

MailSystem address : User↔Address mailbox : Address (→MailBox

The association between users and addresses is given by a relation address, and the association between addresses and mailboxes is given by the partial function mailbox.

Figure 13.2 shows a mail system with three users: Carolyn, Denise, and Edward. Each user has a personal mailbox, with an appropriate address. Car- olyn and Denise share ownership of the system administrator’s mailbox with address admin. Edward has two mail addresses, edward and edwardc , each with its own mailbox.

A mailbox is modelled by a schema type with three components. The first is a sequence of type Message, representing the mail messages stored in the box. The others are time stamps:

MailBox mail : seq Message new mail, last read : TimeStamp

Of these, new mail records the time of arrival of the latest mail message, and last read records the last time that mail in the box was read.

A typical object of type MailBox might be

⟨|mail $ ⟨m1,m2,m3⟩ , , new mail $ Tue 14 Feb, 11.00 a.m. , last read $ Sun 12 Feb, 12.30 p.m. |⟩

This tells us that the box holds three messages—m1, m2, and m3—the last of which arrived at 11.00 a.m. on Tuesday 14th February. It states also that mail in this box was last read at 12.30 p.m. on Sunday 12th February.

190 13 / Promotion

AddressUser Mailbox

address mailbox

Denise

Carolyn

Edward

denise

admin

edwardc

carolyn

edward

Figure 13.2 Addresses and mailboxes

If a message m? arrives at time t? for user u?, then it will be added to one of the mailboxes belonging to u?. These components are taken as inputs to the following operation schema, which describes the effect upon the global state:

ReceiveSystem ∆MailSystem u? : User m? : Message t? : TimeStamp a! : Address

u? ! a! ∈ address address′ = address a! ∈ dom mailbox {a!}−▹mailbox′ = {a!}−▹mailbox (mailbox′ a!).mail = (mailbox a!).mail ⌢ ⟨m?⟩ (mailbox′ a!).new mail = t? (mailbox′ a!).last read = (mailbox a!).last read

The address used, a!, is provided as an output to the operation. The value of address and the contents of the other mailboxes—given by {a!}−▹mailbox—are left unchanged.

13.1 / Factoring operations 191

Again, we may choose an alternative approach, factoring global operations such as ReceiveSystem into two parts. The first part, which is the same for each operation, expresses the link between local and global changes of state:

Promote ∆MailSystem ∆MailBox u? : User a! : Address

u? ! a! ∈ address address′ = address a! ∈ dom mailbox θMailBox = mailbox a! mailbox′ = mailbox ⊕ {a! ! θMailBox′}

The link is made by identifying the user u? and the address a! involved in the operation. The local state is given by mailbox a!, where u? ! a! is an element of the address relation. This is the only part of the global state that will change; this is the frame in which the operation will take place.

The second part of the factorisation is a schema that describes the effect of adding mail to a single mailbox:

ReceiveBox ∆MailBox m? : Message t? : TimeStamp

mail′ = mail ⌢ ⟨m?⟩ new mail′ = t? last read′ = last read

The incoming message is added to the end of the sequence mail , and the new mail is set to t?. The other time stamp remains unchanged.

If we conjoin these two schemas, and abstract away the components of the local state, as in

∃∆MailBox • ReceiveBox ∧ Promote

then we obtain a schema that is logically equivalent to the global operation ReceiveSystem. #

192 13 / Promotion

value

value

local state

global state

Figure 13.3 A data array

In some systems, the components may be indexed sequentially; in this case, the relationship between the global and local states may be based upon a se- quence, rather than a simple function or relation.

Example 13.3 In a model of a data array, each element may be represented by an object of schema type Data, where

Data value : Value

The state of the array is represented by an object of schema type with a single component, a sequence of Data elements:

Array array : seq Data

The relationship between the state of the array—the global state—and the state of a data element—the local state—is illustrated in Figure 13.3.

If an operation upon the array affects but a single element, then we may express it as the product of two schemas: a local operation schema and a pro- motion schema. For example, the operation of assigning a new value to a data element could be described as

∃∆Data • AssignData ∧ Promote

13.2 / Promotion 193

where the local operation schema is introduced by

AssignData ∆Data new? : Value

value′ = new?

and the promotion schema, which makes the link between global and local states using the index of the data, is introduced by

Promote ∆Array ∆Data index? : N

index? ∈ dom array {index?}−▹ array = {index?}−▹ array ′ array index? = θData array ′ index? = θData′

Once again, the promotion schema describes the frame, while the local opera- tion schema describes the effect. #

13.2 Promotion

When a global operation is defined in terms of a local operation upon an indexed component, as in each of the examples above, we say that the local operation has been promoted. Formally, suppose that we have

• a state schema Local , that describes a copy of the local state; • a state schema Global , that describes a copy of the global state; • a local operation schema LocalOperation, that contains decorated and un-

decorated copies of the state schema Local ;

• a promotion schema Promote, that contains decorated and undecorated copies of both Local and Global .

Then the promotion schema promotes the local operation to

∃∆Local • Promote ∧ LocalOperation

which operates on the global state Global .

194 13 / Promotion

Example 13.4 A global box office system keeps track of bookings for a number of performances. The record of seats allocated and tickets sold for each per- formance is represented by an object of schema type BoxOffice. These objects are indexed by a function on Performance, the set of all possible performances:

GlobalBoxOffice announced : PPerformance booking : Performance (→ BoxOffice dom booking ⊆ announced

As well as booking, the system maintains a set called announced for reference purposes. The two components are connected: any performance for which we are booking must have been announced. On the other hand, some performances may have been announced but have not yet started booking.

A booking operation is an operation upon the global box office system that involves the sale or return of a seat. These operations may be factored using promotion. We define a promotion schema:

Promote ∆GlobalBoxOffice ∆BoxOffice p? : Performance

p? ∈ dom booking θBoxOffice = booking p? θBoxOffice′ = booking′ p? {p?}−▹ booking′ = {p?}−▹ booking announced′ = announced

This tells us the relationship between the local state of a box office system and the global state in such an operation, given that we are talking about perfor- mance p?. Such local operations do not affect the list of performances that have been announced.

We may promote the local operation of buying a ticket to a global operation simply by conjoining the schema above with Purchase:

GlobalPurchase0 =̂ ∃∆BoxOffice • Purchase ∧ Promote

A single box office has changed—the one identified by input p?—and the effect of this change is described by the operation schema Purchase.

13.2 / Promotion 195

The promotion schema identifies input p? with a unique performance; if we expand GlobalPurchase0, then the existential quantification can be eliminated. The result is a schema equivalent to the following:

∆GlobalBoxOffice p? : Performance s? : Seat c? : Customer r ! : Response

p? ∈ dom booking ( ( s? ∈ booking p?.seating \ dom booking p?.sold ∧

booking p?.sold′ = booking p?.sold ∪ {s? ! c?} ∧ r ! = okay) ∨ ( s? ̸∈ booking p?.seating \ dom booking p?.sold ∧

booking p?.sold′ = booking p?.sold ∧ r ! = sorry ) )

{p?}−▹ booking′ = {p?}−▹ booking announced′ = announced

Even where the indexing relation is functional, the advantages of structuring our descriptions using promotion should be obvious. #

Of course, the promotion schema is used only in factoring operations which may be described in terms of their effect within an indexed frame. Other oper- ations upon the global state will not be factorised in this way.

Example 13.5 The GlobalPurchase0 operation defined above is not total: it de- scribes only those situations in which the performance in question is already booking. We may wish to add the following alternative:

NotYetBooking ΞGlobalBoxOffice p? : Performance r ! : Response

p? ∈ announced \ dom booking r ! = not yet booking

This describes the situation in which—although the performance in question has been announced—the office is not accepting bookings. #

196 13 / Promotion

Example 13.6 We may instruct the box office system to start accepting book- ings for a performance p?:

StartBooking ∆GlobalBoxOffice p? : Performance

p? ∈ announced p? ̸∈ dom booking announced′ = announced ∃BoxOfficeInit •

booking′ = booking ∪ {p? ! θBoxOffice′}

A performance cannot start booking unless it has been announced; neither can it start booking more than once. #

13.3 Free and constrained promotion

A promotion is said to be free if and only if the promotion schema satisfies

(∃Local′ • ∃Global′ • Promote) ⇒ (∀Local′ • ∃Global′ • Promote)

That is, provided that the update is possible at all, it is possible for all outcomes of the local state.

In a free promotion, neither the promotion schema nor the global state invariant should place any additional constraint upon the component variables of the local state: that is, any constraint above that provided by the local state schema itself. Then, and only then, can the quantifiers be exchanged.

To decide whether a given promotion is free, we expand ∃Global′ • Promote and simplify the predicate part of the resulting schema. We should be left with an expression in which θLocal appears unconstrained, other than by the predicate part of Local iself.

The exchange of quantifiers can then be justified using schema equivalents of the quantifier rules. The rule required for existential elimination is

∃ S • B

⌈s ∈ S⌉[i] ⌈B[s/θS]⌉[i] ...

C

C [∃−elim[i]]

provided that s is not free in either the other assumptions or C

13.3 / Free and constrained promotion 197

and the rule for universal introduction is

⌈s ∈ S⌉[i] ...

B[s/θS] ∀ S • B [∀−intro

[i]] provided that s is not free in the other assumptions

Notice how the decoration mechanism gives us a way of generating instances of the appropriate schema type in such a way that we are able to distinguish between them at component level: the components in S ′ are associated with variables that differ from those of S .

Example 13.7 The data array description of Example 13.3 is an example of a free promotion. The schema ∃Data′ • ∃Array ′ • Promote asserts that the index chosen as input is a valid index for the array—index? ∈ dom array—and does not constrain the value stored at that index, apart from identifying it as array index?. The promotion is thus independent of the actual value stored at the index; provided that the index is valid, the promotion will work: it is free.

To see this in terms of the implication that was used to characterise a free promotion, we consider the expression ∃Data′ • ∃Array ′ • Promote. That is, there is at least one local after-state with a global after-state satisfying the promotion condition.

Consider the inner existential quantification: that beginning with ∃Array ′. Replacing the Promote schema with the body of its definition, and moving the existential quantification of Array ′ into the predicate part of the resulting schema, we see that

∃Array ′ • Promote % [Array ; ∆Data; index? : N |

∃Array ′ • index? ∈ dom array array index? = θData array ′ = array ⊕ {index? ! θData′}]

% [Array ; ∆Data; index? : N | ∃array ′ : seq Data •

index? ∈ dom array array index? = θData array ′ = array ⊕ {index? ! θData′}]

198 13 / Promotion

Simplifying the predicate part using the one-point rule to eliminate the quan- tification of array ′, we obtain

∃Array ′ • Promote % [Array ; ∆Data; index? : N |

index? ∈ dom array array index? = θData array ⊕ {index? ! θData′} ∈ seq Data]

Given that index? ∈ dom array , the last of these conditions requires only that θData′ ∈ Data. Thus

∃Array ′ • Promote % [Array ; ∆Data; index? : N |

index? ∈ dom array array index? = θData θData′ ∈ Data]

The predicate above places no constraint on θData′, other than the requirement that it meets the constraint of Data. It is then a simple matter to show that

∃Data′ • ∃Array ′ • Promote ⇒ ∀Data′ • ∃Array ′ • Promote

using the rules for existential elimination and universal introduction. #

A promotion that is not free is said to be constrained. In general, con- strained promotions are not as elegant: they lack the modularity that freeness implies. However, there are situations in which a constrained promotion is the natural solution.

Example 13.8 We wish to model a stack of data objects, each of which contains a piece of data and a priority value:

PriData priority : N data : Data

The objects in the stack are ordered with respect to their priority values. If object a has a lower index than object b—if it is nearer the top of the stack— then it must have a higher priority value:

13.3 / Free and constrained promotion 199

Stack stack : seq PriData

∀ i, j : dom stack | i < j • (stack i).priority ≥ (stack j).priority

At any time, only the data object with the highest priority may be operated upon: that is, the object at the head of the stack. Our promotion schema includes this condition:

Promote ∆Stack ∆PriData

stack ≠ ⟨⟩ θPriData = head stack stack′ = ⟨θPriData′⟩⌢ tail stack

The constraint of the promotion schema states that the stack must be non- empty, and that any change is made to the object at the head of the sequence.

In this description, the global state invariant refers to a component of the indexed local state: the priority value. In an arbitrary operation, there may be local after-states which violate the global state invariant. Consider the case in which the stack contains two objects:

stack = ⟨⟨|priority $ 3,data $ a|⟩, ⟨|priority $ 2,data $ b|⟩⟩

In an operation, the state of the first object may change to

⟨|priority $ 3,data $ c|⟩

so at least one after-state exists, but after-states such as

⟨|priority $ 1,data $ c|⟩

are disallowed. Hence

∃PriData′ • ∃ Stack′ • Promote ̸⇒ ∀PriData′ • ∃ Stack′ • Promote

and the promotion is constrained. Having observed this, we might decide to strengthen the predicate part of Promote in the hope of achieving a free pro- motion, or we may decide that the existing promotion is an entirely suitable description of our system. #

Chapter 14

Preconditions

The construction of an abstract data type presents two important proof op- portunities. The first involves a demonstration that the various requirements upon the data type are consistent and not contradictory. The second involves a demonstration that each operation is never applied outside its domain, in a situation for which the results of the operation are not defined.

If the language of schemas is used to construct the data type, then these opportunities present themselves as simple mathematical tasks. To show that the requirements are consistent, we have only to show that the constraint part of the state schema is satisfiable. This is usually achieved by proving an initial- isation theorem: we show that an initial state, at least, exists.

To show that the operations are never applied outside their domain, we must investigate their preconditions. These may be calculated from the opera- tion schemas using the one-point rule. In this chapter, we explain the procedure for calculating preconditions, and show how it may be simplified by the use of structuring techniques such as promotion.

14.1 The initialisation theorem

In the previous chapters we have seen how the behaviour of a system may be described in terms of an abstract data type. The state of the system was modelled as an object of schema type, the predicate part of which represented a state invariant: a list of requirements that should be true in any valid state.

Clearly, if this includes a contradiction, then the data type description is vacuous: it is impossible to fulfil the requirements, therefore no state exists. To check that this is not the case, and that our specification is of some use, it is enough to establish that at least one state exists.

202 14 / Preconditions

If the description is to be useful, then there must also exist an initial state. As we saw in Example 12.11, this is usually characterised by a decorated schema, representing the state after initialisation. This is an obvious candidate for our proof of consistency.

Suppose that State describes the state of the system, and that StateInit characterises the initial state. If we can prove that

∃ State′ • StateInit

then we have shown that an initial state exists, and hence also that the re- quirements upon the state components are consistent. This result is called the initialisation theorem for the data type.

Example 14.1 In the case of the box office system, the initial state was charac- terised by

BoxOfficeInit BoxOffice′

seating′ = initial allocation sold′ =∅

The initialisation theorem is therefore

∃BoxOffice′ • BoxOfficeInit

#

The initialisation theorem is an easy one to prove, unless there are compli- cated initial conditions. Most often, the initial state is described uniquely with a number of equations, so the proof strategy is simple: eliminate the quantified variables. Once this has been done, the truth of the predicate should follow immediately from the properties of the mathematical objects involved.

Example 14.2 In the case of the box office, we may proceed as follows:

∃BoxOffice′ • BoxOfficeInit % ∃BoxOffice′ •

[BoxOffice′ | seating′ = initial allocation ∧ sold′ =∅]

[definition of BoxOfficeInit ]

14.2 / Precondition investigation 203

% ∃BoxOffice′ • seating′ = initial allocation ∧ sold′ =∅

[schema quantification]

% ∃ seating′ : P Seat • ∃ sold′ : Seat (→ Customer •

dom sold′ ⊆ seating′ ∧ seating′ = initial allocation ∧ sold′ =∅

[definition of BoxOffice′]

% initial allocation ∈ P Seat ∧ ∅ ∈ Seat (→ Customer

[one-point rule, twice]

The proof may be completed by recalling the axiomatic definition of constant initial allocation, which is indeed of type P Seat , and expanding the definition of the generic symbol (→. #

14.2 Precondition investigation

The precondition of an operation schema describes the set of states for which the outcome of the operation is properly defined. If Operation is an operation schema, then we write

pre Operation

to denote the precondition of Operation. This is another schema, and is ob- tained from Operation by hiding any components that correspond to the state after the operation, and any outputs that happen to be present.

If the state of the system in question is modelled by a schema State, and outputs is the list of outputs associated with the operation, then the following equation defines the precondition schema:

pre Operation = ∃ State′ • Operation \ outputs

This schema characterises the collection of before states and inputs for which some after state can be shown to exist.

Example 14.3 The precondition of the operation schema Purchase0, which de- scribes the effect of a successful purchase, is given by

pre Purchase0 = ∃BoxOffice′ • Purchase0 [definition of pre ]

204 14 / Preconditions

= [BoxOffice; s? : Seat ; c? : Customer | ∃ seating′ : P Seat ;

sold′ : Seat (→ Customer | dom sold′ ⊆ seating′ •

s? ∈ seating \ dom sold sold′ = sold ∪ {s? ! c?} seating′ = seating]

[definition of BoxOffice′]

= [BoxOffice; s? : Seat ; c? : Customer | dom(sold ∪ {s? ! c?} ⊆ seating ∧

s? ∈ seating \ dom sold]

[one-point rule, twice]

= [BoxOffice; s? : Seat ; c? : Customer • s? ∈ seating \ dom sold]

[property of ‘dom’]

The predicate part of Purchase0 identifies an after-state that satisfies the state invariant only if the chosen seat s? has been allocated and not sold. The effect of Purchase0 is defined only when

s? ∈ seating \ dom sold

Notice that the actual precondition includes additional declaration and con- straint information. The effect of the operation is properly defined only if the initial values of seating and sold satisfy the constraint of BoxOffice and s? is an element of Seat . #

In many cases, the precondition for an operation may be obvious to the writer of the specification. For example, the precondition of Purchase0—see the above example—was sufficiently obvious to be included in the operation schema. In general, we might wish to concentrate upon what the operation is supposed to do, and calculate the precondition later. In the specification process, such cross-checking can be useful.

Example 14.4 A simple control system monitors the entry and exit of vehicles from a car park. It maintains a count of the number of vehicles presently inside; this count should never exceed capacity , an integer number greater than zero:

CarPark count : N

count ≤ capacity

We may define an operation Exit0 that describes the successful departure of a car from the parking area:

14.2 / Precondition investigation 205

Exit0 ∆CarPark

count ′ = count − 1

It might seem that this schema would apply to all states of the system, in that we are not placing any explicit constraint upon count . However,

pre Exit0 = ∃CarPark′ • Exit0 [definition of Exit0] = [CarPark | ∃ count ′ : N |

count ′ ≤ capacity • count ′ = count − 1] [definition of CarPark′]

= [CarPark | count − 1 ∈ N] [one-point rule]

Because of the state invariant, this operation should be restricted to those states in which the count variable is strictly greater than 0. The effect upon other states is undefined. By calculating the precondition, we have identified a pos- sible source of error.

To see why Exit0 alone might be an unsatisfactory description of the exit operation, suppose that there is a way for cars to enter the car park unobserved. In this case, the function that implements the exit operation may be called while the value of count is 0. The subsequent value of count , according to Exit0, conflicts with our choice of data representation: anything could happen.

Now that the problem has been detected, we may choose to totalise the operation using a second schema to describe the effect of a car leaving when the system believes that the car park is empty:

ExtraCar ΞCarPark r ! : Report

count = 0 r ! = extra car

Assuming that a suitable type of reports is introduced, we may define

Exit =̂ Exit0 ∨ ExtraCar

and be sure that all of the possibilities are catered for. #

206 14 / Preconditions

14.3 Calculation and simplification

The process of calculating preconditions is both straightforward and routine. Indeed, much of the hard work can be carried out using some form of theo- rem prover or mechanical proof assistant. Suppose that we wish to find the precondition of the following operation schema:

Operation Declaration

Predicate

where Declaration represents the declaration part of Operation, and Predicate the predicate part. To calculate the precondition of Operation,

1. divide Declaration into three parts:

• Before containing only inputs and before components (unprimed state components)

• After containing only outputs and after components (primed state components)

• Mixed containing all other declarations and inclusions

2. if Mixed is not empty, expand every schema mentioned in Mixed ; add all input and before components to Before; add all output and after components to After . As there may be several levels of schema inclusion, repeat this step until Mixed is empty.

3. the precondition of Operation is then

Before

∃After • Predicate

Example 14.5 To see how this recipe for preconditions may be applied, con- sider the following state schema definitions:

14.3 / Calculation and simplification 207

S a : N b : N

a ≠ b

T S c : N

b ≠ c

and suppose that we wish to calculate the precondition of the following oper- ation schema:

Increment ∆T in? : N out ! : N

a′ = a + in? b′ = b c′ = c out ! = c

The first step of our recipe requires that we divide the declaration part of the schema into three parts:

Before = {‘in? : N’}

After = {‘out ! : N’}

Mixed = {‘∆T ’}

The second step requires us to empty the third part, Mixed , by expanding schema definitions and separating input, output, before and after components. The result is

Before = {‘in? : N’, ‘T ’}

After = {‘out ! : N’, ‘T ′’}

Mixed = {}

The precondition of Increment is then given by

208 14 / Preconditions

T in? : N

∃out ! : N; T ′ • a′ = a + in? b′ = b c′ = c out ! = c

#

As we can see from the last example, the precondition schema obtained after the third stage of the recipe may be quite complicated. It is usually possi- ble to simplify the predicate part of a precondition schema using the one-point rule. For a precondition schema

Before

∃After • Predicate

we may proceed as follows:

4. expand any schemas in After that contain equations identifying outputs or after components

5. expand any schemas in After that refer to outputs or after components for which we already have equations

6. if Predicate contains an equation identifying a component declared in After , then use the one-point rule to eliminate that component; repeat this step as many times as possible

7. if After1 and Predicate1 are what remains of After and Predicate, then the precondition is now

Before

∃After1 • Predicate1

14.3 / Calculation and simplification 209

Example 14.6 The precondition of Increment , calculated in the last example, can be greatly simplified using the remaining part of the recipe. Its predicate part is currently

∃out ! : N; T ′ • a′ = a + in? b′ = b c′ = c out ! = c

Looking at Step 5 of the recipe, we expand T ′, as it contains a declaration of an after component for which we have an equation:

∃out ! : N; S ′; c′ : N | b′ ≠ c′ • a′ = a + in? b′ = b c′ = c out ! = c

The same is true of S ′, so we follow this step again:

∃out ! : N; a′ : N; b′ : N; c′ : N | a′ ≠ b′ ∧ b′ ≠ c′ • a′ = a + in? b′ = b c′ = c out ! = c

There are no more schemas to expand, so we proceed to Step 6. The one-point rule can be applied four times, yielding the predicate

a + in? ≠ b b ≠ c a + in? ∈ N b ∈ N c ∈ N

This is as far as the recipe takes us. However, all but one of these conjuncts follow immediately from the declarations in the precondition schema:

in? : N T

210 14 / Preconditions

Removing the redundant information from our predicate, we obtain the final simplified form of ‘pre Increment ’:

in? : N T

a + in? ≠ b

#

14.4 Structure and preconditions

The process of calculating preconditions can be further simplified by consid- ering the structure of an operation. If an operation schema is defined to be the disjunction of several partial operations, or if an operation is defined using promotion, then we may be able to save time and effort by factoring out part of the calculation.

The simplest case is that of disjunction. If an operation schema Op is defined to be the disjunction of two or more operation schemas, then we may make use of the fact that the precondition operator ‘pre’ distributes through disjunction. For example, if

Op =̂ Op1 ∨ Op2

then we may conclude that

pre Op = pre Op1 ∨ pre Op2

This result follows immediately from the definition of ‘pre’, given the following theorem of our predicate calculus:

∃A • P ∨ Q % ∃A • P ∨ ∃A • Q

Existential quantification distributes through disjunction.

Example 14.7 The Purchase operation was defined as a disjunction of two par- tial operations

Purchase =̂ (Purchase0 ∧ Success) ∨ (NotAvailable ∧ Failure)

14.4 / Structure and preconditions 211

Using the distributive property of ‘pre’, we may observe that

pre Purchase = pre (Purchase0 ∧ Success) ∨ pre (NotAvailable ∧ Failure)

We may calculate the preconditions of the two partial operations—Purchase0 ∧ Success and NotAvailable ∧ Failure—separately, and combine them to obtain the precondition of Purchase. #

The ‘pre’ operator does not necessarily distribute through conjunction. If Op =̂ Op1 ∧ Op2 then pre Op may not be equivalent to pre Op1 ∧ pre Op2. However, this will be the case whenever one of the schemas contributes nothing to the precondition.

Example 14.8 In Example 12.8, the schema Success was defined to be

Success r ! : Response

r ! = okay

This schema imposes no constraint upon the before components of the box of- fice state, neither does it describe any input. It therefore makes no contribution to the precondition of an operation, and we may observe that

pre (Purchase0 ∧ Success) = pre Purchase0

#

If an operation is defined using a free promotion, then its precondition may be expressed in terms of the precondition of a local operation. If Promote is a free promotion, then the equivalence

∃Local′ • ∃Global′ • Promote % ∀Local′ • ∃Global′ • Promote (∗)

must hold; this follows from the definition at the start of Section 13.3. Now consider the precondition of GOp, the promotion of a local operation LOp:

pre GOp

% ∃Global′ • GOp [definition of ‘pre’] % ∃Global′ • ∃∆Local • Promote ∧ LOp [definition of GOp] % ∃∆Local • ∃Global′ • Promote ∧ LOp [property of ∃]

212 14 / Preconditions

% ∃∆Local • (∃Global′ • Promote) ∧ LOp [Global′ does not appear in LOp]

% ∃Local • (∃Local′; Global′ • Promote) ∧ ∃Local′ • LOp [free promotion]

% ∃Local • pre Promote ∧ pre LOp [definition of ‘pre’, twice]

The equivalence justified by the phrase ‘free promotion’ can be derived from the equivalence labelled ‘∗’ using the proof rules for existential introduction and universal elimination.

The result that we have established can be stated as follows: under a free promotion, the precondition of a global operation is a conjunction of two preconditions—the precondition of the local operation, and the precondition of the promotion. We might say that the precondition of the local operation has itself been promoted.

Example 14.9 The description of a data array in Example 13.3 included a global operation AssignIndex defined by

AssignIndex =̂ ∃∆Data • AssignData ∧ Promote

This is a free promotion, so the precondition of AssignIndex is given by

pre AssignIndex = ∃Data • pre Promote ∧ pre AssignData

The local operation AssignData is total: the constraint part of pre AssignData is simply true precondition. The promotion schema Promote was defined by

Promote ∆Array ∆Data index? : N

index? ∈ dom array {index?}−▹ array = {index?}−▹ array ′ array index? = θData array ′ index? = θData′

The precondition of Promote adds the constraint index? ∈ dom array . The precondition of AssignIndex is therefore

14.4 / Structure and preconditions 213

Array new? : N index? : N

index? ∈ dom array

#

The separation of concerns afforded by the free promotion is not possible where the promotion is constrained. In such cases, the precondition of a pro- moted operation is calculated by first conjoining the local operation and the promotion schema and then applying the existential quantifier.

Example 14.10 In the prioritised data stack of Example 13.8, we propose a local operation that sets the priority of the top element to 100:

SetPriority ∆PriData

priority ′ = 100 data′ = data

We may promote this operation to the global operation

SetPriorityStack =̂ ∃∆PriData • SetPriority ∧ Promote

where the promotion schema Promote is defined by

Promote ∆Stack ∆PriData

stack ≠ ⟨⟩ θPriData = head stack stack′ = ⟨θPriData′⟩⌢ tail stack

This insists that the stack is non-empty. We may calculate the precondition of SetPriorityStack as follows:

pre SetPriorityStack

% ∃ Stack′ • SetPriorityStack [definition of ‘pre’] % ∃ Stack′ • ∃∆PriData • Promote ∧ SetPriority

214 14 / Preconditions

[definition of SetPriorityStack]

% ∃∆PriData • ∃ Stack′ • Promote ∧ SetPriority [property of ∃] % ∃∆PriData • (∃ Stack′ • Promote) ∧ SetPriority

[Stack′ does not appear in SetPriority]

At this point, we calculate the value of ∃ Stack′ • Promote, and obtain

Stack ∆PriData

stack ≠ ⟨⟩ θPriData = head stack ∀ j : dom tail stack • θPriData′.priority ≥ (stack j).priority

In conjunction with SetPriority , this yields

Stack ∆PriData

stack ≠ ⟨⟩ θPriData = head stack θPriData′.priority = 100 θPriData′.data = θPriData.data ∀ j : dom tail stack • θPriData′.priority ≥ (stack j).priority

Following on from the argument above, we may obtain the precondition of SetPriorityStack by quantifying this schema with ∃∆PriData, yielding

Stack

stack ≠ ⟨⟩ ∀ j : dom tail stack • 100 ≥ (stack j).priority

For the operation to be defined: the stack must be non-empty; every priority value in the tail of the stack must be less than 100; the stack must be ordered according to decreasing priority values.

A very different result would be obtained by factoring the precondition calculation as if it were a free promotion. The constraint part of pre SetPriority is simply true: there is no restriction at the level of the data objects. The schema

∃PriData′ • pre Promote ∧ pre SetPriority

14.4 / Structure and preconditions 215

is equivalent to

Stack

stack ≠ ⟨⟩

This schema that omits an essential part of the precondition: the constraint that every object in the tail of the stack has a priority lower than 100.

The missing constraint appears when we combine the information from the local operation—that the new priority value is 100—with the invariant property of the global state. If we hide the new priority value before combining the two schemas, then this information is lost. #

Any investigation of the initialisation and preconditions of a specification should be properly recorded. A useful convention, followed by many practi- tioners, involves tabulating the results of the investigation. In such a table, we may find related partial operations listed together: any overall precondition is then easily established.

Example 14.11 In our theatre box office system, the constraint part of the ini- tialisation schema is simply true. No initial input is required: the initial value of seating is simply that of some global variable initial allocation.

The Purchase and Return operations were both total. Each is the disjunc- tion of two partial operations, Purchase being defined by

Purchase =̂ (Purchase0 ∧ Success) ∨ (NotAvailable ∧ Failure)

and Return by

Return =̂ (Return0 ∧ Success) ∨ (NotPossible ∧ Failure)

Each total operation involves two inputs—s? and c?—and a single output—r !. Having calculated the preconditions, we may collect the results together in a single table: see Table 14.1. #

216 14 / Preconditions

Operation Precondition

BoxOfficeInit true

Purchase0 s? ∈ seating \ dom sold NotAvailable s? ̸∈ seating \ dom sold

Success true

Purchase true

Return0 s? ! c? ∈ sold NotPossible s? ! c? ̸∈ sold

Failure true

Return true

Table 14.1 Preconditions in the box office system

Assignment on Z.html

You are asked to specify a car rental system. There are three categories of cars: small, medium and large. Cars can be rented to persons who when renting a car automatically become members. For each category, cars are rented on a first-in first-out basis: when a car is returned, it is placed at the end of a queue.

1. Specify the system and the initial state.

2. Specify a rental operation, with as input a person and a category, and as output a car. Make sure the operation is robust and use schema compo- sition. If a person wants to rent in a category where no car is available, he returns home emptyhanded but is still made a member.

3. Specify an operation where a person returns a car. The operation does not need to be robust. Give the precondition of the operation.

4. Specify an operation with as input a category, and as output all the persons that have rented a car in this category.