(1) MATHS is a Multipurpose Abstract Terminology, Heuristic, and Symbology. (2) MATHS makes formal methods easier. (3) MATHS fits many methods. (4) MATHS is modular and reusable. (5) MATHS is a cheap way to write mathematics.
This chapter introduces a graphic representation of MATHS that is called TEMPO. This name is short for "Temporal Map".
. . . . . . . . . ( end of section 2.1 Introduction) <<Contents  End>>
Table
NamePurpose  Elements  Defined_terms  Sources 

Syntax, Grammar  TokensLexemes  Syntactic units  Naur et al 64,... 
Tagged CFG  Lexemes  Tagged sets of strings  Mark & Cochrane 92 
Lexical Dictionary  Strings,character names  Tokenslexemes  Bell Labs 83(lex ) 
Parser  Literals & Characters  Text form of Object  CELLAR[pp2122 of Rettig 93] 
Data Dictionary  Data types and values  Data files  De Marco 80,... 
?  Commands  System Behaviors  Belli & Grosspietsch 91 
Data Structure  Elementary Data  Files, Streams...  JSP 
Dynamic Dictionary  Events  Significant patterns  Kleene,DAD 
"  Events  Entity Life Histories  Robinson 79, SSADM 
"  Messages  Communication protocols  Zave 85, Naik & Sarikaya 92 
"  MessagesMethods  Objects  Botting 86a, Dedene & Snoeck 94 
Scenario Grammar  Events  States in Scenario  Hsia et al 94 
Dialogue Grammars  Stimulus/Response  Dialogues  Boute 81 
Task Documentation  Manual/automatic tasks  User needs  Lustman 94,CELLAR[p22 Rettig 93] 
Logic Grammar  Simple Terms  Predicates  Abramson & Dahl 89 
Interpreter Pattern  TerminalExpression  NonterminalExpression  Gamma et al 94(pp243255) 
Program Structure  Function Calls  Function Definitions  Baecker & Marcus 90 
Correspondence  Data  Programs  JSP, Appendix 3 
Other  Subprogram calls  Paths  Campbell & Haberman 74, S/SL 
?  Entries names  Ada task structure  Hemendinger 90 
Theory  Terminals:a..z  Non_terminals:A..Z  Eilenberg 74,...THEORY 
BNF <number>::=<digit><number><digit> [Naur et al 64]
EBNF number::= digit {digit} [ANSI 83 ADA, ANSI 95 Ada]
MATHS number::= digit #digit.The Ada EBNF symbols '{}[]' are used for sets and subscripts in MATHS. Ada EBNF { x } is #( x ) in MATHS. [x ] in Ada EBNF is O(x ) in MATHS.
Here is how
A::=a #(bc) dis shown in TEMPO on a nongraphic device:
A

 a 

( b  c )

 d 
