Calculating sharp adaptation rules.

DOI10.1016/S0020-0190(00)00215-5zbMATH Open1052.68085WikidataQ127473627 ScholiaQ127473627MaRDI QIDQ1607103FDOQ1607103

Authors: David A. Naumann 

Publication date: 25 July 2002

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

Recommendations

• A sharp proof rule for procedures in WP semantics
• Calculating with procedure calls
• Proof rules for recursive procedures
• Safety and progress of recursive procedures
• A general proof rule for procedures in predicate transformer semantics

zbMATH Keywords

adaptation rules

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Refinement Calculus
• An axiomatic basis for computer programming
• Ten Years of Hoare's Logic: A Survey—Part I
• Title not available (Why is that?)
• Proving total correctness of recursive procedures
• Hoare logic and auxiliary variables
• A categorical model for higher order imperative programming
• An algebraic construction of predicate transformers
• Algebraic proofs of consistency and completeness
• Calculating with procedure calls
• A sharp proof rule for procedures in WP semantics
• Assignment and Procedure Call Proof Rules

Cited In (4)

• A sharp proof rule for procedures in WP semantics
• Algebraic Methodology and Software Technology
• An adaptation-complete proof system for local reasoning about cloud storage systems
• A proof outline logic for object-oriented programming

This page was built for publication: Calculating sharp adaptation rules.

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