Lazy behavioral subtyping

DOI10.1016/J.JLAP.2010.07.008MaRDI QIDQ710675zbMATH OpenOpenAlexFDO

Authors Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen

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

inheritanceobject orientationproof systemscode reuseincremental reasoninglate bindingmethod redefinitionbehavioral subtyping

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Lazy abstraction
• Incremental reasoning with lazy behavioral subtyping for multiple inheritance
• Publication:4730749
• Behavioural subtyping using invariants and constraints
• Lazy Abstraction with Interpolants
• Implementation of Functional Languages
• scientific article; zbMATH DE number 1696907
• Lazy Theories of Operations and Types

Cites work

• scientific article; zbMATH DE number 1693527 (Why is no real title available?)
• scientific article; zbMATH DE number 2089401 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 54048 (Why is no real title available?)
• scientific article; zbMATH DE number 1231452 (Why is no real title available?)
• scientific article; zbMATH DE number 1759367 (Why is no real title available?)
• scientific article; zbMATH DE number 4115919 (Why is no real title available?)
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A Complete Guide to the Future
• A logic of object-oriented programs
• A proof outline logic for object-oriented programming
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Axiomatic semantics of communicating sequential processes
• Behavioral subtyping relations for active objects
• Creol: A type-safe object-oriented model for distributed concurrent systems
• Enhancing modular OO verification with separation logic
• Hoare logic for Java in Isabelle/HOL
• Incremental Reasoning for Multiple Inheritance
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• Separation Logic for Multiple Inheritance
• Separation logic, abstraction and inheritance
• Specification and Development of Interactive Systems
• Specification and verification challenges for sequential object-oriented programs
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(7)

• A sound and complete reasoning system for asynchronous communication with shared futures
• Observable behavior of distributed systems: component reasoning for concurrent objects
• Incremental Reasoning for Multiple Inheritance
• Incremental reasoning with lazy behavioral subtyping for multiple inheritance
• Automatic verification of Java programs with dynamic frames
• Verifying traits: an incremental proof system for fine-grained reuse
• A proof system for adaptable class hierarchies

Describes a project that uses

Uses Software

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

This page was built for publication: Lazy behavioral subtyping

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