diff --git a/doc/manual/contract.md b/doc/manual/contract.md new file mode 100644 index 0000000000..76cc496b42 --- /dev/null +++ b/doc/manual/contract.md @@ -0,0 +1,421 @@ +# Contract Programming + +Nit supports [contract programming](https://en.wikipedia.org/wiki/Design_by_contract). Contracts can be seen as the materialization of specifications in the code itself. The idea is to define the behavior of a property using conditions which will be evaluated on runtime. A contracts define the relations between a property and all its potential callers. If one of the two parties (callee/caller) does not respect the defined rules, the contract is considered to be broken and will cause a runtime error. + +You can put contracts on different elements of the language: methods, attributes, interfaces and classes in order to verify the conformity of the implementation compared with the specification. Different types of contracts exist; the preconditions (`expect`) which check the conditions before execution, the postconditions (`ensure`) which checks the conditions after execution and the invariants (`invariant`) which checks that the conditions remain unchanged. + +The implementation of contracts is recommended when we are dealing with business rules. For example when we are developing a library it may be necessary to specify contracts to guarantee valid usages of wer API. Also, contracts support inheritance, which guarantees that contracts will be satisfied in future specification. + +Let us take a look at the `Stack` class bellow: + +~~~ + class Stack[T] + invariant(size >= 0) + + var data = new Array[T] + + var size = 0 + + fun is_empty: Bool + is + ensure(result == (size == 0)) + do + return size == 0 + end + + # Add `item` on top of the stack + fun push(item: T) + is + ensure(size == old(size) + 1) + ensure(data[size-1] == item) + do + top += 1 + data[top] = item + end + + # Remove the item on top of the stack + fun pop + is + expect(not is_empty) + ensure(size == old(size) - 1) + do + data.pop + top -= 1 + end + + # Return the item at the given index. + fun [](index: Int) + is + expect(index < size) + expect(index >= 0) + ensure(result == data[index]) + do + return data[index] + end + end +~~~ + +As we can see the contracts are defined using several annotations: `invariant` which designates the class invariants, `expect` which designates the preconditions and `ensure` which designates the postconditions. The conditions of a contract must be expressed using boolean expressions in the same way as assertions. Each contract of this example will be detailed in the sections below. + +By default when you compile or interpret (`nitc stack.nit` or `nit stack.nit`) a program, contracts are enabled in "semi-global" mode. i.e. All contracts (`ensure`, `expect`, `invariant`) used in the main module are enabled, direct imported modules have only the expects contracts enabled (`ensure` and `invariant` contracts are disabled). The other indirect imported modules don't have active contracts. We can use options to change the contract rule see `Options` section for more information. + +All contracts conditions can be declared in several ways, all are equivalent: +~~~ + fun foo(a: Int, b: Int) is ensure(a > 0, b < 0) + + fun foo is ensure(a > 0 and b < 0) + + fun foo is ensure(a > 0), ensure(b < 0) +~~~ + +## Writing contracts + +Methods, as well as attribute setters, can be associated with two types of contracts, entry contracts precondition (`expect`) and exit contracts postcondition (`ensure`). Together, they define the rules to be respected between the callee and the caller. If the caller fulfills the `expect` condition on entry then the caller can assume that the callee fulfill the `ensure` condition on exit. + +All contracts (`expect`, `ensure`) are evaluated in the same context as the called method, it's possible to refer to attributes, methods and parameters in the condition. + +When defining a contract (`expect`, `ensure`) on an attribute like bellow, only the automatically generated write property (setter) will use the contract. + +~~~ + var baz: Int is expect(baz > 0) # In the contract, baz refers to the parameter of the write property (setter). +~~~ + +### Define preconditions with `expect` + +We define a precondition using the annotation `expect`. In the `Stack` class, the method `pop` defines a precondition, that a call to the method should be made on a non-empty stack. + +~~~ + fun pop is expect(not_empty) +~~~ + +### Define postconditions with `ensure` + +We define a postcondition using the annotation `ensure`. In the `Stack` class, the method `push` defines postconditions. The first guarantee defines that, the method must add the element received as argument (`object`) at the top of the stack. + +~~~ + fun push(object: T) is ensure(self[size - 1] == object) +~~~ + +Within an `ensure` contract we can refer to the return value of the method with the keyword `result`. In the `Stack` class, the `[]` method guarantees that, the return value is the same as the element stored in the stack at the given index. + +~~~ + fun [](index: Int): T is ensure(result == data[index]) +~~~ + +Note that the keyword `result` can only be used when the method has a return parameter. + + +In `ensure` we can refer to any arguments and instance variables before the method call with the using of `old` keyword. Again, with the `pop` method, we can ensure that the `size` of the stack after the method call will be the same as before minus one `old(size) - 1 == size`. + +~~~ + fun pop(object: T) is ensure(old(size) - 1 == size) +~~~ + +In an `old(expression)` the `expression` is evaluated in the same context as the called method. Thus, it's possible to refer to attributes, methods, and arguments. + +`old(object)` stores a reference to object. By doing so, if `object` is mutated in the method the `old (object)` will also be mutated. To avoid this, it's necessary to provide a way to duplicate the object like `clone` method so that `not old(object.clone).is_same_instance (object)` will be true. In the stack example, the expression `old(stack).is_same_instance(stack) && old(stack.size) != old(stack).size` is true. If we need to `old(stack).is_same_instance(stack)` to be false, we need to provide a method to duplicate the object, such as `not old(stack.clone).is_same_instance(stack)` be true. + +## Writing invariants + +Invariants are used to specify the characteristics of a class/interface which must always be true, except when executing a member function. In other words, invariants define conditions that must be respected by our instance. Any instance which does not respect one or more of those conditions will be considered as incoherent. + +To define an invariant we use the class annotation `invariant`. Here is an example with our Stack. The class defines that it is impossible to be in a state where the size is less than 0. + +~~~ + class Stack + invariant(size >= 0) + end +~~~ + +Another example with a class that represents a date (day, month). To be in a consistent state, the date must be represented with a day between 1 and 31 and a month between 1 and 12. + +~~~ + class Date + invariant(day >= 1 and day <= 31) + invariant(month >= 1 and month <= 12) + + var day: Int + var month: Int + end +~~~ + +When a class defines an invariant all methods and constructors (inherited, redefined and introduced) will check this one. By default, the invariants are only checked on exit. See section `Verification policy` to activate them on in and out. For all constructors the invariant is only checked at the end of this, this is due to the fact that the object is not yet initialized. See the section `Execution order` for example. + +The invariant is not checked when the calle is on `self`. The following example shows the execution of invariant: + +~~~ + class A + invariant(print_invariant) + + fun print_invariant: Bool + do + print "In invariant verification" + return true + end + + fun foo + do + print "In foo" + self.bar # The called property is a member of "self", the invariant will not be checked. + end + + fun bar + do + print "In bar" + end + end + + var a = new A + a.foo # The called property is not a member of "self", the invariant will be checked. +~~~ + +This example gives the following output: +~~~ +In invariant verification +In foo +In bar +In invariant verification +~~~ + +## Inheritance + +The Nit contracts fully support multiple inheritance and refinement. The specialization can be interpreted as subcontracting. All methods, class/interface which are redefined must keep the set of conditions defined by all the previous definitions. Here are the subtyping rules for each type of the contracts: + +* The `expect` can be weakened, which guarantees that all the contracts introduced in the previous definitions will always be considered as valid entries. During the specialization of a method it will be possible to redefine its precondition in order the widen the allowed input. + +Example: +~~~ + class MyClass + fun foo(x: Int) is abstract, expect(x == 0) + end + + class MySub + super MyClass + + redef fun foo(x: Int) is expect(x == -1) + end + + class MySubSub + super MySub + + redef fun foo(x: Int) is expect(x == -2) + end +~~~ + +| Class | Condition of `foo(x)` | +|----------|--------------------------------| +| MyClass | `x == 0` | +| MySub | `x == 0 or x == -1` | +| MySubSub | `x == 0 or x == -1 or x == -2` | + +When refinement a precondition (`expect`) the new condition is equivalent to an `or` between the set of inherited preconditions. + +* The `ensure` can be reinforced, which guarantees that all of the expected results introduced in the previous definitions must be respected. During the specialization of a method it will be possible to redefine its postcondition in order to restrict the possible outputs. + +Example: +~~~ + class MyClass + fun foo: Int is abstract, ensure(result > 0) + end + + class MySub + super MyClass + + redef fun foo: Int is abstract, ensure(result > 10) + end + + class MySubSub + super MyClass + + redef fun foo: Int is abstract, ensure(result > 100) + end +~~~ + +| Class | Condition of `foo` | +|----------|-----------------------------------------------| +| MyClass | `result > 0` | +| MySub | `result > 0 and result > 10` | +| MySubSub | `result > 0 and result > 10 and result > 100` | + +When refinement a postcondition (`ensure`) the new condition is equivalent to an `and` between the set of inherited postconditions. + +* The `invariant` can be reinforced, which guarantees that constraints of validated state previously defined in the superclasses/interfaces must be respected. The specialization of a class makes it possible to restrict all of the valid states. The objective is that an object must always be considered as a coherent value of all of its superclasses/interfaces. + +Example: +~~~ + class MyClass + invariant(i > 0) + var i: Int + end + + class MySub + super MyClass + invariant(i > 10) + end + + class MySubSub + super MySub + invariant(i > 100) + end +~~~ + +| Class | Condition of `invariant` | +|----------|--------------------------------| +| MyClass | `i > 0` | +| MySub | `i > 0 and i > 10` | +| MySubSub | `i > 0 and i > 10 and i > 100` | + +When we specialize or refine a class, its invariant is equal to an `and` between the set of inherited invariants and the new condition. + +Nit however offers the possibility of removing the inheritance of contracts with the `no_contract` annotation (use this annotation only when it's really necessary). + +Example: +~~~ + class MyClass + fun foo(x: Int) is abstract, ensure(x == 0) + end + + class MySub + super MyClass + + redef fun foo(x: Int) is no_contract + end +~~~ + +| Class | Condition of `foo(x)` | +|---------|-----------------------| +| MyClass | `i == 0` | +| MySub | `Null` | + +## Execution + +When performing the evaluation of a contract, all routines and elements will be executed without the evaluation of contracts. The objective is to remove the potential risk of falling into an infinite loop of verification. + +Now we add a small test program to see the contract of `Stack` class in action: + +~~~ + var stack = new Stack[String] + stack.push("Banana") + stack.push("Coconut") + # stack.get_at(5) # Causes an assertion failed because the given index is > size + stack.pop + stack.pop + # stack.pop # Causes an assertion failed because the stack is empty + # stack.size = -1 # Causes an assertion failed because a stack cannot have a size < 0 +~~~ + +### Execution order + +~~~ + class A + invariant(i > 10) + + var i: Int + + init default(i: Int) + is + expect(i > 0) + ensure(self.i = i + 10) + do + _i = i + 10 + end + + fun foo(x: Int): Bool + is + expect( x > 0 ) + ensure( result == true ) + do + return true + end + end + + var a = new A(2) + a.foo +~~~ + +This is the evaluation order of the `var a = new A(2)`: + +1- preconditions (`expect(i > 0)`) +2- called property (execution of the method body) +3- postconditions (`ensure(self.i = i + 10)`) +4- invariant (`invariant(i > 10)`) + +This is the evaluation order of the `a.foo`: + +1- invariant (`invariant(i > 10)`) +2- preconditions (`expect( x > 0 )`) +3- called property (execution of the method body) +4- postconditions (`result == true`) +5- invariant (`invariant(i > 10)`) + +In redefinition when you make a call to `super` the contracts is not checked again. + +Example: +~~~ + class A + fun print_expect: Bool + do + print "In expect A" + return true + end + + fun foo + is + expect(print_expect) + do + print "In foo of A" + end + end + + classe B + super A + + fun print_new_expect: Bool + do + print "In expect B" + return true + end + + redef fun foo + is + expect(print_new_expect) + do + super + print "In foo of B" + end + end + + var b = new B + b.foo +~~~ + +This example gives the following output: +~~~ +In expect B +In foo of A +In foo of B +~~~ + +Note this example also shows the fact that during elevations of `expect` in an inheritance frame when one of the `expect` conditions is satisfied we stop the verification. + +To summarize the evaluation order for public methods/attribute, is as follows: + +1- invariant +2- preconditions (`expect`) +3- called property +4- postconditions (`ensure`) +5- invariant + +For constructors only the invariant verification in entry (first step) is ignored. + +### Options + +Here is the list of options to manage contract verification: + +`--full-contract`: Enable contracts on all modules. Warning: this is an expensive option at runtime. + +`--no-contract`: all contracts are disabled. + +`--in-out-invariant`: Enable `invariant` verification on entry and exit. By default, invariants are only checked on exit + +`--no-self-contract`: Disables all contracts on member routines of the same instance.