Feature request: Class contracts for Mercury

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 Check statement
  • 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 Check statement
  • 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>"

I’m in favor of the Require/End Require, Ensure/End Ensure and Invarians/End Invariants syntax; straight-forward and fits in well, I think.

I’m unsure/undecided about introducing/using an explicit Check “magic” function for the individual checks. What benefit do you see ion using that rather than just having the checks as a plain expression/statement, as is done in the other languages, e.g.:

    fMyWorker <> Null : "There is no worker available"
    fMyValue > 0
    aValue > 0
  End Require

Not covered in the above, I assume we;'d introduce Old. to access the original version of a variable, e.g.

Sub IncreemntIt()
  f = f+1;
    f-1 = Old.f
  End Ensure
End Sub

Just that the syntax is not VB at all - The first word on a code line must always be a keyword.
The only exception to that is a method call, where you are allowed to omit the Call keyword.

That’s not true.

X = 5

that’s a assignment statement that doesn’t start with a keyword?

You are right. Let can also be omitted.

But the point is, you can always write it starting with a keyword.

Curious, Let x = 5 dopes not compile for me. should it?
if we go in that vain, we should use

    Check fMyWorker <> Null : "There is no worker available"
    Check fMyValue > 0
    aValue > 0 // optionally Check can be omitted
  End Require

for consistency?

Tested it in VB and no, no longer supported as error.
So indeed one construct without keyword :flushed:

The : <string> still doesn’t feel like VB …
The : is normally a statement separator.

Check fMyWorker <> Null, "There is no worker available"


Now we are at the normal VB method syntax, the optional one without the braces.

1 Like


should we go with thjs, then? Should we also add “Let” support (it’s a keyword anyways, i think from LINQ).

Let keyword support gives you some extra VB^backwards compatibility.
If you do LET, then also do SET - LET for assignment of value types, SET for assignment of reference types.

For the syntax, only the braces are missing - so, if you can support them too :slight_smile:
Otherwise, this is acceptable.

1 Like

Can you elaborate on this one?

Just for Check, off also for Let, Dim & Co? Else this seems inconsistent.

For now I’ll log it without parens

Logged as bugs://E25717. for class contracts

Logged as bugs://E25718. For Let, pending more info

bugs://E25717 was closed as fixed.

bugs://E25718 was closed as fixed.