Method contracts

[Aurel300]

As discussed on Slack, it would be nice to be able to annotate methods with pre- and post-conditions.

@:pre(x >= 3 && x < array.length + 3)
@:post(return != null)
static function getOffset(x:Int):String {
  return array[x - 3];
}

Potential applications:

• parse the contracts with the static analyser to avoid unnecessary checks (#8815)
• pass the contracts onto an external verifier (Viper, Boogie, Z3…) and emit compilation errors when the code does not fulfil the contract
• parse with dox to slightly enhance documentation

There are also some problems to work out with the syntax, e.g., how to represent:

• the return value? - In the example I used the return keyword, which might work.
• the previous value of a variable? - Conventionally annotated with old. There might also be issues due to variable shadowing or scoping.
• type assertions? - If a dynamic is passed in?
• enum case assertions?

[back2dos]

Is there some good design we could steal?

It would also be nice if one could formulate such contracts for the underlying value of an abstract (e.g. not NaN).

[Aurel300]

The verifiers I've seen so far simply use the syntax of the current language, and annotate the function somehow:

• Nagini - annotates with special calls at the beginning of the method
• Prusti - annotates with attributes
• SpecSharp - adds extra syntax

For underlying values of abstracts I think we need to decide what to do with https://github.com/HaxeFoundation/haxe-evolution/pull/62.

[Simn]

Although it seems that Aurel has basically moved on from Haxe, I'm still quite interested in this subject and would like to explore it at some point. I'll keep the issue open as a reminder.

[Aurel300]

Although I don't use Haxe all that much anymore, I would be interested in contributing to this as well.

[Simn]

I'm happy to hear that! I'm not really sure how to move this forward, but I'd really like to support something here.

A question about the scope of this, because I know almost nothing about method contracts: If we have something like the documentation on String.indexOf:

Returns the position of the leftmost occurrence of str within this String.

If startIndex is given, the search is performed within the substring of this String starting from startIndex.

If startIndex exceeds this.[length](https://api.haxe.org/String.html#length), -1 is returned.

If startIndex is negative, the result is unspecifed.

Otherwise the search is performed within this String. In either case, the returned position is relative to the beginning of this String.

If str cannot be found, -1 is returned.

Will it be possible to express parts of the behavior related to startIndex in the method contract? I'd really like to be able to have this in a single place and then generate both documentation and tests from it, but it's unclear to me if that would even be in-scope here.

[Simn]

We had a very enlightening discussion on slack and I now have a much better understanding of what's going on here. This is Aurel's "mapping" of the indexOf documentation to what could be a contract:

• "If startIndex is negative, the result is unspecified." - @:requires(startIndex != null ==> startIndex > 0) (where ==> is a logical implication)
• "If startIndex exceeds this.length, -1 is returned." - @:ensures(startIndex != null && startIndex >= this.length ==> result == -1)
• In the other cases (i.e. startIndex == null || (0 <= startIndex && startIndex < this.length) ==> ...):
  • We want to say that, if a substring was found, then it can indeed be found at the returned position: result != -1 ==> this.substr(result, str.length) == str.
  • Furthermore, if there was a startIndex, then the result must not be smaller: startIndex != null ==> startIndex <= result.
  • Finally, the substring must not have been found earlier in the string: forall(index: Int :: (startIndex ?: 0) <= index && index < result ==> this.substr(index, str.length) != str). (Is that the null-coalescing operator?)

I also got some reading material as homework!