Calculating with procedure calls

DOI10.1016/0020-0190(93)90098-TMaRDI QIDQ685524zbMATH OpenOpenAlexFDO

Authors A. Bijlsma

Publication date 17 October 1993

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(93)90098-t

zbMATH Keywords

formal semanticsproceduresprogram correctnessprogram specificationproof rules

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

• A sharp proof rule for procedures in WP semantics
• A general proof rule for procedures in predicate transformer semantics
• Proof rules for recursive procedures
• Safety and progress of recursive procedures
• Predicate transformers for recursive procedures with local variables

Cites work

• A general proof rule for procedures in predicate transformer semantics
• A sharp proof rule for procedures in WP semantics
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)

Cited in

(11)

• Equivalence of the Gries and Martin proof rules for procedure calls
• A sharp proof rule for procedures in WP semantics
• Calculating sharp adaptation rules.
• Calculating with pointers
• Safety and progress of recursive procedures
• scientific article; zbMATH DE number 1670754 (Why is no real title available?)
• scientific article; zbMATH DE number 3938534 (Why is no real title available?)
• scientific article; zbMATH DE number 1303993 (Why is no real title available?)
• Staged allocation: a compositional technique for specifying and implementing procedure calling conventions
• Predicate transformers and higher-order programs
• Proof obligations for blocks and procedures

This page was built for publication: Calculating with procedure calls

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685524)