On 7/1/2011 6:53 AM, Daniel Murphy wrote:
To enforce this, the compiler should give an error if a base function's precondition passes but a derived precondition does not.
No, it should not. Only one of the contracts needs to pass.
The requirement is not really that any 'in' contract passing is good enough,
Yes, it is.
it's just assumed that all preconditions on inherited functions will pass if the base contract does.
Only one contract needs to pass.
