< Map ADT AutoProof Code Repository Master clock >

Marriage

Category: Invariant

Source: ECOOP'04

Description

The marriage problem is about a class PERSON with a marry operation, and a class invariant that specifies the consistency constraint that marriage is symmetric. The difficulty lies in specifying the invariant and performing the marry and divorce operations.

download source

Code