Browse Prior Art Database

A GENERAL PROOF RULE FOR PROCEDURES IN PREDICATE TRANSFORMER SEMANTICS

IP.com Disclosure Number: IPCOM000147931D
Original Publication Date: 1983-Dec-31
Included in the Prior Art Database: 2007-Mar-28

Publishing Venue

Software Patent Institute

Related People

Martin, Alain J.: AUTHOR [+2]

Abstract

A GENERAL PROOF RULE FOR PROCEDURES IN' PREDICATE TRANSFORMER SEMANTICS Alain J, Martin Computer Science California Institute of Technology The 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 InPredicate Transformer Semantics Alain J. Martin Computer ScienceCalifornia 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 ,

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 15% of the total text.

Page 1 of 22

A GENERAL PROOF RULE FOR PROCEDURES IN'

PREDICATE TRANSFORMER SEMANTICS

Alain J, Martin

Computer Science

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

The

[This page contains 1 picture or other non-text object]

Page 2 of 22

[This page contains 1 picture or other non-text object]

Page 3 of 22

A General Proof Rule For Procedures

          In
Predicate Transformer Semantics

Alain J. Martin

       Computer Science
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

Introduction

    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

[This page contains 1 picture or other non-text object]

Page 4 of 22

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...