On 1/18/17 5:29 PM, Mark wrote:
I see. Is there a way to call invariant() of a class/struct directly? That would obviate the need for a particular predicate (copy the class state, run the setter, check if invariants are satisfied and restore previous state if they aren't).
It seems painfully obvious the right way is a guarded assignment and anything else would be a more or less painful workaround. -- Andrei
