Calculating with procedure calls (Q685524)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Calculating with procedure calls |
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Calculating with procedure calls |
scientific article |
Statements
Calculating with procedure calls (English)
0 references
17 October 1993
0 references
Various proof rules for procedure calls in weakest precondition semantics have been proposed. The author gives a proof rule that is very easy to use, but does not yield the best possible answer for every specification -- only for a large class of specifications called normal specifications. In the Appendix, he shows how every specification can be transformed into an equivalent normal one.
0 references
formal semantics
0 references
program specification
0 references
program correctness
0 references
procedures
0 references
proof rules
0 references
