Formal Proof Systems for Program Equivalence.
Jan Aldert Bergstra, Jan Willem Klop · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1982
We explore conservative refinements of specifications.These form an appropriate framework for a proof theory for program equivalence that is based on a logic for partial program correctness.We propose two formalized proof methods for program equivalence (inclusion).Both are sound w.r.t. the most general semantics of first order specifications.In spite of being incomplete the methods cover many natural examples.(2) Alg(l:,T) F (p}S2{q}Alg(E,T) F {p)S 1 {q}, for all p,q E L(l:).However, there is no reason to expect that the reverse implication (2) =>(I) will hold, since (2) states only roughly that S C s 2 , where 'roughly' refers to the limited expressive power of L(E).(In fact~ one can show that indeed (2) ./>(I).)Now considerthen the reducts of (E',T')-algebras to E form a subset of Alg(E,T); hence Alg(E,T) F sl s s2 .. Alg(l:',T') F SI s S2")In fact we will restrict our attention to a subclass of all refinements (;,) of (l:, T), namely to the conseY'vative refinements (12) of (E, T), f.or reasons which will be clear later.So consider (4) V(l:',T') C: (l:,T) Vp,q c L(l:')Now we have (I)=> ( 3) => (4) => (2); and it can be shown that ( 4) => ( 1).The conclusion is that one can treat the 'semantical' inclusion (1) by considering only first order properties of s 1 , Sz (i.e.asserted programs {p}Si{q}, i = 1,2), provided one is willing to consider not only (E,T), but all its (conservative) refinements.This observation prepares the way for an approach via Hoare's logic of proving asserted programs.First of all, define (5) s 1 SHL(E,T) s 2 iff Vp,q E L(E) HL(l:,T) f-{p}S 2 {q} => HL(E,T) f-{p}S 1 [q} (proo ftheoretica l inclusion) and consider (6) vci:• ,T'J e: (E,T) sl SHL(E' ,T'l s2 (derivable inclusion)the prooftheoretical analogue of (4).Indeed, it will turn out that this 'deri- vable' inclusion, written as HL(E,T) fs 1 ,S s 2 , implies the semantical inclusion (I).This is our first "proof system" for proving semantical inclusion; we will prove that (6), as a relation of s 1 , s 2 , is semi-decidable in T.