An Algebraic Definition of Simulation Between Programs

1. I~RODUCTION

One aim of this paper is to make precise a sense in which two programs may be said to be realizations of the same algorithm. We can say loosely that for this to be true it is sufficient though perhaps not necessary that the programs do the same 'important' computations in the same sequence, even though they differ in other ways: for example (1) we may disregard other computations perhaps different in the two programs, which are 'unimportant' in the sense that they are only con­ cerned with controlling the 'important' ones, (2 ) the data may flow differently through the variables or registers, !3) the data may be differently represented in the two programs. The program pairs in Figures 1 and 2, studied in detail in Section ~ . illustrate points ( 1) and (3 ) respectively; a trivial illustration of (:) is the following pair of programs:

read x,y

x:= x + y

print x read x,y y:= X+ y print y

Although the above prescription is vague, we give a relation of simulation between programs which may fairly be said to match it. The relation turns out to be transitive and reflexive but not always symmetric; .however mutual simulation is an equiva­ lence relation, and it is the equivalence classes under this relation which may be regarded as al gorithms - at least this is an approximation to a definition of algorithm, We show also that there is a practical technique for proving simulation in interesting cases - though unfortunately simulation between programs handling the integers, for example, is not a decidable (or even partially decidable) relation. Under a simple restriction simulation ensures the equivalence (as partial functions) of the programs, so this is also a technique for proving equivalence; however in general equivalent programs will not satisfy the simulation relation.

vrhi s research was supported mainly by the Science Res earch Council, Great Britain and in part by the Advanced Research Projects Agency of the Department of _Defense : sD-123 ) U.S.A.

I also claim that in order to prove by Floyd's [ 1] method the correctness of a program A, in a case where data is represented unnaturally, perhaps for efficiency's sake, the easiest and most lucid approach is rather close to first designing a program B which is simulated by program A and which represents the data naturally, and then proving B correct. This was in fact the original motivation for studying simulation, and is discussed in more detail in Milner (2], which contains a first attempt at the definition of simulation. The sequel [3] gener­ alizes the definition and the current paper is a synthesis of the two, and may be read independently.

2 . NOTATION

We denote relational composition by juxtaposition; if R S A X B, S S B x C then RS = ( (a,c ) i3b. (a,b )€R , (b,c )ES}. The inverse of R is R-1 = ((b,a)i (a,b )ER}. We intention­ ally confuse a (partial) function F: A~ B with the relation F = ((a,b)lb=F (a )}. R induces a function lmR: 2A ~ 2B; for S =A, lmR (S) = (bl3aES.(a,b)ER}. For a function F we some­ times write FIS) for lmF (S) , The domain of R ;:: A X B is dom R lmR':A) , and the range of R is ran R lmR-1 (B) · For any set A, IA SA X A is the identity relation on A.

3· PROGRA.'-IS AND SIML'LATION

We first introduce a definition of program which enables simulation properties to be stated and proved succinctly.

