A sharp proof rule for procedures in WP semantics

DOI10.1007/BF00289144zbMATH Open0647.68017MaRDI QIDQ1104730FDOQ1104730

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

Publication date: 1989

Published in: Acta Informatica (Search for Journal in Brave)

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A general proof rule for procedures in predicate transformer semantics
• On the notion of expressiveness and the rule of adaptation
• Assignment and Procedure Call Proof Rules
• Title not available (Why is that?)

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)