Verifying traits: an incremental proof system for fine-grained reuse

DOI10.1007/S00165-013-0278-3zbMATH Open1342.68059OpenAlexW1967305746MaRDI QIDQ736803FDOQ736803

Authors: Ferruccio Damiani, Johan Dovland, Einar Broch Johnsen, Ina Schaefer 

Publication date: 5 August 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2318/150050

Recommendations

• Traits: correctness-by-construction for free
• Lazy behavioral subtyping
• A proof system for adaptable class hierarchies
• On flexible dynamic trait replacement for Java-like languages
• Modular specification and verification of object-oriented programs

zbMATH Keywords

traitsprogram verificationobject orientationproof systemsincremental reasoning

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• KeY: A Formal Method for Object-Oriented Systems
• An axiomatic basis for computer programming
• Ten Years of Hoare's Logic: A Survey—Part I
• An axiomatic proof technique for parallel programs
• Creol: A type-safe object-oriented model for distributed concurrent systems
• Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages
• Verification of sequential and concurrent programs
• Lazy behavioral subtyping
• Incremental reasoning with lazy behavioral subtyping for multiple inheritance
• Verifying traits: an incremental proof system for fine-grained reuse
• Behavioral interface specification languages
• Separation logic, abstraction and inheritance
• Separation Logic for Multiple Inheritance
• Combining traits with boxes and ownership types in a Java-like setting
• On flexible dynamic trait replacement for Java-like languages
• Extending FeatherTrait Java with interfaces

Cited In (7)

• Flexible Correct-by-Construction Programming
• Extending FeatherTrait Java with interfaces
• Traits: correctness-by-construction for free
• A proof system for adaptable class hierarchies
• Verifying traits: an incremental proof system for fine-grained reuse
• Combining traits with boxes and ownership types in a Java-like setting
• On flexible dynamic trait replacement for Java-like languages

Uses Software

• JML
• Creol
• Featherweight Java
• FeatherTrait

This page was built for publication: Verifying traits: an incremental proof system for fine-grained reuse

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