Closed anthonyanjorin closed 7 years ago
Suggested consistent precondition (postcondition of #6 ):
FamilyRegister {
}
PersonRegister {
}
To finalise the precondition, set birthdays of all persons in the person register as an idle target update.
Source delta: Delete the empty family Skinner in the family register and propagate. Expected postcondition: person register (now with birthdays set!) should remain unchanged.
Features: [round trip | del+attr | fixed | structural]
Not sure if the test is corr-based or not :( I think not; even if a tool completely messes up the correspondence link, it should still be possible to pass the test as this doesn't seem relevant.
I guess setting of birthdays could be moved to establishing the precondition as this is already tested in #10
A synchroniser is hippocratic if it does not do anything for a pair of models that is already consistent (even if the delta to be propagated is not idle).
Note that this is more than stability, but less than least change.