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]

Test Results

    67 files     338 suites   17m 33s ⏱️
14 227 tests 13 684 ✅ 543 💤 0 ❌
14 683 runs  14 125 ✅ 558 💤 0 ❌

Results for commit dbe708a.