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 the normal view instead:
scientific article; zbMATH DE number 417421
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Calculating with procedure calls |
scientific article; zbMATH DE number 417421 |
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
0.8425675630569458
0 references
0.8100852966308594
0 references
0.7807142734527588
0 references
0.7760628461837769
0 references
0.7736530303955078
0 references