Definition. A program a is a quadruple (Din' 0 comp' Dout' F) where Din' Dcornp' Dout are disjoint domains and F:D ~ D is a total function (D=D,n U D U D ) with restrictions · comp out

• (i) F(Din U 0comp) S Dcomp U 0out
• (ii ) The restriction of F to Dout is the identity I 0 out

We call Din' Dcomp' Dout the input, computation and output domains of a.

Conditions ( i ) and ( ii ) ensure that starting .with a member of Din and applying F repeatedly we get either an infinite sequence in Dcomp' or a finite sequence in D followed by a single comp repeated member of Dout' We have (ii) merely to keep F total, which the theory requires.

Why must the domains be disjoint? What about a program which inputs an integer and outputs an integer? Here one might argue that Din · Dout =

[integers}; but we get into no trouble having two formally disjoint domains with for example an injection or a bijection between them. In fact, in practice we can distinguish between an input object and an output object of a program; for example they occur on different media, or at different spatial locations. We are concerned with a level of abstraction (i.e. abstraction from real computers operating on physical data symbols) lower than that in which a program is considered as for example a function from integers to integers.

Definition. A computation seguence of a is a sequence (oili 2 o} where d 0 E Din' di+l· F(di), i 2 0, and ~ diE Dcomp' i > 0 £L for some k diE Dcomp' 0 < i < k and di&dkE Dout' i2 k.

Definition. A program a determines its associated partial function

in an obvious way.

Often we would have Dcomp · N X E, where

E is the set of possible state-vector values, and for non-recursive (flowchart) programs N is the finite set of nodes of the flowchart while for recursive programs N is the infinite set of possible states of a pushdown store.

Before dealing with simulation, we state without proof some theorems concerning co~rect· ness and termination of programs. Theorem 3.1 embodies Floyd's [1) method of proving partial correctness of programs, There is also a correspondence with Manna's work - for example in [4); our Theorems 3.1 and 3.2 correspond to Theorems 1 and 2 of that paper. However, Manna is concerned with the representability of verifi­ cations (as defined below) in first order predi­ cate calculus; we perhaps gain in succinctness by stating results algebraically and ignoring the question of representability.

Henceforward we assume that the suffix 'in' to a symbol denoting a set implies inclusion in Din' Similarly for 'comp' and 'out'.

Definitions. a,.. is partially correct w.r.t. sin' sout if a (sin) ~ sout'

a is totally correct w.r.t. in addition A a is total on sin'

s is a verification of a or A, if S C D and F(S) ~ S. S verifies

Theorem 3.1

Given Sin' Sout [a partially correct

[There is a verification of a]

Theorem 3.2

Given [a totally correct w.r.t. Sin' Sout) ~

(For every verification

Corollary. (Set S t = D ) [a total ou out - 1 ... on sin [For every verifications: U s' 1 1 ~n_ comp of a, Sin n S in" 0 => S out" 0 J X: u sout

Definition, Let R CD X D 1 · Then R is a weak simulation of a £¥. a' if

• (i) R C D X D 1 U D X D 1 U D - in in comp comp out x o' out
• (ii) R F 1 c F R.

Condition (ii)-simply states that R is a weak homomorphism between the algebraic structures (D,F) and (D' ,F') , This concept is used in automata theory to define the notion of covering -see for example Ginzburg [7, p. 98].

Now denote R n (Di X Di' ) by R , and n n in define Rcomp' Rout similarly, so that R = Rin U R U R comp out and these parts are disjoint.

Theorem 3·3·

• If R is a weak simulation of a by a' then ( i) R a, caR
• (ii) -1 R is a weak simulation of a' by a
• in - out
• (iii) R-1 ac 0 1 R-l in - out

~ (i) The condition R F' S F R may be restated

Vd,d', (d,d') E R => (F (d) ,F 1 (d')) E R ( · ) Now suppose (d 0 ,d~) ERin cr. Then for some d~, (d 0 ,d~) ERin and 0 1 ( d~) · d~, so there is a t i d / d 1 d 1 I compu at on sequence 0 , 1 ······· , k, ······· of 0. Now consider the computation sequence d 0 ,d 1 , .·· ,dk'''''of a. We may prove by induction using (*) that (di,d~) E R, i ~ 0. Hence dkE Dout' ( d 0 ,dk) E ~ (dk,d~ )E Rout and so (d 0 ,d~) E a Rout

• ( ii) It is enough to show R-1 F SF' R-1, But this follows easily from the fact that (*) is equivalent to RF' S FR.

(iii) Follows di-rectly using (i) and (ii), ~ Theorem 3.3(i) says that the diagram

semi-commutes ( i.e. in ( i) we haveS not=). If we wish to be able to use r.f to do the iob of a, we need more: we need the following to commute

i.e. we require 0 = Rin J' R-1 · Theorem 3,4 out below shows that for this it is sufficient to require R to be a strong simulation of a by a', where

Definition. A weak simulation R of is a strong simulation if in addition R;~t are total and single valued, a by a' Rin and

~ote that R-1 is not necessarily a strong simulation of a' by a, so unlike weak simu­ lation, strong simulation is not symmetric,

Theorem 3.4

Proof ( ~ ) Post multiply Theorem 3 .3 (i ) by R 0 -ult and use R R-1 S I 0 (R-1 single valued ) . out out out out

R. and use I 0 c Ri Ri-1 (Rin total).

1n in - n n

~

(Note that in the above we did not use the totality

Let us return to the discussion of algorithm in the introduction. If there is a strong simulation of a by a' we say a' strongly ~­ ~ a, and it is easy to show that this is a transitive reflexive relation, i.e., a quasi­ ordering. ~strong simulation is therefore an equivalence relation, and equivalence classes may be thought of as algorithms, each of which 'is realized by its member programs. Moreover, if we divide out by this equivalence relation we obtain from the quasi-ordering of programs a partial ordering of algorithms.

It is worth noticing that there is always a weak simulation between any pair of programs - just take R · ¢ - so a similar definition of "a' weakly simulates a" is vacuous.

We finish this section with two simple results which exhibit the close relationship between verifications and simulations.

Theorem ~-~

If R is a simulation of a by a' then

( i ) dom R verifies a

( ii ) ran R verifies 17'

Rr2£i In view of Theorem 3·3( ii ) we only prove (i ) . Clearly domR S D, and we only need show F(domR ) £ domR, i.e. Vd. dE domR = F(d) E domR. But dE domR =>3d', (d,d 1 ) E R

This theorem says that simulation of a ~y a' implies the partial correctness of a w.r.t. domRin' domRout' However, normally we are interested in partial correctness w.r.t an Sin' Sout where Sout is much smaller than domRout; for example if Rout is total then domRout ~ Dout' and a is always partially correct w.r.t. Sin' Sout when Sout = Dout

Theorem 3.6

If s of a by verifies a and R is a simulation a' then ImR (S) verifies a'.

Thus in a precise sense a proof of partial correctness of t7 1 may be factored into a proof of partial correctness of t7 together with a proof of simulation of a by a'.

4 . APPLICATION TO FLOWCHART PROGRAMS

In this section, we show how we may demonstrate a simulation between two programs in a manner which bears a close relation to Floyd's method for proving correctness of a single program. Of the two examples, the first has the same data representation but dif· ferent control in the two programs; the second has different data representations in the two programs.

Given a flowchart program with input domain Di n,

state-vector domain E, output domain Dout and nodeset N, and given also an input function fin:Din~ E and output function fout:E ~ Dout' it is a simple matter to formalize it as a program according to our definition, with D "' N x E and F:D ~ D comp defined in terms of fin'fout and the tests and assignments in the boxes. Alternatively, we may formalize it by selecting a subset M c N so that every cycle in the flowchart contains ; member of M (we call such an M a cycle-breaking set ) and define D instead as M x E. The cycle camp breaking property ensures that F D ~ D is again ~·

Now suppose in a and a' we have D " comp M X E, D 1 = M 1 X E' , a and a' may have comp been obtained by the above formalization from flow­ chart programs, for example. If R is a simulation of a by a' , we have R C (M x E) X comp - (M 1 x E') , and to exhibit to exhibit R I for each R canp it is sufficient mE M, m'E M' where

mrn

In t he following two examples we exhibit the Rmm and also indicate how the proof of RF' c FR would go.

Example 1. : See Figure 1 ) . Assume that inputs to each program are pairs (n, x) , state vectors are triples (i,n,x) , and onl y x is output, The node-set { l. ~j ha s been chosen to formalize a, and { 1 1 . ~ I,;') t o formalize a'. So if .;,,;; denote integers and reals we have

and f , given by f(d ) = if the transition functio~ for a. is d£:) t hen (1, (O,n , x \'whe re (n, x \ = d

elseif dE D thenm (m, ( i,n,x)) cd; comp ll i + 1 < 3n ~ (m,(i + l,n,g l x))) else if + 1< ~ n then ( ~ , ( i + l,n, else g x ) else d.-- F1 to-;--(;' is de f ined similarly, g 'x))\

We postulate a simulation R Ri , R and R 1 for (m,m') n out mm by giving 2 ',3'}, as follows:

For example, we may think of R 12 , as containing all state-vector pairs attained at the node-pair (1,2 1 ) when a.~ are obeyed synchronously starting from an input pair in Rin' However, it contains also many other state-vector pairs (since there is no constraint on x in the definition of R 12 , ) , and simulation will normally have this generous property. R 13 , is here taken as the empty set, because the node pair ( 1, 3 ' ) is never reached.

d,d I To prove RF' S fR we must show for a l l (d,d') E R (f \d ) ,F 1 (d') ) € R

and this may be done by cases

which is a fairl y routine matter using the defi n· itions of f,f', and we leave it to the reader .

Now since R is a strong simulation, a nd indeed Rin' Rout are identities, Theorerr. ; .-

entitles us to conclude 8 = ()'.

Example ~ . ·: see figure ::) . This exa r:1ple illustrates simulation between two programs with different data representation, ~e describe this example in less detail, to save space. Each program is supposed to input a string c, a character ~ and a string T, and t ~ output the result of substituting T for ~ everywhere i n c . Thus if S is the alphabet of characters , Din = Din "' s~ X S X s- (where s - is the set

of strings over s ) and D "D' = s-. out out Program a handles strings and characters directly, using the functions hd,tl, < > (concatenation: and the null string t· The three inputs are to the program variables c 0 , ~. ~ 0 respectivel y ,

and output is from the variable c~ . On the other hand, program ~' represents each string as a segment of an integer-indexed character array; on input the two input strings are stored in arrays s, t ( indexed from 1) , their lengths + in integer variables hl,kl and the character in x, and output is the string ss ( l),ss (2 ) ····· ss (hh­ l ) .

The flowcharts are formalized as programs ( in our sense) with node-sets ( 1,2}, ( 1' ,2 '}, and we have D · (1,2} x (the set of possible camp values for the program variable vector of a}, and similarly for o' · F and F', the transition comp functions, are easy but tedious to define. We now exhibit a simulation by giving Rin' Rout and (1',2'), using the RDDD, for (m,m')E (1,2) x an auxiliary function seq; arrays x integers x integers ~ strings defined by

Now as in Example 1 the proof of RF' ~ FR must proceed by cases; it will use certain p;opert· ies {or axioms ) concerning the string handling funct i ons, the array and integer handling functions and the function seq. We leave it to the reader again. Again, since Ri n'·Rout are identities we have proved that a= f1'.

There are some interesting points about this example. (1) It seems t hat program a is more natural than ~, though t his asymmetry was not present in Example 1. In fact, program a' is only a slight modification of part of a real program written for use rather than as an example. In the process of proving t7' correct :see ~ ~] ) using Floyd's technique, I found that the assert· ions associated with parts of the program were most naturally expressed using the function seq. Also : this is discussed in more detail in [ ~ )) the task of proving eJ' correct factored sL'llply into two tasks - that of proving ~ correct , an easier task since a is more natural and closer to programmer's intuition) and that of proving the simulation. Th is 'factoring' was made precise by Theor em ; .t .

(i 1 Unlike i n Example 1, t he flowcharts here have i dentical shape , and it is meaningful and even tr ue! ) to say t hat under identical inputs t he programs follow the same path. In Example 1 such a statement would not be meaningful,but in Section 5 we show that a similar statement has meaning in cases more general then Example 2 , and provides us with necessary and sufficient conditions for the existence of a simulation between two programs,

5. PARTITIONED SIMULATION

lle now obtain necessary and sufficient conditions for the existence of simulation between two programs a and C7' ·

pefinition. If J is any indexing set and TTJ · {cjjjEJ} ,rr; · (cjJjE J) are partitions of Dcomp' D~omp respectively, then (ITJ,TT~ ) is a partition pair for D , D' (Of course any two domains comp comp can have a partition pair, but we are only concerned with computation domains ) .

Theorem ; .1

~ Weak Simulation Theorem) . Given D. x D ~ and a partition pair (TTJ,nJ') ~n 1n Dcomp' D~omp' the following two statements are equivalent:

• a ) Computation sequences ( di} of a. ( d~} of a' far which (do ,clc'\E R~ always agree for ~n ( ITJ,T"~ ) ,

(b) There is a weak simulation R = R~ ~n R of a by a' which respects out I ' R ~ camp ( ,.,. ,.,. , ' 'J . J ' .

Proof :a ) = ( b ~ · It is enough t o take R = { ( e ,e 1 \ I There are computation sequences [ di} of a, ( d~ } of C7' for which (do .dci ) e=d e'=d'l and for some k k 0 k . · E R ~ ~n

1 b) = ~ a ) . Assume R. ' { d ' I f ) computat1on sequence i J , l di ' Take any for which (do ,dci )E R. Then we 1n have ~i ( di,d~ )E R since R is a simulation, so either ( di,d~ \E R" ~ n l R for j SJ d .EC. and d'::: I out or some . ~ C. 1 J 1 J since R respects ('TJ ,TT~ \ . Thus (a ) follows.

Theorem 5.::

+ (Strong Simulation Theorem) . Given Rin ,.... D x D 1 R ~-D D 1 ·-·1'th R-::. in in' out - out x out ~ in' R+-1 both single-valued and total, and (" ~' \ out' J' J a partition pair of D D' the follo1.ring comp' comp' two statements are equivalent:

: a ~ o= R+ in ~I R~:~. and computation sequeoc:es ( di} of '7. ( d 'i i' of t7' for which (de ,d( ) :: R. always agree for <~J'"T; ) . 1n

R = R7" (b ) There is a strong simulation 1n Rof t7 by a' which respects out R comp (rJ',.;'> ·

.f!:..Q£1 ~ a ) = (b) . By the corresponding proof in Theorem ; .1 there is a simulation R7" R 1n comp R wnich respects (~J ,rJ' \ , and for which out

( e,e' ~~ Rout For some ( d,d 1 \~ R~n ' e = ~( d ) and e '= C (d 1 )

(e ,e 1 \ ~ R~ut' A = since '7=

R-.; o' R --1 1n out and both R~ and 1n a'

are single valued.

Thus R = R. whence R~ ..: R out out' 1n comp is also a simulation respecting (-J,-'' ~ R* out and moreover a strong one, from the conditions Theorem. (b ) ,. (a ). Take any dot Din · and -' 1 - R· (-' \ This is defined since R.in ~- in ,u.c , . of the is total. Then by Theorem ;.1 t he computation sequences [di}, (d~ } agree for (~J'"T~ ) . It follo~s also from this that either both or neither of a (dc ) , 8' \dci ) are defined. If neither, then neither of the functions O, R~ 3'' R"-l is 1n out defined for d:. . If both , then for some d' ) ~ R. and d = a:d,. \ d 1 =~I ' d} ', k out k - ' ' k - · · k (dk, But d = R·-1 (d') and d( = R~ de. ) so the functions k out k 1n 0, R~ ~R·-1 both yield result dk for argument 1n out do, since R·-tl is single valued. ou

(Note that this proof nowhere uses the totality of R"-1 )

1n out out

Now the coarsest partition pair (~J.rr; \ has J a singleton and ~ simulation respects it. \,'e therefore have the following corollary to Theorem 5.1.

Corollary " 2 <. ( · lation .. R = R. 1n Given R~n R comp there is a weak simuR of t7 by a' out if and only if computation sequences [ di} in a,(d~ } in a' such that (de ,d:' \~ R~n ahvays have length ~ither both undefined or equal 1 the length of , ... i} is defined as min{kJ dk~ D } ) · out

:X

There is a corresponding corollary to Theorem ; . ~ .which we omit.

Finally, we give a corollary for flowchart programs of the sa~e shape.

Corollary ; .- . Let D ~ Y E D' comp ' cornp ?'\ / E'; call ~ th~ node set :fomrnon t? t7 and a' ). Define c:\ = ~{n} 1. Ejn~ :\;. r:~ = · {n) y E'Jn:: ~· . Then two computation sequences agree for ( ~.\' ,..~ ' exactly when they trace the sane node path, and so we have the following:

Given R~n' there is a weak simulation R = R 1 ~n R R of 0 by a' which comp ou.t respects (-:--; ·~~ ) if and only computation sequences [ di} in if every pair of '7, ( d ~ ~ in t7' l ' such that trace t he same node pat h . ;;

Again, there is a corresponding corollary to Theore~ 5 . ~ . If as in Section- we exhi bit R bv exhibiting R 1 E Y E 1 f or comp · nn - I.- " th "R t ( ..,. -I \ II n,n -:. ·' · en respec s _ :--; · ~ means Rnn' c. r, Example _ n c n'. This is the situation in of that Section.

i: . CO~CLVS IO~;s A~;n POSSIBLE DEVELO!'>fE ::-IS

The idea of simulation, which is really an application of the not ion of weak homomorphisr.. , is interesting in two ways : theoretically , because it allows one to abstract some irrelevant detail from programs to come closer to a defi ni t io~ of algorithm, and practically because there i s a manageable technique for proving simulation between programs, which in some cases may make easier the task of proving a program correct.

There are two possible directions for development. First, we have restricted to a single-valued, total transition function F. The situation looks rather different when we relax these conditions - for example we should consider computation~ rather than sequences. Second , we should consider simulation of parallel progra~s. and treat programs which perform the same compu­ tations but not necessarily in the same sequence as serializations of the same parallel progran - or of mutually simulating parallel programs. These extensions may bear the same relation to the wor k of Manna [5) and Ashcroft and Manna [~) on the correctness of nondeterministic and parallel programs as the present paper bears to Manna's work on serial programs i - J.

ACKNOWLEDGEMENTS

This work owes much to Peter Landin who largely pioneered the algebraic approach to programs. This paper is in the spirit of [8), although that paper is concerned with the structure of a single program (as a product algebra ) rather than relations between programs. I also had profitable discussions with Peter Landin, Rod

Burstall and John Laski.