- Dynamics and Relationships
- : Copyright
- : Program Specifications
- : Dynamic Predicates
- : Binary Relations
- : Example: Family Relationships
- : Inductive Invariants
- : Loops
- : Program Structures
- : Logical Programming?
- : Reasoning about Programs
- : Footnotes
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- C A R (Tony) Hoare
- Assertions: A Personal Perspective
- IEEE Annals of the History of Computing V?n?(Apr/Jun 2003)pp14-25 [ dlib ]
- x'=x+y
After the statement, the value of x is equal to the sum of the old values of x and y. Also, y is unchanged. It could be coded as x:=x+y in Ada/Pascal/... The semantic rule is that "a prime means the new and no prime means the old" [Ross Ashby 56, Part II of Lam & Shankar 90, compare Hehner 84a & 84b, Guttag & Horning 91, Steward 93]. Formally x'=x+y defines a relation on a structured set with variables x and y. So

- x'=1
guarantees that x is 1 afterwards and also that no other variables change.

- x'=1-x
means that the value of x will be complemented - its new value will be the result of subtracting its old value from one while all other variables stay the same.

- x=1
has no primed variable. It means that x has the value one, and does not change - all variables are left untouched. It is a relation that holds between identical states when and only when x has value 1. It filters out all states when x is not 1. It allows computation under a condition. We call it a condition therefore. It can be shown that it is a condition in the sense of Arbib and Manes [87].

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

- S::=$ Net{x1:X1,x2:X2,...,x[m]:X[m]}.
Let P(y1',y2',y3',...y[n]',x1,x2,x3,...x[m]) be a predicate with n distinct primed variables(y1, y2,...y[n]) which also may also appear without primes as xs. For example in x'=x+y, x1=x, x2=y, and y1=x.

The relation defined by P(y1', y2', y3', ...y[n]', x1, x2, x3, ...x[m]) is found by: (1) Replacing primed variables (y1,...) by values in the new state(s2), and (2) Replacing non_primed variables(x1,...) by values in the old state(s1), and (3) Adding the requirement that the static (unprimed) variables do not change. So:

- P(y1',y2',y3',...y[n]',x1,x2,x3,...x[m])::= rel [s1:S, s2:S]( P(s2.y1, s2.y2, ..., s2.y[n], s1.x1, s1.x2, ...,s1.x[m] ) and for all i:1..m where x[i] not in {y1, y2, ..., y[n]}, s2.x[i]=s1.x[i]).
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

- a*x'+b*y'=c and d*x'+e*y'=f.
To specify a process that solves a quadratic equation we write

- a*x'^2+b*x'+c=0.
On the other hand

- a'*x^2+b'*x+c'=0,
specifies that x is left alone and a, b, and c are adjusted to fit the equation.

## Binary Relations

@(T1,T2) symbolizes the relations between T1 and T2. A relation in R:@(T1,T2) can be defined by - For x:T1, y:T2, x R y::@= W(x,y).
or equivalently by

- For R::@(T1,T2)= W((1st), (2nd)).
/R is the converse relation to R. For example if (_^2) is the 'square' function then /(_^2) is the square root relation. Similarly the arc sine function is written /sin. Further we want /parent_of=child_of. MATHS defines

- For R:@(T1,T2), /R::@(T2,T1)= (2nd) R (1st).
Given two binary relations R and S then

R; S = The relation between (1st) and (2nd) where for some z, (1st) R z S (2nd),

R | S = The relation between (1st) and (2nd) where either (1st) R (2nd) or (1st) S (2nd),

R & S = The relation between (1st) and (2nd) where both (1st) R (2nd) and (1st)S (2nd). - For R: @(T1,T2), S:@(T2,T3), R;S::@(T1,T3)= rel[x:T1,y:T3](for some z:T2 (x R z and z S y)),
- S o R::@(T1,T3)= R;S.
- R::@(T1><T2)= {(x,y):T1><T2 || x R y }.
In context, a set can also be used as a relation:

- For A:@T, A::@(T,T)=rel[x:T, y:T](x in A and x=y).
## Example: Family Relationships

