A Semantic Basis for Local Reasoning
Hongseok Yang1and Peter O’Hearn2
1ROPAS,KAIST
2Queen Mary,University of London
Abstract.We present a semantic analysis of a recently proposed for-
malism for local reasoning,where a speci?cation(and hence proof)can
concentrate on only those cells that a program accesses.Our main results
are the soundness and,in a sense,completeness of a rule that allows frame
axioms,which describe invariant properties of portions of heap memory,
to be inferred automatically;thus,these axioms can be avoided when
writing speci?cations.
1Introduction
The need to say what memory cells or other resources are not changed,along with those that are,has always been a vexing problem in program speci?cation.
Consider a speci?cation of a program to copy a tree:
treeτp CopyTree(p;q) (treeτp)?(treeτq) .
Here,the parameter list indicates that p is a value and q a reference parameter. The predicate treeτp says that p is,or points to,a data structure representing a binary treeτ,and(anticipating the work to come)(treeτp)?(treeτq)says that p and q both represent this tree,but that their representations utilize disjoint storage.
This speci?cation certainly captures part of what we intend to say about the procedure.But a Hoare triple typically only describes the e?ects an action has on the portion of program store it explicitly mentions;it does not say what cells among those not mentioned remain unchanged.As a result,the speci?cation of CopyTree(p;q)leaves open the possibility that the procedure alters a cell not in the data structure described in the precondition.To make a stronger speci?cation we need to,in one way or another,take into account the notorious “frame axioms”[8],which describe cells that remain unchanged.
It might seem that this problem is just a nuisance,that we should be con-tent for practical purposes to prove weak properties and not worry about frame axioms.This viewpoint is untenable,for the following reason.At a call site for CopyTree(p;q)there will often be more cells active than those in p’s data structure.In that case the speci?cation is not strong enough to use,unless we somehow take the frame axioms into account.A particular example of such a call site is in the body of a recursive de?nition of CopyTree(p;q),which uses recursive calls for each of two subtrees.As explained in[5],if we do not have
some way of showing that each recursive call doesn’t a?ect the other,then the speci?cation will not be strong enough to use as an induction hypothesis when proving the program.
It might alternatively be thought that the problem can be easily solved, simply by listing the variables that a program might alter as part of the spec-i?cation.This viewpoint is untenable when there are storage cells other than those directly named by variables,typically when there are pointers of one form or another.This solution is thus not applicable to realistic imperative languages.
Nonetheless,although much more than a nuisance,this frame problem is still irritating.It seems unfortunate to have to think up a general formula to function as a description of the cells left unchanged,covering all potential call sites,when-ever we write a speci?cation.And intuitively the speci?cation of CopyTree(p;q), for instance,seems to already carry enough information.The hitch is that for this intuition to be realized we need to somehow require that any state alteration not explicitly mandated by the speci?cation is excluded.
Unfortunately,this last part,that“any state alteration not explicitly man-dated by the speci?cation is excluded”is di?cult to make precise,and that di?culty has spawned hundreds of papers in AI and in program speci?cation. Twice unfortunately,no completely convincing solution has emerged.
In this paper we study the semantics of an approach recently developed in an extension of Hoare’s logic for reasoning about mutable data structures[5]. The scope of the approach is modest in intent,in that it is not put forward as a general solution to the frame problem.Rather,the suggestion is that,when certain assumptions are met,there is a natural and simple way to avoid frame axioms.Although,as we further demonstrate here,these assumptions are met in some natural models of imperative languages,there is no claim that they are universally applicable in reasoning about action.
The general idea is that by focusing on the idea of the memory footprint of a program we can get a concrete handle on the resources that a speci?cation of a program needs to describe.More speci?cally,there are two components to the approach.
1.We interpret a speci?cation{P}C{Q}so that,when C is run in a state
satisfying P,it must dereference only those cells guaranteed to exist by P or allocated during execution.
2.An inference rule,the Frame Rule,lets us obtain{P?R}C{Q?R}from
the initial speci?cation{P}C{Q}of a procedure or command,where P?R is true just when P and R are true of separate areas of the current heap memory.
Point1is reminiscent of the old informal idea of a tight interpretation of spec-i?cations:we assume that a speci?cation mentions all the resources relevant to understanding a program,that other resources are automatically una?ected. With it the speci?cation of the CopyTree procedure above implies that any ac-tive cell not in p’s tree before execution will remain unchanged;this allows us to avoid explicit frame axioms and instead work with the simple speci?cation.Point
2
2then gives us a proof method that enables us to infer the invariant properties supported by tightness.
We stress that the?rst of these points does not depend on the second.Given the tight interpretation,a host of invariant properties are simply true,and this is independent of the language used to describe pre and postconditions.The?connective just gives us a direct way to exploit tightness,in a program logic.
The purpose of this paper is to provide a semantic analysis of these ideas. The basic conception of the interplay between points1and2above as a basis for local reasoning is due to the second author.Many of the semantic foundations, particularly those related to completeness described later,were?rst worked out thoroughly by the?rst author.We refer to the precursor papers[9,2,5]for exam-ples of reasoning with the spatial formalism,for program logic axioms for speci?c heap-altering and accessing commands,and for references to the literature on program logic and on the frame problem(see also[8]).
The?rst problem we tackle is the soundness of the Frame Rule.This turns out to be surprisingly delicate,and it is not di?cult to?nd situations where the rule doesn’t work.So a careful treatment of soundness,appealing to the semantics of a speci?c language,is essential.We phrase our argument here in terms of a model devised by Reynolds[10,5],for an extension of the language of while programs with operations for pointer manipulation,including address arithmetic.
In the course of proving soundness we will attempt to isolate the properties on which it relies.Once these properties are established,much of the work in this paper can be carried out at a more abstract level and we sketch the appropriate de?nitions.But a thorough abstract account will be left for other work;here our goal is to remain concrete and provide a detailed analysis of a single language.
After showing soundness we move on to prove a completeness result,which shows a sense in which no frame axioms are missing.Our approach to complete-ness follows a line of work which goes under the name of sharpness or adaptation completeness[4].There one of the main issues is always to conclude certain in-variant properties of variables not free in a command.Our completeness result can be seen as extending such results to handle the heap as well,where there are other store locations than those associated with program variables.The key idea for proving completeness is to view commands as predicate transformers satisfying a locality property.
2A Programming Language
The programming language is an extension of the language of while programs, with operations for manipulating pointers in a heap.The syntax and domains for the language are in Table1.
The model has two components,the store and the heap.The store is a map-ping from variables to integers,and the heap is a?nite mapping from natural numbers(addresses)to integers.The heap is accessed using indirect addressing [E]where E is an arithmetic expression.
3
Syntax
C::=x:=E|x:=[E]|[E]:=F|x:=cons(E1,...,E n)|dispose(E) |C;C|while B C|if B then C else C
E,F::=x,y,...|0|1|E+F|E×F|E?F
B::=false|B?B|E=F|E Domains Nats?={0,1,...,17,...}Ints?={...,?17,...,?1,0,1,...,17,...} Variables?={x,y,...}Stores?=Variables→Ints Heaps?=Nats ?n Ints States?=Stores×Heaps Functionality of Expressions [[E]]s∈Ints[[B]]s∈{true,false}(where s∈Stores) Table1.Syntax and Domains We assume the standard denotational semantics of integer and boolean ex-pressions.Note that expressions are heap-independent. The crucial operation on heaps is disjoint combination.We write h#h to indicate that the domains dom(h)and dom(h )are disjoint.When h#h holds, h?h is the heap obtained by taking the union of disjoint partial functions.When h#h does not hold,h?h is unde?ned.The empty heap[]is the unit of?.The notation[n→m]describes the singleton heap which maps n to m and which is unde?ned everywhere else. The operational semantics of commands de?nes a relation on con?gura-tions.Con?gurations include terminal con?gurations s,h,triples C,s,h,and a special con?guration fault indicating a memory fault.The command x:=[E] reads the value at address E in the heap and places it in x.[E]:=F updates address E so that its content is F.x:=cons(E1,...,E n)allocates a sequence of n contiguous heap cells,initializes them to E1,...,E n,and places the address of the?rst cell in the segment in x.dispose(E)removes address E from the heap. The commands x:=[E],[E]:=F and dispose(E)generate a memory fault,a particular kind of error,if E is not an active address.Notice that the number m is chosen non-deterministically in the rule for cons.An example of a command that always faults is dispose(x);[x]:=42.In typical implementations an at-tempt to dereference a disposed address might not always lead immediately to a fault.Generating these faults early in the semantics is a device that allows us to 4 x:=E,s,h (s|x→[[E]]s),h [[E]]s=n dispose(E),s,h?[n→m] s,h [[E]]s=n n∈dom(h) dispose(E),s,h fault [[E]]s=n∈dom(h)h(n)=m x:=[E],s,h (s|x→m),h [[E]]s∈dom(h) x:=[E],s,h fault [[E]]s=n∈dom(h) [E]:=F,s,h s,(h|n→[[F]]s) [[E]]s∈dom(h) [E]:=F,s,h fault m,...,n+m?1∈dom(h)v1=[[E1]]s,...,v n=[[E n]]s x:=cons(E1,...,E n),s,h (s|x→m),(h?[m→v1,...,n+m?1→v n]) C1,s,h C 1,s ,h (C1;C2),s,h (C1;C2),s,h C1,s,h s ,h (C1;C2),s,h C2,s,h C1,s,h fault (C1;C2),s,h fault [[B]]s=true if B then C else C ,s,h C,s,h [[B]]s=false if B then C else C ,s,h C ,s,h [[B]]s=false while B do C od,s,h s,h [[B]]s=true while B do C od,s,h (C;while B do C od),s,h Table2.The Programming Language:Syntax and Semantics arrange the formalism in a conservative manner,where well-speci?ed programs will never try to dereference a disposed address. In the semantics we use(f|i→j)for the(perhaps partial)function like f except that i goes to j.This notation is used both when i is and is not in the domain of f. 3Speci?cations We treat predicates semantically in this paper,so a predicate is just a subset of the set of states. Pred?=P(States) To evoke the semantics of the assertion languages from[9,2,5],we sometimes use the satisfaction notation s,h|=p as an alternative to(s,h)∈p. To de?ne the semantics of Hoare triples?rst recall point1from the Intro-duction,where we guarantee that if{p}C{q}holds then C must not access any cells not guaranteed to exist by p.We can formalize this by observing that if C did guarantee to access such a cell,then it could be made to fault by running it in a state in which that cell is not active.This is the role of the following notion of safety. 5 –“C,s,h is safe”when C,s,h ?fault. For partial correctness the interpretation of triples is the standard one,with an additional safety requirement. Partial Correctness.{p}C{q}is true just when,for all s,h, if s,h|=p then –C,s,h is safe,and –if C,s,h ?s ,h then s ,h |=q. This fault-avoiding interpretation of triples is not new,but the connection to the intuitive notion of tight speci?cation does not seem to have been observed before(excepting[2,5]).To describe this,suppose E →F is a predicate saying that F is the contents of the active address E in the current heap.Suppose, further,that the triple {x →5}C{x →6} holds and that C does not alter any variables(though it might alter heap cells). Then we claim that,just from this information,we can infer that C does not modify any heap cell existing in the starting state,other than the one denoted by x.To see the reason,suppose that C does modify such a cell and call it y.Then the speci?cation says that the program will not fault if it is run in the singleton state where x is the only active address(with contents5).But we just said that C alters the address y,and so this attempt to dereference y must generate a fault starting from the singleton state. We will also consider a total correctness form of speci?cation.For total cor-rectness,we do not need an explicit safety assumption,because total correctness is about“must termination”which itself includes a safety requirement. –“C,s,h must terminate normally”when C,s,h is safe and there is no in?nite -sequence starting from C,s,h. Total Correctness.{p}C{q}is true just when,for all s,h if s,h|=p then –C,s,h must terminate normally,and –if C,s,h ?s ,h then s ,h |=q. To formulate the Frame Rule we will need the?connective;if p and q are predicates then p?q?={(s,h?h )|s,h|=p∧s,h |=q∧h#h } The statement of the Frame Rule from[2,5]is as follows. Frame Rule,Syntactic Version {P}C{Q} Modi?es(C)∩Free(R)={} {P?R}C{Q?R} 6 where Modi?es(C)denotes the set of variables updated in the command C, i.e.,those appearing as the destination of an assignment statement in C.To be precise,the Modi?es set of each of x:=···is{x},while for[E]:=F and dispose(E)it is empty;these latter two statements a?ect the heap but not the values of variables in the store.Since we are working semantically with predicates in this paper,we need to reformulate the rule slightly and replace the reference to the free variables of R in the side condition.We will precede this with a short discussion. The condition for variables in the rule is straightforward;it simply checks whether any variables in R are modi?ed by a command C.However,the condition for heap cells is more elaborate.With the spatial conjunction,it says that for every state satisfying P?R,the current heap can be split into two subheaps so that P holds for the one and R for the other;then,the tight interpretation of the Hoare triple{P}C{Q}says that the command can only access the?rst part,i.e.the part for P,consequently making R an invariant during execution. As an example,starting from the speci?cation of CopyTree in the Introduc-tion we can infer that copying p’s tree does not a?ect a cell not in it’s data structure. treeτp CopyTree(p;q) (treeτp)?(treeτq) (treeτp)?(x →y) CopyTree(p;q) (treeτp)?(treeτq)?(x →y) Here,the Modi?es set of CopyTree(p;q)is assumed to be{q}. To describe a version of the rule which refers to semantic rather than syntactic predicates we utilize a notion X#p of independence of a predicate from a set of variables.This can be formulated simply in terms of quanti?cation.If X is a set of variables then ?X.p?={(s,h)|?s X∈[X→Ints].(s[s X],h)∈p} where s[s ]denotes the update of s by s de?ned by: s[s ](y)?= s (y)if y∈dom(s ) s(y)otherwise Then -X#p holds just if p=?X.p. Frame Rule,Semantic Version {p}C{q} Modi?es(C)#r {p?r}C{q?r} 4Soundness of the Frame Rule The Frame Rule codi?es a notion of local behaviour,and in this section we undertake to describe that notion in terms of the operational semantics. It will be helpful to?rst consider a plausible property that does not hold. 7 If C,s,h0 ?s ,h 0and h0#h1,then C,s,h0?h1 ?s ,h 0?h1. The intuition behind this property is just that we can add on extra state,and any execution that works for a smaller state can still go ahead.This property fails because of the behaviour of cons.An address that is allocated during an execution from a small state cannot be allocated starting in a bigger state where it is already active.For example, x:=cons(2,3),[x→m],[] [x→0],[0→2,1→3] but if we run x:=cons(2,3)in a heap where0is already active,then a di?erent address than0must be chosen by . This is an example of where an action on a little state can be disabled when moving to bigger states.Such behaviour might make us doubt that the Frame Rule could be sound at all.However,it only indicates that the language does not behave locally with respect to“may”properties.With Hoare triples we are interested in a form of“must”property.If{p}C{q}holds and,starting from a state satisfying p,the command terminates,then the?nal state must satisfy q. Put another way,it is not individual computations that we will judge local,but properties of classes of computations. The correct property says that if a command is safe in a given state,then the result of executing it in a larger state can be tracked to some execution computation on the little state. Lemma1(Safety and Termination Monotonicity). 1.If C,s,h is safe and h#h ,then C,s,h?h is safe. 2.If C,s,h must terminate normally and h#h ,then C,s,h?h must terminate normally. Lemma2(Frame Property).Suppose C,s,h0is safe,and C,s,h0?h1 ?s ,h . Then there is h 0where C,s,h0 ?s ,h 0,and h =h 0?h1. Proof.For x:=cons(E1,...,E n),consider m,...,n+m?1∈dom(h0?h1), The operational rule gives us s =(s|x→m)and h =h0?h1?[m→v1,...,m+n?1→v n].Then since m,...,m+n?1∈dom(h0),this segment may be selected by the operational rule for cons applied in the smaller heap h0. So h 0=h0?[m→v1,...,m+n?1→v n]gives us the desired result. For[E]:=F,since[E]:=F,s,h0is safe by assumption we know[[E]]s∈dom(h0)and therefore[[E]]s∈dom(h1).Thus,the assignment leaves h1un-changed,and taking h 0=(h0|[[E]]s→[[F]]s)gives the result. For dispose(E),if[[E]]s=n then n∈dom(h0)by safety,and h0decomposes as h 0?[n→m]for some m.This h 0satis?es the requirement of the theorem. For x:=[E],safety ensures that[[E]]s∈dom(h0),and taking h 0=h0gives the result. 8 To cover C;C ,while and if,we need to prove a slightly stronger result. We state the property,which is needed to get the right induction hypothesis, but omit the detailed proof.Consider a variant of the theorem which considers non-terminal con?gurations;speci?cally,where the terminal con?gurations s ,h and s ,h 0are replaced by C ,s ,h and C ,s ,h 0.The terminal and non-terminal variants are proven simultaneously,by induction on the derivation of C,s,h0?h1 ?s ,h or C,s,h0?h1 ?C ,s ,h .The rules for atomic commands above were already considered above,and each of the rules for while and C;C has an immediate proof. Theorem1(Soundness).The Frame Rule is sound for both partial and total correctness. Proof.The proof uses the Frame Property,and the following locality property for variables. If C,s,h ?s ,h and a variable x is not assigned in C,then s(x)=s (x). For partial correctness,suppose the premise of the Frame Rule holds,and that s,h0|=p and s,h1|=r.The premise gives us that C,s,h0is safe,and safety of C,s,h0?h1follows from Safety Monotonicity.If C,s,h0?h1 ?s ,h, the Frame Property yields h 0where h=h 0?h1and C,s,h0 ?s ,h 0.The premise then ensures s ,h 0|=q.The variable locality property implies that s agrees with s on all variables not in Modi?es(C),so s ,h1|=r follows since we know s,h1|=r and Modi?es(C)#r.The semantics of?then yields s ,h|=q?r. The argument for total correctness appeals additionally to Termination Mono-tonicity. 4.1The Scope and Delicacy of the Frame Rule Some remarks are in order on the delicacy of the soundness result. First,the non-deterministic nature of cons was relied on in an essential way. If we had interpreted cons so that,say,the smallest possible free address was always chosen for allocation,then adding memory would change what this new address was,and the di?erence could be detected with address arithmetic;this would invalidate the Frame Rule.Non-deterministic allocation is used to force a program proof not to depend on details of how the allocator might work.(In a language without address arithmetic,we could use invariance under location renaming rather than non-determinism in allocation to ensure this sort of inde-pendence.) Second,suppose we were to add an operation for trapping a memory fault to our language.If we did this,without changing?,then the Frame Rule would be invalid;the reason is that we could branch on whether or not a cell is active,and this would contradict Safety Monotonicity.This does not necessarily mean that fault trapping is incompatible with the Frame Rule.We could perhaps change the interpretation of?so that the unde?nedness it introduces is regarded as introducing the possibility of a further kind of error,di?erent from memory 9 fault.(The way Calcagno puts it,we need a notion that is detectable in the program logic,but not in the programming language.) Although delicate,the scope of the Frame Rule is wider than the speci?c programming language considered here.We brie?y sketch an abstract setting. Suppose we have an arbitrary partial commutative monoid(pcm),in place of (Heaps,?,[]),and an arbitrary set V of values,which we use to de?ne Stores= Variables→V.Then a“local action”is a binary relation between States and States∪{⊥,fault}satisfying Safety and Termination Monotonicity,and the Frame Property.With this de?nition,the Frame Rule is sound for every local action. An example somewhat removed from heap storage that?ts this de?nition is given by Petri nets.A net without capacity N=(P,T,pre,post)consists of sets P and T of places and transitions,and two functions pre,post:T→M from transitions to markings,where a marking is a?nite multiset of places and M denotes the set of all markings.M forms a pcm whose commutative monoid structure comes from the multiset union and the empty set.This is a total commutative monoid.If we regard a transition that is not enabled as equivalent to faulting,then each transition t∈T determines a local action1by the?ring rule:M[t]N i??t.?M .M=pre(t)?M and N=post(t)?M . Nets with capacity1provide a counterexample.Suppose that places in a net can hold at most one token;consequently,markings are simply subsets of places, and pre,post map transitions to?nite subsets of places.Transitions are?red in this case only when it is guaranteed that all the tokens to be produced do not violate the capacity requirement.We can de?ne a pcm on the set of places, where?is union of disjoint sets(which is unde?ned on sets that overlap).A transition t that violates Safety Monotonicity has pre(t)={a},post(t)={b}, where a=b.t is enabled in{a}but not in{a,b}because the post-place of t is already?lled in{a,b}.(It is possible to de?ne a di?erent pcm,for which transitions do correspond to local actions,by recording when a place is known to be unmarked;we can do this using P {full,empty},with?as union of partial functions with disjoint domains.) These examples and counterexamples indicate that the Frame Rule is not something we expect to be automatically valid,in the way that we expect,say, the rule of Consequence always to be.Close attention must be paid to the inter-play between the de?nition of?and the kinds of operation present in a language. 5Completeness of the Frame Rule Suppose we are given a Hoare triple speci?cation{p}C{q}but we are not told exactly what C is.The question we are concerned with in this section is whether we can derive all other speci?cations that follow from it,without making use of knowledge of C. To formulate this we consider Hoare triples{p}?{q}with an unspeci?ed command.Following[3,12,1],we call such a Hoare triple with a hole a speci?-1We take Stores to be the singleton set[Variables→{1}]. 10 Consequence p ?p{p}?{q}q?q {p }?{q }Frame Rule {p}?{q} X#r {p?r}?{q?r} Table3.Proof system for speci?cation statements with Modi?es set X cation statement.Throughout this section we assume a given set X of variables, regarded as the Modi?es set.To derive one speci?cation statement from the other we use the usual rule of Consequence from Hoare logic,and the Frame Rule;see Table3. The completeness question,which is variously called sharpness or adapta-tion completeness,is whether this system lets us derive one speci?cation state-ment from another just when this inference holds semantically.Since the rule of Consequence is itself treated semantically,in that it uses inclusion between predicates-as-sets rather than a provable implication,all of the stress in this question is placed on the Frame Rule:it is essentially asking whether we obtain enough frame axioms. To show completeness we need to de?ne a notion of semantic consequence be-tween speci?cation statements.There is a niggling problem here:Not all pre/post pairs determine a relation in a direct way.The traditional way around this prob-lem in work on speci?cation statements is to use predicate transformers,which correspond more directly to pre/post pairs.One then separately singles out spe-cial kinds of transformers and pre/post pairs that have a good correspondence with relations.In the remainder of the paper we just work with transformers. The tie-up with relations is possible,but omitted for lack of space;we refer the reader to Yang’s thesis for further information[11]. 5.1Local Predicate Transformers In a predicate transformer interpretation,a command C is interpreted as a mapping from a postcondition to a precondition.For instance,the predicate transformer induced by x:=2maps y=x to y=2. Mathematically,predicate transformers are monotone maps from predicates to predicates. PT?=Pred→monotone Pred Given a predicate transformer t the Hoare triple“{p}t{q}”corresponds to the property p?t(q).Then,the monotonicity requirement is equivalent to saying that the rule of Consequence is valid. The domain PT contains predicate transformers which,when viewed opera-tionally,don’t exhibit the local behavior of commands as described in Section4. For instance,the predicate transformerλq.{(s,h)∈q||dom(h)|≤3}corre-sponds to a command which generates a memory fault when there are more 11 than3active heap cells and skips otherwise;2this command doesn’t satisfy Safety Monotonicity.So,it is not surprising that the Frame Rule is not valid for PT since the rule is closely related to the locality properties of Section4. We re?ne PT by requiring predicate transformers to satisfy a locality con-dition.Recall that in this section we are assuming a given set X of modi?able variables. Locality for X:?r,q∈Pred.X#r=?t(q)?r?t(q?r) The condition is equivalent to saying that t satis?es the Frame Rule,which in predicate transformer terms is ?p,r,q∈Pred.X#r∧p?t(q)=?p?r?t(q?r) The domain LPT(X)of local predicate transformers with Modi?es set X is de?ned as: LPT(X)?={t∈PT|t satis?es locality for X}. LPT(X)inherits the ordering from PT,which is just a pointwise ordering induced by the subset ordering of Pred.With such an ordering,LPT(X)forms a complete lattice,in fact,a complete sublattice of PT. Proposition1.LPT(X)is a complete sublattice of PT.Therefore,given a set {t i}i∈I of elements in LPT(X),its least upper bound is given byλq. i∈I t i(q), and its greatest lower bound is given byλq. i∈I t i(q). Proof.Let r be a predicate such that X#r.It su?ces to show that i∈I t i(q?r) and i∈I t i(q?r)include( i∈I t i(q))?r and( i∈I t i(q))?r,respectively.The ?rst inclusion follows because i∈I(t i(q)?r)=( i∈I t i(q i))?r,and the second inclusion holds since?is monotone with respect to the subset ordering. 5.2Operational Sensibility The locality condition in LPT(X)has an operational explanation via mappings, wp and wlp,from commands to predicate transformers,which correspond to total correctness and partial correctness.Let C be a command and q a predicate.Then we de?ne the weakest,and weakest liberal,precondition predicate wp(C)(q)?={(s,h)|C,s,h must terminate normally and if C,s,h ?s ,h ,then s ,h |=q} wlp(C)(q)?={(s,h)|C,s,h is safe and if C,s,h ?s ,h ,then s ,h |=q} We can now establish the operational sensibility of local predicate trans-formers,which says that if X?Modi?es(C),both wp(C)and wlp(C)are local predicate transformers in LPT(X). 2This command,call it C,makes{{(s,h)∈q||dom(h)|≤3}}C{q}true for all q in both total and partial correctness,and C is the smallest such in the sense that all other such commands satisfy more Hoare triples than C. 12 Proposition2.For a command C,both wp(C)and wlp(C)satisfy locality for X i?C satis?es Safety and Termination Monotonicity,Frame Property and the following locality property for variables: if C,s,h is safe and C,s,h ?s ,h ,then s(y)=s (y)for all y∈Variables?X. Notice that this proposition establishes as close a correspondence with the local-ity properties of Section4as we would expect;since both wp and wlp completely ignore all unsafe con?gurations we can not obtain any properties of unsafe con-?gurations with predicate transformers. 5.3Proof of Completeness We have already given a proof system for speci?cation statements in Table3. This determines a notion of consequence between speci?cation statements. {p}?{q} X{p }?{q }i?{p }?{q }can be derived from{p}?{q} using the rules in Table3. The semantic interpretation of each speci?cation statement is given by a satisfaction relation between local predicate transformers in LPT(X)and speci-?cation statements.For t in LPT(X) t|=X{p}?{q}i?p?t(q). We can now de?ne the semantic consequence relation|=by requiring that any transformer satisfying the antecedent also satis?es the consequent. {p}?{q}|=X{p }?{q }i?for all t∈LPT(X), t|=X{p}?{q}implies t|=X{p }?{q }. The proof system is sound with respect to this interpretation since the mono-tonicity condition in PT ensures that the rule of Consequence is sound and the locality condition for X guarantees that the Frame Rule is sound. Proposition3(Soundness,II).If{p}?{q} X{p }?{q },then{p}?{q}|=X{p }?{q }. In the remainder of this section we concentrate on the proof of the converse. Theorem2(Completeness).If{p}?{q}|=X{p }?{q },then{p}?{q} X {p }?{q }. The proof of completeness proceeds by?nding the smallest local predicate transformer t in LPT(X),amongst those that satisfy a given speci?cation.To describe this transformer it will be convenient to use a notation for the spatial implication??of predicates in pointer logic[2,5],which is itself taken from the logic of Bunched Implications[6,7]. p??q?={(s,h)|?h .h #h∧s,h |=p=?(s,h?h )|=q} In words,p??q holds of a given heap if,whenever we are given new or fresh heap satisfying p,the combined new and current heap satis?es q. 13 Lemma3.Given predicates p,q∈Pred,the predicate transformer t=λr.p??X.(q??r)is in LPT(X)and satis?es p?t(q).Moreover,it is the smallest such in LPT(X)with respect to the pointwise ordering. Proof.It is straightforward to see that t is monotone.To see that t satis?es the locality condition for X,pick predicate r,r with X#r .Then,we have: t(r?r )=p?(?X.(q??r?r ))?p?(?X.(q??r)?r ) ?p?(?X.(q??r))?(?X.r )=p?(?X.(q??r))?r =t(r)?r The condition p?t(q)is also easily veri?ed as follows: t(q)=p?(?X.(q??q))?p?(?X.emp) ?p?emp?p where emp={(s,[])|s∈Stores}is the unit of?.Finally,t is the smallest satisfying p?t(q)because for any other t ∈LPT(X)with p?t (q), t (r)?t (q??X.(q??r))?t (q)??X.(q??r)?p??X.(q??r). We denote the smallest local predicate transformer in Lemma3by smallest(p,q,X). To prove completeness,?rst note that for predicates p,q,r,the precondi-tion smallest(p,q,X)(r)can be calculated with the Frame Rule and the rule of Consequence: {p}?{q} {p??X.(q??r)}?{q??X.(q??r)}q??X.(q??r)?r {p??X.(q??r)}?{r} The right-hand inclusion is just an application of the usual rule of?-elimination, together with a monotonicity rule for?and the version of modus ponens that connects?and??. Now,let{p }?{q }be a speci?cation statement with{p}?{q}|=X{p }?{q }. Then,we have p ?smallest(p,q,X)(q )by Lemma3,and{p }?{q }can be derived from{p}?{q}as follows: p ?p??X.(q??q ) {p}?{q} {p??X.(q??q )}?{q } {p }?{q } This?nishes the proof of Theorem2. To sum up,in this paper we have shown the soundness of a rule for au-tomatically inferring frame axioms,and we have also shown a sense in which the rule gets all the frame axioms we need.We did this by appealing to the operational semantics of a speci?c programming language:Perhaps the main 14 unresolved question is whether the approach here and in[9,2,5]can be adapted to problems further a?eld.We outlined a more abstract setting for the work,and a range of other models do?t the abstract de?nitions,but pointer models are the only ones whose program logic has been examined in detail so far.Particularly worthwhile would be to attempt to apply the notion of local action,mentioned in Section4.1,in an AI setting,where the frame problem originally arose and where it continues to be intensely studied[8]. Acknowledgments Thanks to David Naumann and Uday Reddy for advice on predicate transform-ers,to John Reynolds for discussions on the signi?cance of fault avoidance in speci?cations,and to the anonymous referees for suggesting improvements to the presentation.Yang was supported by the US NSF under grant INT-9813854and by Creative Research Initiatives of the Korean Ministry of Science and Technol-ogy.O’Hearn was supported by the EPSRC under the Local Reasoning about State project. References 1.R.-J.R.Back.On the Correctness of Re?nement Steps in Program Development. PhD thesis,Department of Computer Science,University of Helsinki,1978.Report A-1978-4. 2.S.Ishtiaq and P.O’Hearn.BI as an assertion language for mutable data structures. In Principles of Programming Languages,pages14–26,January2001. 3. C.C.Morgan.The speci?cation statement.ACM Transactions on Programming Languages and Systems,10(3),Jul1988. 4. D.Naumann.Calculating sharp adaptation https://www.wendangku.net/doc/5b2225501.html,rmation Processing Letters, 2000.To appear. 5.P.O’Hearn,J.Reynolds,and H.Yang.Local reasoning about programs that alter data structures.In L.Fribourg,editor,Proceedings of15th Annual Conference of the European Association for Computer Science Logic:CSL2001,pages1–19. Springer-Verlag.LNCS2142. 6.P.W.O’Hearn and D.J.Pym.The logic of bunched implications.Bulletin of Symbolic Logic,5(2):215–244,June99. 7. D.J.Pym.The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers,Boston/Dordrecht/London,2002.To appear. 8.R.Reiter.Knowledge in Action.MIT Press,2001. 9.J.C.Reynolds.Intuitionistic reasoning about shared mutable data structure.In Jim Davies,Bill Roscoe,and Jim Woodcock,editors,Millennial Perspectives in Computer Science,pages303–321,Houndsmill,Hampshire,2000.Palgrave. 10.J.C.Reynolds.Lectures on reasoning about shared mutable data structure.IFIP Working Group2.3School/Seminar on State-of-the-Art Program Design Using Logic.Tandil,Argentina,September2000. 11.H.Yang.Local Reasoning for Stateful Programs.Ph.D.thesis,University of Illinois, Urbana-Champaign,Illinois,USA,2001. 12.H.Yang and U.S.Reddy.On the semantics of re?nement calculi.In Foundations of Software Science and Computation Structures,pages359–374.Springer-Verlag, 2000. 15