Browse Prior Art Database

A GENERAL PROOF RULE FOR PROCEDURES IN PREDICATE TRANSFORMER SEMANTICS

IP.com Disclosure Number: IPCOM000127932D
Original Publication Date: 1983-Dec-31
Included in the Prior Art Database: 2005-Sep-14
Document File: 14 page(s) / 35K

Publishing Venue

Software Patent Institute

Related People

Alain J. Martin: AUTHOR [+3]

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 "intention", for a certain precondition J, the proof rule permitting to determine under which conditions a certain procedure call establishes the posteondition E, the "extension", is based on finding an "adaptation" A, as weak as possible, such that A " I ==> E'. (E' is derived from E by some substitution of parameter variables.) It is preferable, but not essential, that the body be "transparent" for the value parameters, i.e., that the value parameters are not changed by the body. . Pasadena, 9 February 1983

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 15% of the total text.

Page 1 of 14

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A GENERAL PROOF RULE FOR PROCEDURES IN PREDICATE TRANSFORMER SEMANTICS

Alain J. Martin Computer Science California Institute of Technology

i

5075--TR: 83 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

California Institute of Technology A General Proof Rule For Procedures In . Predicate Transformer Semantics

Alain J. Martin Computer Science California Institute f 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 "intention", for a certain precondition J, the proof rule permitting to determine under which conditions a certain procedure call establishes the posteondition E, the "extension", is based on finding an "adaptation" A, as weak as possible, such that A " I ==> E'. (E' is derived from E by some substitution of parameter variables.) It is preferable, but not essential, that the body be "transparent" for the value parameters, i.e., that the value parameters are not changed by the body. .

Pasadena, 9 February 1983

Introduction

In programming, 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 will be used to prove properties of recursive programs as well.

Apart from making recursion possible, the procedure mechanism, as we define it, does not introduce a new semantic concept - a new "predicate transformer". It permits to define arbitrary primitives whose semantics, unlike those of usual primitives, are only a partial function. More precisely, the "procedure declaration" mechanism permits to construct a program part - the "procedure" - of an arbitrary complexity. This procedure is designed for a certain intended net- effect: it is specified how the procedure establishes a certain postcondition, but not how it establishes and postcondition. The "procedure call" 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.

California Institute of Technology Page 1 Dec 31, 1983

Page 2 of 14

A GENERAL PROOF RULE FOR PROCEDURES IN PREDICATE TRANSFORMER SEMANTICS

Although we shall couch the procedure paradigm in the notation of an imperative programming language, the concepts of abstraction and of partial specification that this paradigm embodies ar...