Its surprising how quickly you can define even complex situations using these notations:- ... male, female::@being.
- parent::@(being,being)=(1st)is a parent of(2nd).
- ...
- child_of::=/parent.
- father::=male;parent.
- mother::=female;parent.
- son::=male;child_of.
- daughter::=female;child_of.
- grandfather::=father;parent.
- ...
- granddaughter::=daughter;child_of.
- grandson::=son;child_of.
- ...
- sibling::@(being,being)= (/parent;parent) ~ (=).
- -- I am not my own sibling!
- sister::=female;sibling.
- ...
- uncle::=brother;parent.
- ...
- niece::=daughter;sibling.
- first_cousin::=/parent;sibling;parent.
- second_cousin::=/parent;/parent;sibling;parent;parent.
- lineal_descendant::= child_of | lineal_descendent; child_of,
- ancestor::=parent | parent; ancestor
- cousin::=/parent;sibling;parent | /parent;cousin;parent,
- first_cousin_once_removed::=/parent;first_cousin | first_cousin;parent.
- [From Logic.Natural.KINSHIP]
- ...

## Inductive Invariants

The last four definitions above are like productions in context free grammar. The definitions of ancestor and lineal_descendant illustrate the transitive closure or ancestral relation. It is so common that a special notation is defined: x do(R) y::= x=y, or x R y or x R;R y, or....Example:

- (above)|-ancestor=parent; do(parent) and lineal_descendant=child_of; do(child_of).
The defining property of do is that if something is invariant (or fixed, or closed) under R then it will not be changed by any number of Rs[footnote1]:

- inv(R)::= the invariants of R
- inv(R)::=the sets X such that if x in X and x R y then y in X.
Example: families::=inv(parent).
- |-For R:@(X,X), F:@X, if F.R ⊆ F then F in inv(R) and F.do(R) ⊆ F.
- Example: families.do(parent) ⊆ families.
Similar to the idea of an invariant set of states is the idea of an stable variable of function:

- stable(R)::=The stable functions under R
- stable(R)::=the functions f such that R;f=f
and, so if f in stable(R) then f in stable(do(R)). Also for all R and f, f is
stable under not(R).
## Loops

Consider the following expression: - SUM::=(n'=1 and s'=0; do(n<>101; s'=s+n and n'=n+1); n=101).
The definition for SUM looks like a program but is an expression in the calculus of relations [Whitehead & Russell]and so has provable properties. First since the (+) is defined to be an operator on numbers, so the state space is ${n,s:Numbers}. Next define names for the parts of SUM:

- S::=(n'=1 and s'=0).
- L::=(s'=s+n and n'=n+1).
- E::=(n=101). W::=not E.
- (S, L, E)|- (eq1): SUM= (S; do(W; L); E).
Now s is stable under E:

