Lazy behavioral subtyping

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

zbMATH Keywords

inheritanceproof systemsobject orientationincremental reasoningcode reuselate bindingmethod redefinitionbehavioral subtyping

Mathematics Subject Classification ID

Theory of software (68N99)

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

• JML
• Spec#
• Creol
• Featherweight Java
• Simula 67

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