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
In the Require and Ensure blocks, the only things that are allowed are:
- The
Checkstatement - Comments
The Require block statement MUST be the first statement in the method (only comment or white-space is allowed before it)
The 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 Require and Ensure blocks, the Invariant methods can only contain:
- The
Checkstatement - Comments
The syntax of the Check method is the same as it is in the Require and Ensure blocks.
The Check statement syntax
Check(condition As Boolean, Optional FailureMessage as String)
As the Check method can only be used within the Require and 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>"
