Contracts: Add invariant contract

[Delja]

This pr adds a two major feature in the contracts, the addition of invariants as well as the care of the old in the ensure.

Annotations

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

Invariant generation process

Building contract phase

A phase is executed to check all classes and methods. This check is done to know if:

• The class is annotated (redefined or not)

When a contract is detected the code is extended to add the verification features. One method is created. This method is the contract invariant verification.

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

Exemple

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 has added on the object class to resolve multi inheritance problem.

Old generation process

Now when a ensure contract has been declared a check is made to see if a call with the name old is made. If this is the case we :

• Store all expressions that call old.
• Create a new old class for the visited ensure.
• Add new attributes in the class to capture old values.
• Create a method to instantiate our new old class.

Note: The information that is kept by the old is a reference to the designated object. If the old designate a non-immutable complex object, it will be necessary to use a cloning method to duplicate the object.

Exemple:

class MyClass
    fun add_one(i: Int): Int 
    is 
        ensure(old(i) + 1 == result)
    do
        return i + 1
    end
end

Representation of the compiled class

class MyClass
    fun add_one(i: Int): Int 
    is 
        ensure(old(i) + 1 == result)
    do
        return i + 1
    end

    fun _contract_add_one(i: Int): Int
    do
        var old =  _init_old_add_one(i, new Old_MyClass_add_one)
        result = add_one(i)
        ensure_add_one(i, result, old)
        return result
    end

    fun _init_old_add_one(i: Int, old: Old_MyClass_add_one): Old_MyClass_add_one
    do
        old.i = i
        return old
    end
end

class Old_MyClass_add_one
    var i: nullable Int
end

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.

Other features

Option to disable contract verification in self

The --no-self-contract was added to disable the contract verification on self.

Add contrat on attribut

It is now possible to add contracts on the attributes (expect and ensure). Only the setter have a contract feature.

Exemple:

class MyClass

    var bar: Int is ensure(self.bar != 10)  
end

Representation of the compiled class

class MyClass

    var _bar: Int

    fun bar=(x: Int)
    do
        _bar = x
    end

    fun contract_bar=(x: Int)
    do  
        bar=(x)
        ensure_bar(x)
    end

    fun ensure_bar(x: Int)
    do
        assert(self.bar != 10)
    end
end

Disable warning on TypingVisitor

This pr adds a way to disable warnings in typing when we are manipulating generate code.This pr include the invariant contract.

NitBuilder introduction

This module help the instantiation and transformation of language entities (AST and model). The objectif of this module is to help the creation of entities language (Attributes, Methods, Class).