A general proof rule for procedures in predicate transformer semantics
From MaRDI portal
Publication:797986
DOI10.1007/BF00264276zbMATH Open0546.68012OpenAlexW2015744089MaRDI QIDQ797986FDOQ797986
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
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
- Title not available (Why is that?)
- Procedures, parameters, and abstraction: Separate concerns
- Calculating sharp adaptation rules.
- A sharp proof rule for procedures in WP semantics
- Proof obligations for blocks and procedures
- Proof rules for recursive procedures
- Title not available (Why is that?)
- 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)
