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

DOI10.1007/S00165-013-0278-3MaRDI QIDQ736803zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(7)

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

Describes a project that uses

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)