Semantic Collaboration
Semantic Collaboration (SC) is a methodology to specify and reason about invariants of arbitrary object structures. It combines ownership for hierarchical structures and collaboration for non-hierarchical inter-object dependencies. To make sure collaborative invariants are maintained, SC equips every object x with a ghost set observers to keep track of all objects o, whose invariant might depend on x. In turn, o's invariant is only allowed to depend on x if it also states that x.observers contains o, which prevents x from forgetting about o.
Extended Version
Extended version of the report: [arXiv]
Main differences with the submitted version: more detailed soundness proof and comparison with related work.
Soundness Proof
Proof of soundness of Semantic Collaboration mechanized in Dafny: [browse online]
Challenge problems
We have assembled a set of six challenge problems, which capture the essence of various collaboration patterns often found in object-oriented software: the observer pattern, the iterator pattern, master clock, doubly-linked list, the composite pattern, and the priority inheritance protocol.
Full descriptions and our solutions: [browse online]
Try in AutoProof
AutoProof is part of the Eiffel Verification Environment (Eve): a research branch of the EiffelStudio IDE. The tool is also available through a simple web interface below. The web interface does not support all the features available in Eve, such as selecting the modules to be verified or navigating to errors.