Chuck wrote:I forget the D syntax, but Eiffel has "else require" and "then ensure". Cobra has the same thing but calls them "or require" and "and ensure" since the operations, as with Eiffel, are OR and AND.
Looks like I have forgotten Eiffel, so I have reviewed DbC :
* D has only "require" and "ensure" ; the "or" and "and" are implicit.
* Standard Eiffel does exactly like Cobra (mandatory explicit "or" and "and").
* SmartEiffel, the open source implementation, deviates from the standard, and uses "require" for the first real precondition and "or require" for the next ones.
* Spec# does like D, but forbids precondition modifications in overrides, so using Spec# as a backend to leverage its verification tools will be a problem. There are other restrictions, and exceptions thrown have to be in the contract, like in Java.
Grepping the SmartEiffel code base for statistics :
* "or require" is less than 1% of all "require" ; they are so seldom used that the drastic Spec# rule of precondition invariance is reasonable after all.
* "and ensure" is about 4% of all "ensure" ; hence the SmartEiffel rule : in Cobra 96% of "and ensure" will be fake ones and the maintainer will miss the real ones.
As a conclusion, there is no standard for DbC. My choice would be SmartEiffel rule for "ensure" because it gives more information to the maintainer, and Spec# rule for "require" because restrictions can be removed later without breaking existing code but not added (and Spec# may become the standard for DbC on the CLI in a few years).
