A general proof rule for procedures in predicate transformer semantics

DOI10.1007/BF00264276MaRDI QIDQ797986zbMATH OpenOpenAlexFDO

Authors Alain J. Martin

Publication date 1983

Published in Acta Informatica (Search for Journal in Brave)

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

zbMATH Keywords

parameterssemanticsrecursive procedurescorrectnessprocedure callproof rule

Mathematics Subject Classification ID

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

Recommendations

• A semantic basis for proof queries and transformations
• Predicate-transformer semantics of general recursion
• scientific article; zbMATH DE number 408800
• Towards a calculus of predicate transformers
• Transformational methodology for proving termination of logic programs
• Predicate transformers and higher-order programs
• Deriving proof rules from continuation semantics
• An Intuitionistic Predicate Logic Theorem Prover
• Predicate Transformer Semantics
• Inductive proofs by specification transformations

Cited in

(13)

• Equivalence of the Gries and Martin proof rules for procedure calls
• Procedures, parameters, and abstraction: Separate concerns
• Calculating sharp adaptation rules.
• scientific article; zbMATH DE number 6819811 (Why is no real title available?)
• A sharp proof rule for procedures in WP semantics
• Proof obligations for blocks and procedures
• Proof rules for recursive procedures
• scientific article; zbMATH DE number 3888897 (Why is no real title available?)
• A predicate transformer for the progress property `to-always'
• Inference rules for proving the equivalence of recursive procedures
• Predicate transformers and higher-order programs
• Formalizing Dijkstra's predicate transformer wp in weak second-order logic
• Calculating with procedure calls

This page was built for publication: A general proof rule for procedures in predicate transformer semantics

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