[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Monograph] / 02_MATHS_AND_TEMPO.example
[Index] || [Contents] || [Source] || [ Search monograph] || [Notation] || [Copyright] Wed Aug 4 10:09:13 PDT 2010
Opening the PDF files on this page may require you to download Adobe Reader or an equivalent viewer (GhostScript).


    An Example of Formal Analysis

      .Note This uses my MATH notation. Notes on method will be prefixed by '.Note'. In the raw format (.mth or .txt) headers have a '.' in the first column. Sections start with .Open and end with .Close. A UNIX shell script renders this into HTML.


      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 Jackson 83, Wing 87, Chang 89, Mili et al. 89, and many others. Implementation steps have also been covered [Botting 87, for example JSD+ADA in Yeung & Topping 90].

      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 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"(a 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 is based on part of chapter 2 of a monograph I'm trying to get published. This was revised in April 1993.

      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 Lift Problem


        In a building there are some elevators (or lifts) each of which can stop at any of the floors in the building. Each elevator has buttons inside that are pushed by people to request floors which that elevator will service. Outside the elevator there are also buttons - these request a visit from an elevator traveling in a particular direction (up or down).

        Formal Analysis

        Elevators, floors and buttons are documented because they appear in the description of the problem. 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 this is documented as:

      1. Elevators::Finite_Sets,
      2. Floors::Finite_Sets,
      3. Buttons::Finite_Sets,
      4. B::=Buttons,
      5. E::=Elevators,
      6. F::=Floors,
      7. m::=|E|,
      8. n::=|F|.
      9. -- the number of elements in set E is |E|=Card(E).

        The above has declarations (with a two colons ) and definitions (with a 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 will ultimately be implemented as entity types, abstract data types, or classes of objects.

        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 (1).

      10. (1): n >= 2 and m>= 1 .

        There are two distinct types of button - floor selection buttons inside elevators and the call elevator buttons on the floors outside the elevators.

      11. G::@B=Buttons inside elevators that select floors.
      12. H::@B=Buttons on floors for calling lifts to floor.

        It is helpful to associate a name with a phrase. The special string form ... allows this. This gives a natural language translation of the term. The "@" means "set of" (\power-set ).

        Now a button is either inside an elevator, or outside. 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:

      13. (2): B >== { G, H }.

        The buttons outside the elevator ( H ) are labeled with one of two directions(D):

      14. D::=Directions::={Up, Down}.

        Up and Down are not in F:

      15. (3): Up and Down not_in F. 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.
      16. L::=Labels::= F | D.

        Each Button has its own label, so there is a mapping from B to a set Labels.

      17. l::B->L=the label on button (_).

        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). l(b) shows the result of applying the function l to element b.

      18. |- (4): For all b:B, l(b)=the label on button b.

        The sign (|-) is short for "It can be shown." It shows that the formula can be derived from previous formulae [ Ina Jo , Wing and Nixon 89, Whitehead and Russell 66].

        MATHS also use the 'dot' notation for function application:

      19. |- (5): for all b:B, l(b) =b.l.

        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.

        There is a version of the lambda notation for maps:

      20. l::B->L= map[b]the label on button b.

        I also overload maps so that they also to apply to sets, so:

      21. |-for all f:A->B, X:@A, f(X) = X.f = {b:B || for some x:X (b=a.f )}.

        We can therefore state the following axioms:

      22. (6): l(G) = F -- buttons in elevators are assumed to have floors as labels.
      23. (7): l(H) = D -- labels of buttons outside the lift are assumed to be directions.

        I use '/' symbol to reverse the direction of a map or relation. For example:

      24. for all y, /l(y)=y./l =buttons labeled y.

        If a function f maps from A->B then /f maps subsets and elements in B into subsets of A. In general:

      25. for f:A->B, b:B, b./f= /f(b)={a:A || a.f = b},
      26. for f:A->B, Y:B, Y./f=/f(Y)={a:A || a.f in Y}.

        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:

      27. |- (8): H=D./l.
      28. |- (9): G=F./l.

        Harel's Higraphs are an extended Venn diagrams that summarize and clarify systems of sets and maps [Harel 86 & 88, Coleman et al 92]. In a higraph, "blobs" represent sets and arrows represent maps.

        .Higraph Net{ B,H,G,D,L,F,E,l}. [ Lift.Fig1.pdf ] (PDF)

        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):

      29. (10): l in H(n-1)-(1)D,
      30. (11): l in G(m)-(1)F.

        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:

      31. For b:B, u:F|E, b P u::@=b is a part of u,
      32. For b:B, b.P::F|E=the elevator b is in or the floor b is on,
      33. For x:F|E, x./P::@B=the buttons that are parts of x. F./P::=the buttons placed on floors, E./P::=the buttons placed inside an elevator.

        We assume that each part is in (or on) one other object:

      34. (12): P in B->F|E.

        After examining some elevators we add these properties of 'parts of` (/P) and 'labelled'(/l):

      35. (13): G = E./P = F./l,
      36. (14): H = F./P = D./l,
      37. (15): P in H(1..2)-(1)F | G(n)-(1)E,

        Expressions like A(n)-(m)B represent sets of relations - those that link 1 A with m Bs and 1 B to n As. .Higraph Net{ B,H,G,D,L,F,E,l, P}. [ Lift.Fig2.pdf ] (PDF)

        Bachman designed a diagram for documenting collections of sets and relations [Bachman 69]. There are several varieties [ Chen 80, Martin & McClure, Wiederhold 77, Ward & Mellor 85]. I use only the simplest form - a Conceptual Model [SSADM 80] or Conceptual Structure[Carasik et al 90]. This is equivalent to a simple UML class diagram with all attributes and operations hidden. Boxes represent sets and lines show mappings. The boxes are placed so that the mappings run from lower boxes to higher ones - this makes the diagrams easier to read [Martin & McClure]. 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].


        .Bachman Net{f:A(n..m)-(1)B}. .Bachman 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 [ Codd ]. 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. .Higraph Net{A,B::Sets, X::@(A><B)} .Bachman 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: .Bachman 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.

        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 [Beer 74, Ross Ashby 57]. So the abstract model of a system to be controlled or monitored reveals the structure of the software that controls or monitors it[ Jackson 78].

        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

      38. R::@B=buttons with outstanding requests for service,
      39. (16): R&G= requests for a lift to come to a floor.
      40. (17): R&H= requests for lifts to go to a floor.
      41. S::@B=buttons with no outstanding requests for service
      42. (18): B>=={R,S}, -- some buttons have requests, others don't.
      43. (19): S&G=serviced elevator call buttons.
      44. (20): S&H=serviced go to floor buttons.

        Hence we can formulate concepts like:

      45. The buttons on floors with requests to go up = R & Up./l.
      46. The buttons on floors without requests to go up = S & Up./l.
      47. The buttons in lifts with requests to go to floor = R & Up./l.
      48. The floors with up requests = (R & Up./l).P.

        We can also prove that

      49. |-(21); R&H & Up./l= R & Up./l

        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:

      50. U::Sets=The universe of discourse.
      51. (22): U>=={E,F,B}.

        In the elevator problem we will need to reason about the relative heights of objects:

      52. For u1,u2:U, u1>u2::@= u1 is above u2.

        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 :

      53. (h1): u1<u2 iff u2>u1.
      54. (h2): if u1>u2>u3 then u1>u3.
      55. (h3): Exactly one of u1<u2, u1=u2, or u1>u2 is true. .Higraph Net{U, U><U>=={(<), (=), (>)}.}

        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':

      56. X::@Real=Heights of Objects,
      57. x0::=min X,

        x0 is the minimum height - just above the height of the bottom of the building.

      58. x1::=max X,

        x1 is the maximum height - just below the height of the top of the building.

        Assume that there are no holes in the building:

      59. (23): X={x:Real | x0<=x<=x1}.

        Assign a height x(u):X to all objects u:U that are in the problem,

      60. x::U->X=the height assigned to (_).

        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,

      61. (24): for all s:E | F, Button b where b P s (b.x=s.x).

        Notice that we can always use a map to 'pull back' properties from its codomain 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)):

      62. for u1,u2:dom(x) ( u1>u2 iff x(u1)>x(u2) ),

        This last is written (chapter 4, structure preserving maps) (>)::@(U><U)=(>/x),

      63. |- (24): x in (>) U->X.

        Therefore for all heights h between x0 and x1 we can define the next floor above and next floor below a height,

      64. next_above::=(min{f:F || x(f)>(_)}),
      65. next_below::=(max{f:F || x(f)<(_)}),
      66. |- (25): next_above and next_below in X (some)-(0..1) F.

        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:

      67. T::=Times::linear_ordered_set(<), for t1,t2:T, t1 < t2::@= time t1 is before t2.

        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. I have a long term goal to create an Internet library of formal systems for this purpose.

        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 like this:

      68. LOSET::=
          T::Sets. A Linearly Ordered set.
        1. (L0): Strict_partial_order(T,<).
        2. ...
        3. |- (Ln): For some m:T->Real, m in (T,<)->(Real,<).
        4. }.

          The dollar sign indicates a set of documentation and the ellipsis (...) hides unwanted details. Given a set of documentation called N then N is a set of objects that satisfy the documentation. For example:

        5. |- (26): (T, <) in LOSET.

          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.

        6. is_moving::E (0..)-( 0..1) D,
        7. at::E ( 0..m)-(0..1) F.
        8. (27): For all e:E ( for some d:D( e is_moving d ) or for some f:F ( e at f ) ).

          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 we have a velocity,

        9. Y::=velocities::=Real,
        10. y::U->Y.
        11. (28): For all u:E, u.y=d(u.x)/dt.
        12. (29): For all u:F, u.y=0, -- floors don't move.
        13. (30): For all u1, u2:U, if u2 P u1 then u2.y=u1.y,
        14. --parts have same velocity as the whole.

          Using x and y we can define what it means to service a request for a floor:

        15. (31): If elevator e services floor f at time t then f.x=(e(t)).x and (e(t)).y = 0.

          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).

        16. V::=events::Sets,
        17. (32): V=B><W. -- Events involve pushing or servicing buttons, where
        18. W::Finite_Sets=Types of events occurring to buttons,
        19. p::=pushed::W, s::=serviced::W,
        20. (33): W={p,s}.

          Let v::T->V, (34):for all t:T, b::B, v(t)=(b,p) iff b is pushed at time t,

        21. (35): for all t:T, b:B, v(t)=(b,s) iff b is serviced at time t.

          The significant patterns of events in the life of an button are defined by this grammar [Botting 87]:

        22. For b:B, Button_life_history(b)::= #Request(b),
        23. For b:B, Request(b)::= Push(b) #Push(b) Service(b),
        24. Push(b)::={(b,p)},
        25. Service(b)::={(b,s)},
        26. For all A, #A= ( {""} | A #A), ... .

          Jackson has shown that detailed code can be derived from grammars like this[Jackson 75 and 83, Cameron, ]

        27. Requirements::=
          1. (R1): All requests are ultimately serviced:
          2. for all t1:T, b1:B, (
            1. if v(t1)=(b1, p) then for some t2:T(t1<t2 & v(t2)=(b1, s).
          3. (R2): No request is serviced more than once:
          4. for all t1, t2:T, b:B (
            1. if t1<t2 and v(t1)=v(t2)=(b,p) then for 0..1 t:T (t1<t<t2 & v(t)=(b, s)).
          5. (R3): ... }=::Requirements

            The three dots (elision) show that part of the set of requirements has been hidden (elided).

            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.

          6. Z::=D|{0}, z:U->Z,
          7. z::E->Z=current direction of elevator (_),
          8. z::F->Z= (0),
          9. z::B->Z= (if (_) in H then (_).l else 0).

            Every object in U has 3 co-ordinate values (x,y,z) in a 3 dimensional space - call it XYZ:

          10. XYZ::=X><Y><Z,
          11. xyz::U->XYZ=map[r](r.x, r.y, r.z).
          12. (36): For all u:U, u.x=u.xyz.1st and u.y=u.xyz.2nd and u.z=u.xyz.3rd.
          13. (37): For all f:F, xyz(f)=(f.x, 0, 0), - floors don't move!
          14. (38): For all u:U~H, r: u./P ( xyz(u)=xyz(r) ).

            We can now state a desirable property of elevators: When elevators are moving then they should be moving in the desirable direction:

          15. (39): For all e:Up./z (y(e)>=0) and for all e:Down./z(y(e)<=0), or equivalently:
          16. (40): For all e:E, if z(e)=Up then y(e)>=0 else if z(e)=Down then y(e)<=0.

            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 [Botting 85].

            Higraph of Lift Problem

            .Higraph following
            1. B::=Buttons::Finite_Sets.
            2. E::=Elevators::Finite_Sets.
            3. F::=Floors::Finite_Sets.
            4. G::@B=Buttons inside elevators.
            5. H::@B=Buttons on floors for calling lifts.
            6. D::=Directions::={Up, Down}.
            7. d::=Down::D.
            8. L::=Labels::= F|D. p:W::=pushed.
            9. P::B->F|E= is a part of.
            10. b.P::F->E=the elevator b is in or the floor b is on. u./P::@B=the buttons that are parts of u.
            11. R::@B=buttons with outstanding requests.
            12. S::@B=buttons with no outstanding requests.
            13. s::=serviced::W.
            14. T::=Times::linear_ordered_set(<).
            15. U::Sets=Universe of discourse. U=E|F|B.
            16. u::=Up::D.
            17. V::=events::Sets.
            18. W::Finite_sets=Types of events occurring to buttons.
            19. X::@Real=Heights of Objects.
            20. x::U->X
            21. XYZ::=X><Y><Z.
            22. xyz::U->XYZ=map[r](r.x, r.y, r.z).
            23. Y::=velocities::=Real.
            24. y::U->Y.
            25. Z::=D|{0}.
            26. z::U->Z.

            (End of Net)

            [ Lift.Fig3.pdf ] (PDF)

          . . . . . . . . . ( end of section The Lift Problem) <<Contents | End>>


          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 [See Jackson 83, Botting 85 & 87, Wing 87, Chang 89, Mili et al. 89, ... , Yeung & Topping 90].

          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.

          The models are used to validate requirements, specifications, designs, algorithms, data structures, and data bases.

          Overview of Other Conclusions

          In my monograph I argue that the 'Art of Computer Programming' can be replaced by a form of Software Engineering that is based on science.

          .Figure SADT Actigram

            A1::=Analysis::Action. A2::=Design::Action. A3::=Implementation::Action.
          1. Analysis=(input=> Model, output=>model, Control=> {system, client,
          2. proposal}, Support=>{Scientific Method, Discrete Math, CASE}).
          3. Design =(input=> Designs, output=>{Proposals, Designs}, Control=> {Model,
          4. problem}, Support=>{ Math, Stats, Computer Science,CASE}).
          5. Implement =(input=> System, output=>{System, Problems}, Control=>
          6. {Designs}, Support=>{ Computing, Software Tools}).

          In the monograph I show how the calculus of relations and an extension to the lower predicate calculus are useful for specifying processes and programs(Chapters 2, 4, 5 and 6]. I also argue that logic, mathematics, and proofs should be a part of project documentation from the initial stages. An inference engine or automatic theorem prover is not essential and may be an uneconomic investment since simpler software can check the engineer's reasoning when it is expressed in a formal language [Chapter 4 of my monograph]. I have designed an ASCII based formal language (MATHS). Since Engineers use blueprints I also demonstrate a natural graphic representation (TEMPO). These are based on a formal model of documentation.

          Some documentation says too little, and some says too much. Intuitively we have a category of logical systems that document objects. In this category we can distinguish two extremes. Free or initial documentation is the weakest useful documentation. At the other extreme there are the final, inconsistent or universally attractive documentation which over-defines the situation to the point where no instances can exist. In between, for each project, there is the level of documentation that reflects exactly what the client understands the situation to be. There is a another set describing the technical structure of the software and hardware involved. The combined set I call this the canonical documentation. It forms the cannon or Bible for the project. It shows the user or client that we understand all their terminology.

          MATHS & TEMPO are defined to support formal analysis and design. They help solve two outstanding problems in the software process. First, As Hoare suggested, we need to show the user the external design of software [Hoare 73]. The diagrams and formulae show how the user's data is handled in terms that they understand(sections 2 and 3 of chapter 2 of my monograph). In chapters 3, 5 and 6 of my monograph I will show how we can guarantee that this understanding is accurately modeled in the software. Second, Strachey pointed out the need to discover data structures before attempting functional design [Strachey 66]. The sets and maps found by formal analysis connect facts to conceptual data structures(section 4). Standard data base and data structures techniques can then implement the conceptual solution to the problem(section 5).

        . . . . . . . . . ( end of section An Example of Formal Analysis) <<Contents | End>>