Contract: Add `invariant` contract

[Delja]

This pr adds invariant feature.

Annotations

To define a new class contract you need to use the invariant annotation. The principle is the same as the other contract expect and ensure all expressions returning a boolean (comparison, method call ...) can be used as a condition.

Invariant generation process

When a contract is detected, the code is extended to add verification functionality. A new method is then introduced to verify the invariant clause.

When a class has an invariant contract, all methods (redef, inherited, intro) have now two contracts facet to check it. One for the invariant verification and one for a potential ensures, expect or both verification. This split was made to avoid the invariant verification on self.

Note: All properties defined in object are considered as pure and therefore they don't have an invariant facet. This offers two advantages, we avoid an overcost on all the classes that will use object properties, as well as a problematic for checking null type (== and !=).

class MyClass
    invariant(bar == 10)

    var bar: Int = 10   

    fun foo(x: Int)
    do
        [...]
    end
end

Representation of the compiled class

class Object
    fun _invariant
    do
        [Empty body]
    end
end

class MyClass
    invariant(bar == 10)

    var bar: Int = 10   

    fun _invariant
    do
        super
        assert bar == 10
    end

    fun _contract_bar=(x: Int)
    do
        foo(x)
    end

    fun _contract_inv_bar(x: Int)
    do
        _contract_bar
        _invariant
    end

    fun foo(x: Int)
    do
        [...]
    end

    fun _contract_inv_foo(x: Int)
    do
        _contract_foo(x)
        _invariant
    end 

    fun _contract_foo(x: Int)
    do
        foo(x)
    end 
end

The invariant method was added on the object class to resolve multi inheritance problem with a systematic call to super.

Option

Invariant contracts are normally supposed to be checked in enter and exit. But in Nit the verification is only made at the exit of the method. It is however possible to activate the checking of the input and output invariants with the --in-out-invariant option.

Refactoring

Now the contract toolcontext options are defined in the contract module. It's seems to be a better place to keep the options and the implementation in the same module.

[github-actions[bot]]

Test Results

    67 files     338 suites   17m 33s :stopwatch: 14 227 tests 13 684 :white_check_mark: 543 :zzz: 0 :x: 14 683 runs  14 125 :white_check_mark: 558 :zzz: 0 :x:

Results for commit dbe708a4.