The graphic representation for an intersection needs a third dimension. Instead we place the items diagonally and put an ampersand("&") at the top left hand corner:
The number sign ("#") always applies to the immediately following item and means "a number of (including none)". So if
To show that a Record might be missing we use
To show that several Records can occur for each header/footer pair we would write
Similarly, (a  #b) indicates either an a or any number of bs, as does (#ba). This, plus the precedence of spaces over vertical bars means that a #b c  #b describes a string with a single a followed by many bs and one c or else many bs.
Parentheses (()) are put around unions within sequences, and iterations.
Notice that this describes four alternative forms because:
. . . . . . . . . ( end of section 2.2 EBNF & Dictionaries) <<Contents  End>>
The meaning of EBNF is that each non_terminal and each set_expression represents a set of strings of characters. MATHS contains EBNF as a special case. A context free grammar(CFG) is a grammar without ("&") and ("~"). Here is an informal introduction to the problem of defining what a dictionary means (see chapter 3 for a more formal treatment). This section introduces ideas that reappear later in other contexts.
First we need to define what we mean by "string" and "sets of strings." Several formal models of strings have been translated into MATHS [Appendix 1.Theories of strings]. In all theories, strings come from an empty string by concatenating symbols. Concatenation of strings is shown by an exclamation mark (!). It is an associative operation with a unit ( the empty string "" ). Each string, by definition, has a unique sequence of atomic symbols, which when concatenated generate the original string. Temporarily we symbolize strings by lower case variables and sets of strings by upper case variables. We next define operations of union(), intersection (&), complementation (~), concatenation() on sets of strings by:
A string is treated as a singleton set when it is in a context that needs a set of strings:
The above value satisfies the fixed point definition of M = g(M). Any subset does not. The reason that the Ss seem to get closer to M is that we have to look at longer and longer strings to find a string in M that is not in S(i) as i tends to infinity. Using a limit to define the meaning of grammar has been around in the literature for a long time  but is not stated in many texts(bibliography in section 6.7 of chapter 3). The fixed point definition came later and similar to Scott's denotational semantics [ACM 86]. In chapter 3 we will have the notation to make the above more formal. Similar techniques are appearing across a wide range of research in software engineering and computer science [ Example: Tsai Wiegert & Jang 92]. We will return to fixed points and recursion in chapters 4 and 5.
Note that the operations on strings and sets of strings do not normally need defining in a MATHS document. They are part of a standard package of operators that are predefined [See Appendix 4 and Chapter 4, section 8].
These define the magnetic tape's physical structure. If we were designing a program to process a file of enrollement records we might describe a file sorted by sections as follows:
Strictly speaking a definition of form A::= B  A~B is a theorem ` A = B  A~B`.
If the domain has the words "file", "section" and "student" we use a similar structure, even if the class header is absent and a student record identifies the student's class instead. The result is called a logical structure.
If the problem is to summarize the data on each section then we might show the output as:
It is easy to combine these into one structure and map it into a program structure:
The structure above becomes a program when operations and conditions are added (See Section 6.5 below and DDD in Chapters 2, 6, and 9).
Notice that the dictionary developed while designing a program must document all the important structures of the data  both the physical and the conceptual. Thus semantic and pragmatic terms are defined to clarify the meaning and use of data. This in contrast to the data dictionary developed by an analyst or system designer. These must be free of semantic and pragmatic structures because a file can be used for many purposes and hence is parsed into different structures. Typically:
Data dictionaries and TEMPO diagrams can solve a problem pointed out by Hoare in 1973: How to show a nonprogrammer what a program is expected to do. The canonical grammar or dictionary shows the user or client that we understand all their terminology. Canonical diagrams and dictionaries show how the user's data is handled in terms that the users and clients understand[Katzenberg & Piela 93]. The test of a canonical dictionary is that clients and users certify it as complete and accurate. Canonical dictionaries are the strongest useful dictionaries.
Consider a button on a control panel. There are two types of event that can effect it  it may be pushed  requesting a service, and it can be serviced by some means or other. At first glance we have:
. . . . . . . . . ( end of section 2.3 Syntax Description) <<Contents  End>>
MATHS documents are a mixture of commentary and formal statements[cf McDermid 89 p136]. I also include some commentary about the notation that would normally be omitted.
. . . . . . . . . ( end of section 2.4 An Example of Formal Analysis) <<Contents  End>>
Expression  Values  Syntax  Semantics 

P  true false    
not P  false true  prefix  @>@ 
Table
Expression  Values  Syntax  Semantics 

P  true true false false  
Q  true false true false  
P and Q  true false false false  infix(serial)  @><@>@ 
P or Q  true true true false  infix(serial)  @><@>@ 
P iff Q  true false false true  infix(parallel)  @><@>@ 
if P then Q  true false true true  special  @><@>@ 
Surprisingly, unlike most programming languages, mathematics has two kinds of infix operator. MATHS follows mathematics:
Notice that when predicates get complicated then it pays to be able to display them in the form of tables and/or charts  This has proved good for logic circuit design (Karnugh maps), Data Processing (Decision tables), and formal specifications[Leveson et al 94]:
A predicate is a proposition that has variables, quantifiers and an equality relationship. MATHS spells quantifiers out and includes numerical quantifiers like "one", "no", "0..1". The syntax attempts to make the writing of formal statements as natural as possible. In the following X is a set or a type, x is a variable and W(x) a proposition containing x in a number of places. for all x:X(W(x))::=For all x of type X, W(x) is true, for x:X(W(x))::= for all x:X(W(x)), for no x:X(W(x))::=for all x:X(not W(x)), for some x:X(W(x))::=not for no x:X(W(x)).
for 0 x:X(W(x))::= for no x:X(W(x) ), for 1 x:X(W(x))::= for some x:X(W(x) and for 0 y:X(x<>y and W(x)), for 2 x:X(W(x))::= for some x:X( W(x) and for 1 y:X(x<>y and W(y)) ). for 3 x:X(W(x))::= for some x:X( W(x) and for 2 y:X(x<>y and W(y)) ).
Table
Expression  Meaning  Type Example.  

Sets  
{}, ∅  null or empty set  Ambiguous  
T  universal set @T  Numbers  
{e1} = $(e1)  singleton @T (e is of type T)  {1}  
{e1,e2,e3,...} extension @T (e1,e2,...are type T) {1,2,3}  
{x:T  W(x) } intention @T  {n:Natn*n=4}={2}  
${D} Set satisfying documentation D  [See section 5.5].  
S1 & S2, S1 ∩ S2 intersection  @T><@T > @T  ..n&m..=n..m  
S1  S2, S1 ∪ S2  union  @T><@T > @T  ..n1  m+1.. 
S1 ~ S2  complement  @T><@T > @T  = Nat ~(n..m) 
Predicates  
e in S1, e ∈ S2,  
e is in S2 membership  T><@T > @ 1 in 1..  
S1<> S2, S1 \noteq S2  inequality  @T><@T > @  1..<>0.. 
S1 = S2 equality @T><@T > @  1..2={1,2}  
S1==>S2, S1 are S2,  
S1 ⊆ S2 subset or equal  @T><@T > @  1..2==>1..3  
S1=>>S2, S1 ⊂ S2 proper subset @T><@T > @  1..2=>>1..3  
S1>==S2  S1 partitions into S2  @T><@T > @  {1,2,3}>=={{1,2},{3}} 
S1  S1 is not empty  @ (overloaded) ..n+1&n1..  
no S1  S1 is empty  See below( Q A)  no ..n1 & n+1..

Strings are also part of MATHS. #T is the type of object generated by concatenating objects of type T together. They can be modeled by lists and inherit the operations, properties, and predicates acting on lists. In addition
Tupls look like this: (a=>xa, b=>xb, ...). They are in a type defined by one of the following ways:
Short forms
Long definition
Each label in a MATHS structure can be used to extract components from tupls with the dot operator of Ada, C, Pascal,..., and Z:
Because projections are maps, they are relations and so have converses. So for eaxmple
One way to imagine a MATHS structure is to think of it as a record or object in a high level language or a labeled tupl in a RDBMS. The formal definition implies a collection of maps. Thus phones=Net{name,number::Strings} implies name in phones>String and number in phones>String. Formally, phones is the universal (free, initial, or universally repelling) object in the category of types with names and numbers. In other words: all types with two functions called name and number mapping objects into the Strings, is modeled by phones, because for any such type there is a function that maps phones into it without loosing the information about names and numbers. Therefore phones encodes all sets of objects with names and numbers(details in Chapter 5).
In general a property of the components defines a set of objects:
Codd has shown that any set of data can be expressed as simple structured tables like the above. Thus we can model all data as tuples. A collection of sets of tuples is a relational data base and forms a category. The objects in an object oriented design also forms a similar category [Freedman 83]. Adding constraints to sets of tuples proves to make specifications much simpler[ Z, Gal & Etzion 95]. Structures form a conceptual model of the area being studied that is readily implemented using modern technologies such as data bases, logic programming, and objects[Chapter 5].
Binary relations lead to a language for program specification and design  see sections 6.3 and 6.4 below.
. . . . . . . . . ( end of section 2.5.5 Structures) <<Contents  End>>
After some more analysis the model became: [ UNIVERSITY in rjb93b.discrete ]
Maps
Relations
Properties For f:F, s:N, if f T s then f M d(c(s))
Conceptual Model
(Each vertical line is a mapping  a "hasa" relation. "n" represents a range of numbers yet to be determined. '+' shows that the lower class inherits all the properties, etc. of the upper one, an "isa" relation)
People
1 1
+ +
0..1 
Faculty Department 
1 1 1 1 1 
 +    
 0,1 *  * 0..1
 Member  Qualification Student
  1 1 1 1
   * * 
 *  Declared 
 Course * 
+ 1 1 ElectiveSet 
   1 
 * * * 
 Section in 
 1 1 
0,1 * 10..200 0..10
Teacher Enrollment
Standard technology and techniques can be used to implement sets and mappings  using (1)files, (2)a DBMS[ DATA], or (3)data structures plus OOP[ OOP]. An alternative is to treat each entity and relationship as a functor or predicate in a logic programming system[Keller 87, PROLOG]. However classes can not be derived from the static analysis above. It should now be extended by a study of the dynamics of the entities and relationships so that objectoriented classes (with both attributes and methods) can be specificied. Two examples of this were given for a push button in sections 3 and 4 above. Further an inheritance structure often needs to be worked out in detail in complex models to make the logical desin and physical implemntation more reusable  this is covered in section 6.2 next.
. . . . . . . . . ( end of section 2.5 Logic, Sets, and Structures) <<Contents  End>>
So for x:MAMMAL, cat(x) iff species(x)=feline, see Chapters 5 and 6 for details.
In frame theory there are normal and abnormal forms[Tsai Wiegert & Jang 92, Kaindle 93]. In MATHS it is possible to develop two pieces of documentation for each case and keep what is common to both separate, for example see the theory of ORDERS in Appendix 1.
The somewhat confusing concept of inheritance found in objectoriented programming seems to be an attempt to implement these classifications. In chapter 5 I define inheritance as a relationship between different types (not between objects, nor between subsets of the same type). One Type inherits from another if the signature of the first is a subset of the signature of the second, and for all other types, if the second type appears in the signature then so does the first type. Using inheritamce can lead to a simpler diagram in complex systems. It is also claimed to lead to more reusable code[Gamma et al 94].
MATHS relations can be written in a form that makes them look like statements in a programming language. Some syntactic sugar is defined for while/for/loops/. Here follows an introduction. Formal treatment comes later when we have the techniques [Chapters 5].
The key definition is that of a dynamic predicate. A predicate is a proposition that has free variables. A dynamic predicate has free variables with primes (') attached to them. Here is an example:
Here is a more general statement of the MATHS interpretation of a predicate that contains variables with primes. Consider a simple state space S which declares m variables x1, x2,...x[m] of types X1, X2, ...X[M]:
The relation defined by P(y1', y2', y3', ...y[n]', x1, x2, x3, ...x[m]) is found by:
A more rigorous definition will be worked out in Chapter 5 meanwhile here are some examples. To specify a process that solves two simultaneous linear equations we write
Dynamic predicates can be used with any type of variable. The Programming Research Group at Oxford University, England has shown how dynamics can be simply specified as changes to sets[ Z]. Sets specify the possible data bases. This can be done in MATHS. Here is an example from the Elevator system(section 4 above):
Relationships change in real systems. Indeed most Z specifications contain scheme that describe the changes that can occur in a collection of sets and relations. For example, in a university in section 5.6 above a student can add and drop sections of classes:
Relationships can also be defined in a EBNF like form  complete with recursion:
The definitions of ancestor and lineal_descendant illustrate the transitive closure or ancestral relation of parent and child. The reflexive transitive closure is important and defined as follows:
We can also define the power of a relation [cf Antoy & Gannon 94] via the following equations:
Returning to how we could manipulate SUM above: First since the (+) is defined to be an operator on numbers, so the smallest state space is ${n,s:Numbers}. Next define names for the parts of SUM:
NowS ==> F and F;E==>F.
so
Hence, after SUM, s= 1+2+3+4+...+(n1) where n=101 = 5050.
Notice that MATHS is not a programming language. So
MATHS includes structures like those of structured programming because: For R:@(S,S),
MATHS expresses something like an extension of Dijkstra's Guarded Commands  see chapter 6 for details. Any group of MATHS users can document and then use its own set of abbreviations. For example:
MATHS can express mixtures of conditions and actions in one relation. A well known enigmatic program is often written:
In MATHS it can be transformed:
MATHS makes the derivation of programs more logical: (1) state the properties of the changed variables as a set of equations and then (2) solve for the primed variables. Similarly, a nondeterministic relationship can often be refined to a form that is compatible with a declarative programming system such as Prolog [Compare Lamport 87].
Finally, MATHS relational expressions follow the calculus of relations which can be used to simplify sequences into disjunctive normal form, like this:
Suppose we are interested in objects in a set A. #A is the set of sequences of objects in A. MATHS defines the following operators (See Chapter 4(section 8), chapter 5, and sample at the end of book):
Here is an example Data Directed solution to the problem of replacing double asterisks by a caret symbol [Hoare 78, compare Chandy & Misra 88].
The variables i and o are used for the standard input and output of a program so:
The above looks deceptively like pseudocode, but may demand unusual coding techniques (Appendix 2). The theory is developed in chapter 3, 4, and 5, and its application to programming is in chapter 6.
A second requirement is that in the possible expression the types of the symbols fit together. Variables and terms have types declared for them. When ambiguous the name of the type can be used to cast the term or variable. Operators and functions act on ambiguous expressions and form expressions of a particular type: For T:types, e:expression, T(e)=e.T has type T. For f: T1>T2, e1:T1, e2:T2,
Serial & Parallel Operators In mathematics
If + is a binary operator(with type T1^(T1><T1) say) and is defined to be serial, then for e1,e2,e3,e4,...,e[n]:T1,
Homogeneous relations are operators of type (T1><T1)>@. They are all parallel operators with two exceptions: (and) and (or). So for any relation R:
Consider the GCD example in section 6.6 above. Euclid's Algorithm is the standard solution. However if one has to evaluate a many GCD's then Euclid's algorithm is clearly inefficient, and remains so when coded iteratively. For example, when gathering statistics on the GCD's of all pairs of numbers in the range 1..2^p as p>oo I found that Euclid's algorithm recalculates the same values many times. Backtracking to the definition in section 6.6 we have:
. . . . . . . . . ( end of section 2.6 Special Techniques) <<Contents  End>>
MATHS is an unusual computerized language. Its philosophy includes these ideas:
When there is a need for unobvious statements then MATHS provides the ability to show that the uncertain statements must follow from less doubtful ones. A special sign () shows that the formula can be derived from previous formulae. An complete inference engine or automatic theorem prover may be an uneconomic investment since the engineer can work interactively with a simpler proof checker [Chapter 4].
Some documentation says too little, and some says too much. Intuitively we have a category of logical systems. In this category of documentation we can distinguish two extremes. There is a free, initial, or universal repelling object in the category of documented objects. Free or initial documentation is the weakest useful documentation. At the other extreme there are final, inconsistent, or universally attractive documentation  this overdefines the situation to the point where it can not exist. In between there is the level of documentation that reflects exactly what the client understands the situation to be. 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. Canonical documentation shows the user's world in terms that the users and clients accept. Ideally, the client reacts: "But, of course, that's what I mean,... ." The test of canonical documentation is that clients and users certify it as complete and accurate. Canonical documents are the strongest useful conceptual documentation.
Project documentation also describes the physical constraints caused by the technology (software+hardware+methods) used. Again there are two extremes: free and inconsistent. Some where between them is the best level. This records every assumption that can be made about the implementation technology. It is the canonical documentation of the technology being used when the software engineers are its clients and users. Ideally it would be provided, as a matter of proffessional ettiquete, by the supplier of the implementation technology  like a supplier of chips documents the logical and physical properties of their circuits, but not the internal blueprints.
MATHS & TEMPO help solve several outstanding problems in the software process. First, we can 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 this chapter). In chapters 3, 5 and 6 I will show how we can guarantee that this understanding is accurately modelled 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). Finally practice has added special features(section 6).
Projects that use MATHS can "zeroin" 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. These steps are an exercise in stating the obvious. Facts are recorded and verified by experts and by observation. Simple facts lead to validation of algorithms, data structures, and data bases.
If a system interacts with another system then it will implement an internal model of the external system  even if the producers have failed to document it. However an abstract model of the external system is also a model for the internal system 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. So software design can be based on science. There is also a natural graphic representation (TEMPO). This is, by chapters 0 and 1, a basis for Software Engineering.
. . . . . . . . . ( end of section Chapter 2) <<Contents  End>>