doc/manual: Add contract manual

Signed-off-by: Florian Deljarry <[email protected]>

doc/manual/contract.md

@@ -0,0 +1,329 @@
+# 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 contract define the relations between a property and all the 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 contract 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 type of contracts exists; 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 you are dealing with business rules. For example when you are developing a library it may be necessary to specify contracts to guarantee valid use of the 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 do return size == 0
+
+		# Add the given argument `object` on top of the stack
+		fun push(object: T)
+		is
+			ensure(size == old(size) + 1)
+			ensure(data[size-1] == object)
+		do
+			top += 1
+			data[top] = object
+		end
+
+		# Remove the last item on the stack
+		fun pop
+		is
+			expect(not is_empty)
+			ensure(size == old(size) - 1)
+		do
+			data.pop
+			top -= 1
+		end
+
+		# Return the element at the given index.
+		fun get_at(index: Int): T
+		is
+			expect(index < size)
+			ensure(result == self[index])
+		do
+			return self[index]
+		end
+	end
+~~~
+
+As you 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 a section below.
+
+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 you can refer to the return value of the method with the keyword `result`. In the `Stack` class, the `get_at` method guarantees that, the return value is the same as the element stored in the stack at the given index.
+
+~~~
+	fun get_at(index: Int): T is ensure(result == self[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, 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 you need to `old(stack).is_same_instance(stack)` to be false, you 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. Finally, invariants must hold before and after any method called (except those called by `self` directly).
+
+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.
+
+## Inheritance
+
+The Nit contracts fully support inheritance (single or multiple) and refinement. The specialization can be interpreted as subcontracting. Subcontracting element must keep the set of conditions defined by all previous contractors. Nous alons prendre pour example la définition. 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
+	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)`)
+
+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.
+
+### Verification policy
+
+Since contracts are expensive in resource, Nit offers several levels of contract verification :
+
+Default: In default mode the contracts can be defined as "semi-global". I.E. All contracts (ensure, expect, invariant) used in the main modules are enabled, expects contracts are enabled (ensure, invariant contracts are disable) in direct imported modules. Other indirected imported modules doesn't have active contract.
+
+Full contract: Enable contracts on all modules(`--full-contract` option). Warning: this is an expensive option at runtime.
+
+No contract: all contracts are disabled (option --no-contract).
+
+In out invariant: As indicated previously, invariants are enabled only in exit. It is, however, possible to activate them on entry and exit with the `--in-out-invariant` option.
+
+No self contract: Disables all contracts on member routines of the same instance.