- (above)|-E ⊆ (s'=s),
or
- (above)|-E ==> (s'=s).
and after E we know that n=101 because

- (above)|-post(E)=img(E)={ x :X || x.n=101}.
Similarly after S we know that n=1 and s=0. Further W by definition will not change s and n. Next we look for something that does not change in L. Both s and n change - in parallel:

- (above)|-L = ( (s',n')=(s+n,n+1) ).
With a little creativity or experience we discover the following invariant set of L:

- F::= ( s=1+2+3+4+...+(n-1)).
- (above)|-F; L ⊆ F,
- (above)|-F in inv(L).
Similarly

- (above)|-F in inv(W) and inv(E),
so

- (above)|-F in inv(W;L).
Thus

- (above)|-(F; do(W; L)) ⊆ F.
Now

- (above)|-S ⊆ F and F;E ⊆ F.
so

- (above)|-SUM = (S; do(W; L); E) ⊆ F and n'=101
Hence, after SUM, s= 1+2+3+4+...+(n-1) where n=101 = 5050.

Notice that MATHS is not a programming language. So

- x (do(W; L)) y
is not the same as

- x (do(W; L); E) y.
In the first case y.n can have many values. In the second y.n will be 101. Similarly, when

- x ( i=1; i'=2 | i'=3 ) y
permits y.i=2 even if i<>1, but if x.i=1 then y.i MUST be 2. Whatever happens y.i is either 2 or 3. Such non-determinism seems to be essential for a simple model of processes[Dijkstra 76, Hoare 78, Hoare 85, Gabrielian & Franklin 91].

## Program Structures

MATHS includes structured programs because - For R:@(S,S), no(R)::@(S,S)= ((1st)=(2nd) and for no y((1st) R y).
- For A:@S, R:@(S,S), while(A)(R) ::=(do(A; R); no(A)),
- For I,J,K:@(S,S),R:@(S,S), for(I, J, K)(R) ::=(I; while(J) ( (R); K ) ),
- For A:@S, R,T:@(S,S), (if A then R else T fi) ::=(A; R | no A; T).
We can, for example, when n<=m define:

- SUM(f, i, n, m, s)::=for(i'=n, i<=m, i'=i+1)(s'=s+f(i))
and show

- (above)|-SUM(f, i, n, m+1, s) = SUM(f, i, n, m, t) and s=t+f(m+1).
MATHS includes 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:

- ADA_PDL::= Net{
- ...
- For A,B,C:@(S,S), loop A; exit when B; C; end loop::= (do ( A; no(B); C); (A; B) ).
- ...

}=::ADA_PDL.MATHS can express mixtures of conditions and actions in one relation. A well known enigmatic program is often written:

- Enigma::= ( while(n>1) (
- if n in even then n'=n/2
- else n'=3n+1
- fi
- )
).
In MATHS it can be transformed:

- |-Enigma=while(n>1)( 2*n'=n | 2*n'=3*n+1 ).
## Logical Programming?

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, (1) give non-deterministic relationships and reduces them to a form that is compatible with a declarative programming system such as Prolog [Compare Lamport 87].## Reasoning about Programs

Finally, MATHS relational expressions follow the calculus of relations which can be used to simplify sequences into disjunctive normal form, like the following: - R = A1 and A2 and A3 and... or B1 and B2 and... or...
These relations can then be expressed as and/or tables.

Typical rules are:

Net- |- (dist): R;(S|T) = (R;S) | (R;T).
- |- (cond1): (P(x, y); Q(x, y, y')) = (P(x, y) and Q(x, y, y')).
- (cond1)|- (condassign): (Q(x, y); x'=e(x, y) ) = (x'=e(x, y) and Q(x , y)).
- |- (assign): (x'=e(x, y); Q(x, y, y')) = (x'=e(x, y) and Q(e(x, y), y, y')).

(End of Net)

## Footnotes

(footnote1): Originally in Whitehead and Russell's Principia, the same form is in Floyd's loop invariant technique and reminiscent of Kleene closure in grammar theory. The definition relies on using higher order quantifiers[cf Guerevich 87].

(footnote2): In theory a better specification of a piece of a program has two relations. The first indicates when the program can be safely used. When the relation holds it does not effect the state of the program. When is does not hold the program has no specified behavior and may not even terminate. The second relation indicates the changes that may occur when the first relation is true and the relation is safe to use. This comes from Parnas's work.I plan to expand on this later. I envisage modeling a program as a collection of relations describing when it is safe to use, what resources will be demanded for it to work, and the actual effect of the program.

- |- (dist): R;(S|T) = (R;S) | (R;T).
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.

This is part of Chapter 2 of a research monograph tentatively entitled "MATHS for Software Engineering".

MATHS relations can be written in a form that makes them look like statements in a programming language. Some syntactic sugar is defined for those who want to write while/for/loops/. . . . The key definition is that of a dynamic predicate. Here is an introduction. Formal treatment comes later when we have the techniques [ [ math_14_Dynamics.html ] [ math_75_Programs.html ] ].

The MATHS approach is very similar to the ones that Tony Hoare evolved:

. . . . . . . . . ( end of section Dynamics and Relationships) <<Contents | End>>

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

For a more rigorous description of the standard notations see