A sharp proof rule for procedures in WP semantics

DOI10.1007/BF00289144MaRDI QIDQ1104730zbMATH OpenFDO

Authors A. Bijlsma, P. A. Matthews, J. G. Wiltink

Publication date 1989

Published in Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

specificationweakest preconditionsharpnessprocedure callproof rulepostconditionWP semantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Calculating with procedure calls
• A general proof rule for procedures in predicate transformer semantics
• Calculating sharp adaptation rules.
• Proof rules for recursive procedures
• scientific article; zbMATH DE number 3888897

Cites work

• scientific article; zbMATH DE number 3874650 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• A general proof rule for procedures in predicate transformer semantics
• Assignment and Procedure Call Proof Rules
• On the notion of expressiveness and the rule of adaptation

Cited in

(5)

• Equivalence of the Gries and Martin proof rules for procedure calls
• Calculating sharp adaptation rules.
• An adaptation-complete proof system for local reasoning about cloud storage systems
• A proof outline logic for object-oriented programming
• Calculating with procedure calls

This page was built for publication: A sharp proof rule for procedures in WP semantics

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