CaltechAUTHORS
  A Caltech Library Service

A General Proof Rule for Procedures in Predicate Transformer Semantics

Martin, Alain J (1983) A General Proof Rule for Procedures in Predicate Transformer Semantics. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1983.5075-tr-83

[img]
Preview
Other (Adobe PDF (286KB))
See Usage Policy.

768Kb
[img]
Preview
Postscript
See Usage Policy.

872Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1983.5075-tr-83

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 post condition E, the "extension", is based on finding an "adaptation" A , a s 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.


Item Type:Report or Paper (Technical Report)
Group:Computer Science Technical Reports
Record Number:CaltechCSTR:1983.5075-tr-83
Persistent URL:http://resolver.caltech.edu/CaltechCSTR:1983.5075-tr-83
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:26989
Collection:CaltechCSTR
Deposited By: Imported from CaltechCSTR
Deposited On:07 Aug 2002
Last Modified:26 Dec 2012 14:11

Repository Staff Only: item control page