Contract implementation

[Delja]

Contract.

This pr is a copy of #2747 with some modifications. It has a dependency with the #2779 and #2788.

Adding programming by contract (Design by contract) in Nit language. Contracts works with nit annotations. I decided to cut the contract pr in a smaller part to facilitate reviewing (some feature are not available on it, see section futur feature).

Annotations

To define a new contract you need to use the corresponding annotation. For example it's possible to define a contract that x parameter must be strictly greater than 5. To do it would be necessary to define the contract in the following way expects(x > 5). All expressions returning a boolean (comparison...) can be used as a condition.

Three annotations were added:

• expects to indicate the conditions need to the execution of the methods
• ensures to indicate the conditions of guarantee at the end of the execution of the methods
• no_contract to remove the inherited contract

This syntaxe is choose because in the next version of c++ (20) (see P1369 for a overview) the contract will be define with the keywords expects and ensures. So I think it would be interesting to keep the same principle. But if all nit developper prefer to use require and ensure it's fine to change it.

Method contract (ensures, expects)

For each method it's possible to define preconditions (expects) and post-conditions (ensures). If the call of the method satisfies the prerequisites (expects) of the method, the caller may assume that the return conditions (ensures) will be satisfied.

The method contracts can access all the parameters of the method as well as the set of attributes/methods visible in the context of the method. i.e the set of parameters and the set of methods and attributes of the current class can be used (attributes declare locally in the method can not be used). For post-conditions (ensures) the result attribute has been added to perform a check on the return value of the method. Currently it's not possible to refer an old value in a ensures (exemple old(length) == length + 1).

Process

Building contract phase

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

• The method is annotated (redefined or not)

• The method is a redefinition of a method already having a contract (i.e a method that does not add any new conditions to the existing contract).

When a contract is detected the code is extended to add the verification features. Two methods are created. The first method is the contract face. Its goal is to provide the call of the contract verification and the call of the original method. With this strategy, the original code of the method is preserved. The second created method is for the contract verification.

Exemple

Expect:

class MyClass
    fun foo(x: Int)
    is
        expects(x > 0)
    do
        [...]
    end
end

Representation of the compiled class

class MyClass
    fun foo(x: Int)
    is
        expects(x > 0)
    do
        [...]
    end

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

    fun _expects_foo(x: Int)
    do
        assert x > 0
    end
end

Ensure:

class MyClass
    fun foo(x: Int): Bool
    is
        ensures(result == true)
    do
        [...]
        return true
    end
end

Representation of the compiled class

class MyClass
    fun foo(x: Int): Bool
    is
        ensures(result == true)
    do
        [...]
        return result
    end

    fun _contract_foo(x: Intl): Bool
    do
        var result = foo(x)
        _ensures_foo(x, result)
        return result
    end

    fun _ensures_foo(x: Int, result: Bool)
    do
        assert result == true
    end
end

Inheritance

Contracts support redefinition and adding condition. Note that when a contract is define in a parent class, it's no longer possible to remove this contract on all the classes that inherit or redefine them. They only need to be increased according to different subtyping rules.

All preconditions (expects) can be weakened. i.e it's possible to provide a new alternative to validate the contract. This corresponds to the use of a logical OR between the old and the new conditions.

All post-conditions (ensure) can be consolidate. i.e the new condition of the contract will provide a new guarantee to the user of the method. This rule can be translates into a logical AND between the old and the new conditions.

Exemple

Expect

class SubMyClass
    super MyClass

    redef fun foo(x: Int)
    is
        expects(x > 0, x == 0)
    do
        [...]
    end

    redef fun _expects_foo(x: Int)
    do
        if x == 0 then return
        super(x)
    end

    redef fun _contract_foo(x: Int)
    do
        _expects_foo
        super(x)
    end

end

Ensure

class SubMyClass
    super MyClass

    redef fun foo(x: Int): Bool
    is
        ensures(result == true, x > 0)
    do
        [...]
    end

    redef fun _ensures_foo(x: Int, result: Bool)
    do
        super
        assert super(x, result)
    end

    redef fun _contract_foo(x: Int, result: Bool): Bool
    do
        var result = super
        _ensures_foo(x, result)
        return result
    end
end

Summary

Annotation	Inheritance condition type
expects	and
ensures	or

Invocation

All calls to contract methods are intercepted to call the contract version. For the moment the contracts are systematically called, whether it's an internal or external call. Only calls to super do not execute the contracts.

This part is subject to evolution with a parameter to activate or not the internal call verification.

Building

Since contracts are expensive in resource, several levels of use have been defined based on the needed verification:

• No contract: all contracts are disable (option --no-contract).

• Default: By default the contracts can be defined as "semi-global". I.E. All contracts (ensures, expects)used in the main package are enabled, the expects contracts are enabled (ensures contracts are disable) in direct imported package. Other indirected imported package doesn't have active contract.

• Full contract: Contracts are enable (ensures, expects) on all classes (option --full-contract).

Future work

This pr has been simplified to facilitate the reviewing.

Future features:

• Support class invariant contracts
• Ability to put contracts on auto-getters and setter
• Detection of query or command to avoid the contract to change the object state (this functionality will probably be an advice because it's difficult to define if a method has no side effect.)
• Old support for the ensures contract to refer at the same value during the expects condition

Some pr will follow to use the contacts directly in the lib (collection...).

Note

Currently the syntax of contracts is strict, only comparisons and method calls returning bouleans can be used. Indeed the arguments passed to the annotation of contract are directly used for assert. A solution would be given a more open syntax for more complex contracts instead of using a method. But this would cause problems in the syntax of annotations. If you have any suggestion don't hesitate. An issue is available to talk about the potential syntax. (#1340)