# 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](http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1369r0.pdf) 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:
```nit
class MyClass
fun foo(x: Int)
is
expects(x > 0)
do
[...]
end
end
```
Representation of the compiled class
```nit
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:
```nit
class MyClass
fun foo(x: Int): Bool
is
ensures(result == true)
do
[...]
return true
end
end
```
Representation of the compiled class
```nit
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
```nit
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
```nit
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)
Pull-Request: #2790
Reviewed-by: Jean Privat <jean@pryen.org>
nitlanguage / nit.git / commitdiff