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.


More examples