A proof outline logic for object-oriented programming
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1701766 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- A Proof System for Communicating Sequential Processes
- A logic of object-oriented programs
- A sharp proof rule for procedures in WP semantics
- A syntax-directed Hoare logic for object-oriented programming concepts.
- Algebraic Methodology and Software Technology
- An axiomatic basis for computer programming
- An axiomatic proof technique for parallel programs
- Calculating sharp adaptation rules.
- Hoare logic for Java in Isabelle/HOL
- How the design of JML accommodates both runtime assertion checking and formal verification
- Inductive proof outlines for monitors in Java.
- Mathematics of Program Construction
- Modular specification and verification of object-oriented programs
- On the notion of expressiveness and the rule of adaptation
- Separation and information hiding
- Ten Years of Hoare's Logic: A Survey—Part I
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Weakest pre-condition reasoning for Java programs with JML annotations
Cited in
(18)- Weak arithmetic completeness of object-oriented first-order assertion networks
- WP semantics and behavioral subtyping
- Abstraction and subsumption in modular verification of C programs
- Frame rule for mutually recursive procedures manipulating pointers
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- A logic of object-oriented programs
- scientific article; zbMATH DE number 1670750 (Why is no real title available?)
- Verification of object-oriented programs: a transformational approach
- Algebraic Methodology and Software Technology
- Lazy behavioral subtyping
- scientific article; zbMATH DE number 549985 (Why is no real title available?)
- Graph-based object-oriented Hoare logic
- Incremental reasoning with lazy behavioral subtyping for multiple inheritance
- A syntax-directed Hoare logic for object-oriented programming concepts.
- Abstraction and subsumption in modular verification of C programs
- Denotational semantics for a program logic of objects
- Incremental Reasoning for Multiple Inheritance
- On assertion-based encapsulation for object invariants and simulations
This page was built for publication: A proof outline logic for object-oriented programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2571207)
