Lazy behavioral subtyping
From MaRDI portal
Publication:710675
DOI10.1016/j.jlap.2010.07.008zbMath1204.68072OpenAlexW2006935274MaRDI QIDQ710675
Olaf Owe, Martin Steffen, Einar Broch Johnsen, Johan Dovland
Publication date: 22 October 2010
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/10852/9861
inheritanceproof systemsobject orientationincremental reasoningcode reuselate bindingmethod redefinitionbehavioral subtyping
Related Items (6)
Observable behavior of distributed systems: component reasoning for concurrent objects ⋮ A sound and complete reasoning system for asynchronous communication with shared futures ⋮ A proof system for adaptable class hierarchies ⋮ Automatic verification of Java programs with dynamic frames ⋮ Incremental reasoning with lazy behavioral subtyping for multiple inheritance ⋮ Verifying traits: an incremental proof system for fine-grained reuse
Uses Software
Cites Work
- Creol: A type-safe object-oriented model for distributed concurrent systems
- An axiomatic proof technique for parallel programs
- Behavioral subtyping relations for active objects
- A proof outline logic for object-oriented programming
- Specification and verification challenges for sequential object-oriented programs
- Specification and Development of Interactive Systems
- Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
- Separation logic, abstraction and inheritance
- Enhancing modular OO verification with separation logic
- Axiomatic semantics of communicating sequential processes
- Incremental Reasoning for Multiple Inheritance
- Ten Years of Hoare's Logic: A Survey—Part I
- Hoare logic for Java in Isabelle/HOL
- Verification: Theory and Practice
- Separation Logic for Multiple Inheritance
- An axiomatic basis for computer programming
- A Complete Guide to the Future
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Lazy behavioral subtyping
