.Open Dynamics and Relationships
. Copyright
Richard J Botting 2003
.See http://www/dick/
You may link to the whole of this document.
All other rights are reserved.
This is part of Chapter 2 of a research
monograph tentatively entitled "MATHS for Software Engineering".
. Program Specifications
Relations behave like the operations and conditions in a programming language
because each operation in a program relates the current state to the set of
possible future states. If there was always a single next state then the
relation is deterministic, and by composing deterministic steps carefully we
get an algorithm. In turn an algorithm can be coded for input to a suitable
translator giving an executable program. Thus a relation describes a set of
acceptable behaviors and the implementor selects a particular algorithm
[compare with Kowalski, Hoare 87]. For a dissenting view see $footnote2.
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 [
.See ./math_14_Dynamics.html
.See ./math_75_Programs.html
].
The MATHS approach is very similar to the ones that Tony Hoare
evolved:
.Set
C A R (Tony) Hoare
Assertions: A Personal Perspective
IEEE Annals of the History of Computing V?n?(Apr/Jun 2003)pp14-25
.See http://computer.org/publications/dlib
.Close.Set
. Dynamic Predicates
A predicate is a proposition that has free variables. A dynamic predicate has
free variables with primes (') attached to them. Here is an example:
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
`x`s. 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>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`:
()|- E \subseteq (s'=s),
or
()|- E ==> (s'=s).
and after `E` we know that `n=101` because
()|- 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:
()|- 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)).
()|- F; L \subseteq F,
()|- F in inv(L).
Similarly
()|- F in inv(W) and inv(E),
so
()|- F in inv(W;L).
Thus
()|- (F; do(W; L)) \subseteq F.
Now
()|- S \subseteq F and F;E \subseteq F.
so
()|- SUM = (S; do(W; L); E) \subseteq 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
()|- 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')).
.Close.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.
.Close Dynamics and Relationships