I’d like to request the Class contracts (already available in Oxygene, C#, Swift and Java) to be implemented in Mercury.
Link for the current implementation in the other languages for the ones that do not know what class contracts are: Class Contracts
For the Mercury-VB syntax of the method pre and post conditions
Sub DoWork(aValue: As Integer) Require 'Block with checks to see if the state and parameters are within the expected range ' Check(fMyWorker <> Null, "There is no worker available") Check(fMyValue > 0) Check(aValue > 0) End Require //... do the work here Ensure 'Block with checks to see if the state that was changed and the result are within the expected range ' Check(fMyResult <> Null) Check(fMyResult.Value >= 5) End Ensure End Sub
Ensure blocks, the only things that are allowed are:
Require block statement MUST be the first statement in the method (only comment or white-space is allowed before it)
Ensure block MUST be the last block in the method, making
End Ensure the last statement in the method (only comment or white-space is allowed before it)
For the Mercury-VB syntax of the class invariant conditions
Public Class MyClass ... some methods or properties Public Invariants 'Will be executed at the end of every public method, after the Ensure block ' Check(fField1 > 35, "fField1 should always be greater than 35!" Check(SomeProperty = 0) Check(SomeBoolMethod() and not (fField2 = 5)) End Invariants private Invariants 'Will be executed at the end of every method (public or private), after the Ensure block ' Check(fField > 0) End Invariants End Class
The Invariant method can be specified twice, one time Public and one time Private. Friend and Protected Invariant methods do not exist. Public, Friend and Protected methods that execute will invoke both the Public as the Private Invariant Methods, Private methods that execute will only invoke the Private Invariant Method.
As in the Method
Ensure blocks, the
Invariant methods can only contain:
The syntax of the Check method is the same as it is in the
The Check statement syntax
Check(condition As Boolean, Optional FailureMessage as String)
Check method can only be used within the
Ensure blocks, and in the
Invariant methods, where other methods can not be used (unless as parameter of this
Check method), this
Check method can not interfere with or create an unintended overload for an existing
Check method in the user code.
When the failure message is not given in the call, it will return the same as in the other languages; something like
"Method DoWork assertion failed <condition>"