A GENERAL PROOF RULE FOR PROCEDURES IN PREDICATE TRANSFORMER SEMANTICS
Original Publication Date: 1983-Dec-31
Included in the Prior Art Database: 2007-Mar-28
Software Patent Institute
Martin, Alain J.: AUTHOR [+2]
A GENERAL PROOF RULE FOR PROCEDURES IN' PREDICATE TRANSFORMER SEMANTICS
A GENERAL PROOF RULE FOR PROCEDURES IN'
PREDICATE TRANSFORMER SEMANTICS
Alain J, Martin
California Institute of Technology
research described in this paper was sponsored by the
Defense Advanced Research Projects Agency, ARPA Order number 3771,
and monitored by the Office of Naval Research under contract number N00014- 79-C-0597
O 1983, California Institute of Technology
A General Proof Rule For Procedures
Predicate Transformer Semantics
Alain J. Martin
California Institute Of Technology
Abstract Given a general definition of the procedure call based on the substitution rule for assignment, a general proof rule is derived for procedures with unrestricted value, result, and value-result parameters, and global variables in the body of the procedure. It is then extended for recursive procedures. Assuming that it has been proved that the body establishes a certain postcondition I, the "intentionn, for a certain precondition J, the proof rule permitting to determine under which conditions a certain procedure call establishes the postcondition E, the nextension", is based on finding an "adaptationw A, as weak as possible, such that A ,
I ==> Ev. (E1 is derived from E by some substitution of parameter variables.) It is preferable, but not essential, that the body be *transparentn for the value parameters, i.e., that the value parameters are not changed by the body.
Pasadena, 9 February 1983
In progratming, the procedure mechanism fulfills two roles. First, it allows recursion; second, it provides a general abstraction mechanism. It is the procedure as an abstraction mechanism that is studied here, although the results w i l l be used to prove properties of recursive programs as well.
Apart from making recursion possible, the procedcre mechanism, as we define it, does not introduce a new semantic concept - a new "predicate
transformerw. It permits to define arbitrary primitives whose semantics, unlike those of usual primitives, are only a partial function. More precisely, the "procedure declarationn mechanism permits to construct a program part - the "proceduren - of an arbitrary complexity. This procedure is designed for a certain intended net-effect: it is specified how the procedure establishes a certain postconditiow, but not how it
establishes any postcondition. The wprocedure calln mechanism permits to use the procedure as a primitive, i.e., by knowing only what it does, and ignoring how it does it. Hence, the main issue with procedures is how to deal with partial semantic specification.
Although we shall couch the procedure paradigm in the notation of an impera...