Disclaimer. CSUSB and the CS Dept have no responsibility for the content of this page.
Copyright. Richard J. Botting ( Fri May 12 15:34:05 PDT 2006 ). Permission is granted to quote and use this document as long as the source is acknowledged.
There are archival copies at [ rjb9Xa.lift.html ] [ rjb9Xa.lift.mth ] (raw) and [ rjb92a.lift ]
Notation This document was prepared using my [ MATHS in research ] notation. This notation can be converted into other text formats including HTML. So far there is a prototype mth2html program.
In the raw form (a *.mth file) the document starts out as a list
of "bulleted" headlines.
Headers have a '.' in the first column. Sections start with .Open and end
with .Close.
Introduction
I plan to show how simple mathematics - sets, mappings, relations,
definitions, assertions, etc. can define a formal language for software
specification and design. The language models a particular domain. I
will be using as an example an elevator control system. Several
conferences, papers, and methodologists have used the problem of designing
a controller for a set of elevators to demonstrate and/or test various
methods. A variety of plausible specifications and designs have been
presented. See
[Jackson83],
[Wing87],
[Chang89],
[Milietal89], and many
others. Implementation steps have also been covered
[Botting87], for
example JSD+ADA in
[YeungTopping90].
Notes on notation and the process of formal analysis will be prefixed by 'Note: topic'.
The sample problem is called the "Lift Problem" in the literature. I first met it in a prototype Jackson System Development(JSD) course in England when the British Civil Service College was in the process of selecting a standard method of analysis and design in 1979-81. I started it afresh in the summer of 1985 using Telos's "Filevision"( visual data base. I demonstrated the result at the international workshop on software specification and design in September 1985. In the summer of 1987 I reworked the model and transcribed it into regular expressions. I published the result as part of the papers for the 1987 workshop. In 1989, on sabbatical, I removed some complications and presented it at EXPOSIM'89 at the Monterey Institute of Technology in Mexico(ITESM), Torreon, Coah., Mexico.. This presentation developed from a chapter in a monograph on a notation for organizing documentation that has mathematics in it. This was revised in April 1993. The notation was modernized in 1998. This latest revision started in December 2004.
My goal is to show how to develop a mathematical model of a situation as a basis for formal requirements, specifications, designs, and implementations. The key idea is not solving non-problems, and not assuming things that are false. My approach is to establish a semi-formal language for talking about the domain and its problems. Once this in place we can discuss ways of solving any problems and so ways to implement the solutions.
But at any time a number of facts are true. But these change every now an then. For example, at one time:
There are also "facts" relating to what people want:
Expressing Facts Mathematically
The elevators, floors and buttons must be documented because they appear in the
description of the problem. Further,
they are names of things that (1) are outside
the controller, (2) interact with the controller, and (3) are individually
identifiable by the controller. The goal is to define as many of the
words in the description of the problem as possible. People may be the
reason for the existence of elevators, but a typical elevator control
system cannot distinguish them or control them so they are left undefined.
We have a finite sets of elevators, floors and buttons. Let the set of floors be called F. Let n be the number of floors. Let E represent the set of elevators. Let m be the number of elevators. Let B represent the set of buttons.
In MATHS the above paragraph is documented like this:
Note: Declarations and Definitions The above statements have declarations (with a two colons ) and definitions (with the BNF two colons and an equals sign). A declaration defines a symbol as a member of a set without giving it any particular value. A definition makes a symbol stand for something else. Mathematical variables are introduced as abbreviations for words taken from the problem. B, E, F represent sets and may ultimately be implemented as entity types, abstract data types, or classes of objects.
Note: Abbreviations Much of the power of mathematics comes from the use of short symbols in place of complex words and ideas. This lets them be written, read, and thought quickly. Add some rules to manipulated them and you get the power of algebra. However, the symbology of mathematics introduces an initial bump in the road for people who have not used the notation before. It is wise to say things in both long and short form, and then add a diagram.
We also record all assumptions (axioms) that we make. If we think about
buildings and elevators we can be certain that there is at least one
elevator, and at least two floors. In symbols we have axiom or assumption
e1:
Axioms The sign in front of the above formula is short for "It is asserted that". It is placed in front of formulas that are taken to be true in the remainder the current context. In the above case e1 is assumed throughout this document. The assertion symbol comes from [WhiteheadRussell66]. It is also used in Ina Jo [WingNixon89]. In Maths it is also used to indicate proved results or theorems as well as formula that are assumed.
Special Kinds of Button
There are two distinct types of button - floor selection buttons inside
elevators and the call elevator buttons on the floors outside the
elevators.
Note: Subsets The "@" means "set of" (\power-set ). The above states that G and H are special kinds of buttons (B). This is close to the idea of inheritance or generalization used by object-oriented people.
Note: Verbalizations It is helpful to associate a name with a phrase. The above descriptions show one way of doing it. In raw MATHS I use reversed quotes:
`...`to indicate statements in other languages than mathematics. This gives a natural language translation of the term. These strings allow us to write designations relating our symbols to the things that they symbolize. They help people understand what the mathematics means.
Now a button is either inside an elevator, or outside.
Of course, a button
can not be both inside (G) and outside(H) an elevator.
So buttons(B) are
partitioned into those inside(G) and those outside elevators (H). I show
that B
is partitioned into G and H like this:
Buttons outside elevators have up and down on them.
The buttons outside the elevator ( H ) are labeled with one of two
directions. Here is the mathematical definition:
The above properties and definitions let use prove
Note: Notation for reasoning In the above line you are shown the reasons for the truth of the statement:
(list of reasons)|-(label): consequence.It states that the formula can be derived from listed formulas. The proof may be included in a document, (click the assertion symbol to see if a proof is attached) or be omitted depending on the audience and the risks of errors. It can be as formal as we like, and can be at any level of abstraction. The formal rules are documented elsewhere.
Up and Down Buttons
Up and Down are not floors, and so are not in F:
Labels on buttons
When we look at a button outside an elevator we see a label reading either
Up or Down. Inside an elevator the labels on the buttons identify
floors.
Each Button has its own label, so there is a function l that takes each button b in B into a unique label in L. We write the label on b as l(b). We call l a function, map, or mapping:
Here are some properties we can derive from the definition of l:
Note: Many to one functions
The set of all maps from A to B is shown as A->B. A is called the
domain (dom) and B the co-domain (cod). Both
l(b) and b.l show the result of applying
the function l to element b.
I think of the application process as filling in the holes in
an expression.
I indicate a "hole" like this: "(_)".
There is also a version of the lambda notation:
Note: Maps Functions like l are also called maps and mappings. They are total many-to-one relations. They describe the structure of the problem domain and are used to document requirements and specifications. Functions are often implemented as the operations in abstract data types and/or methods of objects. Functions can also become navigation paths through a data base or set of data structures. Thus maps and sets define the structure shared by the solution and the problem's environment.
Note: Overloading
I also overload maps so that they also to apply to sets, so:
Properties of labels on buttons
We can state the following axioms:
Note: inverse functions
I use the '/' symbol to reverse the direction of a map or relation.
If a function f maps from A->B then /f maps subsets and elements in B
into subsets of A. In general:
"Labeled"
For example:
We can prove properties of buttons - for example a button outside a lift has
either an Up or a Down on it, not a floor's name:
Relationships
The map l is equivalent to a relation between buttons and labels. If we
decompose l into a relation between H and D, plus a relation between
G and F then we discoverer that there are n-1 Up buttons and
n-1 Down buttons. Further each floor appears as a label on exactly m
buttons (one per elevator):
Systems Analysis by Stating the Obvious
Formal analysis proceeds primarily by stating the obvious. For example,
each floor button is on one floor and each button in an elevator is in one
elevator. This is an example of a common type of relationship - `is a part
of`. Here is the formal documentation of 'P', the relation between an
object and the object to which it is attached:
We assume that each part is in (or on) one other object:
After examining some elevators we add the following
properties of 'parts of` (/P)
and 'labeled'(/l) as assumed (or defining) properties:
Note: (n)-(m) Relations Expressions like A(n)-(m)B represent sets of relations - those that link 1 A with m Bs and 1 B to n As. Bachman designed a diagram for documenting collections of sets and relations [Bachman69]. There are several varieties [Chen80], [MartinMcClure85], [Wiederhold77], [WardMellor85]. The UML notation unifies these concepts with object-oriented modelling. For systems and requirements analysis I use only the simplest form - a Conceptual Model [SSADM circa 1980] or Conceptual Structure [Carasiketal90]. Boxes represent sets and lines show mappings (=attributes). The boxes are placed so that the mappings run from lower boxes to higher ones - this makes the diagrams easier to read [MartinMcClure85]. Symbols at the bottom of a line show the range of sizes of inverse images under the map - this is used to validate the model[SSADM]. .UML Net{f:A(n..m)-(1)B}. .UML Net{f:A(n)-(1)B}.
A binary relation R is equivalent to a set of pairs X (in @(A><B)) and an n-ary one to a set of n-tuples. Many-many relations are shown as sets of objects plus maps - a restriction that starts to 'normalize' the model [Codd70] and [Codd82]. Now a relation is in A(n)-(m)B iff there is a set X in @(A><B) such that A(1)-(m)X(n)-(1)B. .UML Net{A(1)-(m)R(n)-(1)B}
Even complex systems of relationships can be modeled using sets and functions. For the elevators we have: .UML Net{Elevator, Button, Floor, Direction, Button_in_elevator, Button_on_floor}
Abstracting a formal model of a system proceeds by stating the obvious. Boring truths are certain truths. Simple facts, sets, and maps determine the set of logically correct data structures or data bases.
Dynamics
So far we have documented the unchanging or static properties of the
elevators. We now look at varying properties - the dynamics of elevators.
A dynamic system is imagined to have a state that varies with time. A
set of possible states is often called a state-space . If a dynamic has
one or more parts then each has its own a state. The state-space of the
whole has components (or dimensions) for each of its parts. When a system
has many similar parts, the state of the whole is an n-tuple. Often a
systems state is also constrained to lie within a subset of the product
space of its components. Now a system needs an internal model of the any
system it controls and this implies a homomorphism connecting them
[Beer74]
[RossAshby57]. So the abstract model of a system to be controlled or
monitored reveals the structure of the software that controls or monitors
it
[Jackson78].
To describe the state of the whole "Lift System" we define the state of
each elevator and button. At any time a button has either been pushed to
request a service, or it has not been pushed or if pushed then the request
has been serviced since the last push. Therefore we define
R::@B=buttons with outstanding requests for service,
Hence we can formulate concepts like:
The buttons on floors with requests to go up = R & Up./l.
The buttons on floors without requests to go up = S & Up./l.
The buttons in lifts with requests to go to floor = R & Up./l.
The floors with up requests = (R & Up./l).P.
We can also prove that
Universe of Discourse
We will need to make a model of the positions of the elevators and other
objects. Let U be the universe of discourse - the set of all objects we
are discussing:
Heights
In the elevator problem we will need to reason about the relative heights of
objects:
One of the main benefits of using mathematics in analysis and design is
using known results. Thus we look at elevators and talk to our clients and
users and verify the following axioms :
This means that < is a linear order on U. From the theory of linear orders we know that we can model the relation by associating a number with each object. We can assume that the floors are vertically above each other and inside a finite building. We can model height as a set of real numbers called 'X':
x0 is the minimum height - just above the height of the bottom of the building.
x1 is the maximum height - just below the height of the top of the building.
Assume that there are no holes in the lift shaft:
Assign a height x(u):X to all objects u:U that are in the problem,
This is not the "real" height, but an assigned height - for example buttons
are assigned the same height as the object to which they are attached,
Notice that we can always use a map to 'pull back' properties from its
co-domain into its domain. Define ' above/equal/below' relations in U (the
dom(x)) as the inverse image of 'less than/equal/greater than' in the X
dimension(cod(x)):
Therefore for all heights h between x0 and x1 we can define the next floor above and next floor below a height,
Times
Now, the position of moving objects (like elevators and the buttons in
them) depend on the time. We can symbolize the set of times by T and we
will assume the following properties for it:
Reusable Specifications on the Net
Now a linear order is a standard part of mathematics. A library of standard
mathematics is vital resource. Software Engineers need a library of
documentation for fundamental ideas like order, time, number, arithmetic,
calculus, sequence, tree, list, space, group, and so on. Manuals and
source code are already shared by Electronic Mail or anonymous FTP. Ideas
also need to be shared. In this case much of the formal theory
of orderings is already online:
[ math_21_Order.html ]
We need a much larger Internet
library of formal systems like this!
In my work a set of declarations, assertions, theorems, comments and definitions is reusable if it is named. For example a linear ordered set is documented as a "net" of variables and properties like this:
Given a set of documentation called N then $ N is a
set of objects that satisfy the documentation. For example:
This declares a set T with relations(<,>,<=,>=) and imports its axioms from the library. Similar ideas are used in most formal documentation systems - Z, Lotos, Ina Joe, ....
Returning to the dynamics of elevators, a common convention omits the ts (Times) from definitions and assertions that hold at all possible times. I will do this from now on. We might assume that an elevator is always at a unique floor, but there exist times when it is between floors. When a lift is between floors it should be moving in a particular direction, and when moving it should not be 'at' a floor. If a lift ceases to move between floors then something is wrong with it. In other words a particular lift is either moving in a direction, stopped at a floor, or out of service. It would be incorrect to document movement as a map from Elevators into Directions, because stationary Elevators are not moving in a Direction.
Note: optative mode
The above is a nice example of what Michael Jackson calls a statement that is
in the optative mood. The term comes from Alonzo Church's terminology for
the logic of wishes.
Statements in this mode are statements that
we want to be true of our system when our designed machine or improvement
is correctly installed in the system. We can not expect randomly moving
elevators to avoid stopping between floors and trapping their passengers,
so we must require our controller to enforce this unnatural rule. In
the SCR method NAT is the set of statements describing the behavior of
the natural world and REQ are the statements describing the
required world. Jackson notes that if SPEC describes the
software system and we have written it correctly
then we expect to be able to prove the following:
if SPEC and NAT then REQ.
Velocities
The elevator's movement should be smooth to keep the passengers happy.
Therefore we can talk about the velocity of the lift - the rate of change
of the height with respect to time. Model velocities by another variable
(y). We can assign the velocity of zero to floors - since they do not
move. Thus for all objects u, we have a velocity y(u),
Using x and y we can define what it means to service a request for a floor:
Events in the Life of an Elevator
In this problem, we are only interested button pushes and buttons being
serviced. Thus each significant event has two components - the button and
the type of event (pushed or serviced).
The significant patterns of events in the life of an button are defined by this grammar [Botting87a], [Botting87b]:
Jackson has shown that detailed code can be derived from grammars like this [Jackson75], [Jackson83], [Cameron84], [Cameron86], and [Cameron89].
The three dots (elision) show that part of the set of requirements has been hidden (elided).
Why Buttons are labeled Up and Down
We have abstracted a model of 'Up' and 'Down', but we have not explained
why there are up and down labels on the buttons on the floors of the
building. Now if we talk to some users we find that they prefer to get on
an elevator that is going in the right direction even though the
elevator is stationary at the time. Or perhaps we look at some elevators
and we see that they have lights indicating a direction - even when they
are stationary. We therefore add a third dimension to our state space -
Z={Up, Down, 0} and assign a value ( z(u)) in Z to each the object u:U.
State Space
Every object in U has 3 co-ordinate values (x,y,z) in a 3 dimensional space
- call it XYZ:
We can now state a desirable property of elevators: When elevators are
moving then they should be moving in the desirable direction:
The next step is to derive the sequence in which each lift/elevator can service buttons in terms of xyz coordinates from the physical limits on how fast elevators can stop and start. From here it is easy to describe how the sequence changes as events occur and use it to define a strategy for deciding which elevator is allocated to serve buttons. Implementation of these relations is discussed elsewhere [Botting85].
. . . . . . . . . ( end of section The Lift Problem) <<Contents | End>>
Conclusions
I have shown how mathematics can help analyze a semantic domain. The
product is formal model or language that is suited to the construction of
requirements, specifications, and designs
[Jackson83],
[Botting85],
[Botting87a],
[Botting87b],
[Wing87],
[Chang89],
[Milietal89], . . . ,
[YeungTopping90].
In general Formal Analysis proceeds by stating the obvious. Simple facts determine the set of logically correct structures. In my monograph I argue that grammars, dictionaries and sets of sequences are useful for documenting the data (data dictionaries). The same theory helps define the dynamics (entities, events and patterns) in a situation. Sets and functions describe the structure of the problem domain and are used to document requirements and specifications. These sets and functions define entity types, abstract data types, classes of objects, and/or paths through the data structures and data base. Thus maps and sets define the structure shared by the solution and the problem's environment.
Projects that use mathematics and logic can "zero-in" on the best software. First: Define things that appear in the description of the problem and (1) are outside the software, (2) interact with the software, and (3) are individually identifiable by the software. Second: Define events, entities, identifiers, relationships, attributes, facts, and patterns. .Figure Zeroing In
These initial steps are an exercise in stating the obvious. Facts are recorded and verified by experts and from observation. When the obvious facts are not enough then hypotheses need to be introduced and theories constructed. The Scientific Method is an effective way to develop a mathematical theory or model of the situation. If a system interacts with another system then it will have an internal model of the other system. Abstracting a formal model of the external system reveals a natural internal structure and so a structure for a design. Computer Science already teaches the techniques to implement the designs plus the calculus of sets, maps, and relations used for this purpose.
Because the model is abstract it is more reusable than computer oriented documentation. Further it can refer to abstract models developed by mathematicians: ordering, topology, algebra, geometry, etc. These are highly reusable. Because the syntax is formal it also possible to extract information from the document using comparatively stupid tools. These tools can produce variously rendered forms of the same ideas (diagrams, HTML, SGML, \Tex, ...). Questions can be answered by simply searching the raw documents as well.
The models are used to validate requirements, specifications, designs, algorithms, data structures, and data bases.
We have two Directions, and Up and Down are two different
elements in that set. So
. . . . . . . . . ( end of section An Example of Formal Analysis) <<Contents | End>>