A General Proof Rule for Procedures in Predicate Transformer Semantics
- Creators
- Martin, Alain J
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.
Files
Name | Size | Download all |
---|---|---|
md5:123c2df817afd9c36e069d194f7be877
|
786.4 kB | Preview Download |
md5:645c95ccc721b9c74d828602e66e30c9
|
893.5 kB | Download |
Additional details
- Eprint ID
- 26989
- Resolver ID
- CaltechCSTR:1983.5075-tr-83
- Created
-
2002-08-07Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports