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)

Full work available at URL https://doi.org/10.1007/BF00289144

zbMATH Keywords

postconditionprocedure callproof rulesharpnessspecificationweakest preconditionWP 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

• A general proof rule for procedures in predicate transformer semantics
• Assignment and Procedure Call Proof Rules
• 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?)
• On the notion of expressiveness and the rule of adaptation

Cited in

(6)

• 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
• scientific article; zbMATH DE number 1303993 (Why is no real title available?)
• 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)