doc/manual: Add contract manual

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

doc/manual/contract.md

@@ -0,0 +1,175 @@
+# Contract Programming
+
+Nit supports contract programming like Eiffel. 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.
+
+In Nit all the conditions of contract must be expressed using boolean expression in the same way as an assertion. Note that the potential routines that compose the condition of the contract should have no side effects.
+
+## Method/Attribute contract
+
+Methods and attributes (setter) can be associated with two types of contracts, entry contracts (expect) and exit contracts (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 fulfills the `ensure` condition on exit.
+
+Both are declared, between the definition of the signature followed by the keyword `is` and the block start keyword `do`.
+
+### Expect
+
+We define a precondition using the annotation `expect`. Here is an example with a `pop` method which removes the last element of the stack. It defines as a precondition to its call that the stack must not be empty.
+
+~~~
+	fun pop
+	is
+		expect(not_empty)
+	do
+		# Remove the last item on the stack
+	end
+~~~
+
+### Ensure
+
+We define a postcondition using the annotation `ensure`. Here is an example with a `push` method which adds the element received as an argument (`object`) at the top of the stack. It garantees to the caller that the object will be added at the top of the stack `self [size] == object`.
+
+~~~
+	fun push(object: T)
+	is
+		ensure(self[size] == object)
+	do
+		# Add the given argument `object` on top of the stack
+	end
+~~~
+
+The `ensure` contract offers the possibility of referring to the return value of the method, using the keyword `result`. Example the `get_at` method which returns the object which is stored at the index received as an argument (`index`). It guarantees the caller that the returned element represented by `result` corresponds to the element stored in the stack with the given index `result == self [index]`.
+
+~~~
+	fun get_at(index: Int): T
+	is
+		ensure(result == self[index])
+	do
+		# Return the element at the given index.
+	end
+~~~
+
+In `ensure` we can refer to any arguments and instance variables before the method call with the using of `old` keyword. Again, using the pop example, 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)
+	do
+		# Remove the last item on the stack
+	end
+~~~
+
+### Additional informations
+
+* When defining a `ensure` or `expect` contract on an attribute, only the automatically generated write property will use the contract.
+
+~~~
+	var baz: Int is expect(baz > 0) # In the contract, baz refers to the parameter of the write property (setter).
+~~~
+
+* The `ensure` or `expect` contracts are evaluated in the same context as the called method, it's possible to refer to attributes, methods and parameters in the condition.
+
+* In `ensure` contracts, the keyword `result` can only be used when the method has a return parameter.
+
+* The expression contained in an `old` 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 expresion `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.
+
+* Contracts can be declared in several ways, all are equivalent:
+
+~~~
+	fun foo(a: Int, b: Int)
+	is
+		ensure(a > 0, b < 0)
+	do
+		# Do something
+	end
+
+
+	fun foo
+	is
+		ensure(a > 0 and b < 0)
+	do
+		# Do something
+	end
+
+
+	fun foo
+	is
+		ensure(a > 0)
+		ensure(b < 0)
+	do
+		# Do something
+	end
+~~~
+
+
+## Class/interface
+
+### Invariant
+
+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)
+	end
+~~~
+
+### Additional informations
+
+* The invariant is only checked at the end of a constructor.
+
+* By default, the invariants are only checked on exit. See section `Verification policy` to activate them on in and out.
+
+## 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 promises initially defined by all previous contractors. 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.
+
+* The `ensure` can be reinforced, which guarantees that all of the expected results introduced in the previous definitions will be respected. During the specialization of a method it will be possible to redefine its postcondition in order to restrict the possible outputs.
+
+* The `invariant` can be reinforced, which guarantees that constraints of validated state previously defined in the superclasses/interfaces will 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.
+
+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).
+
+## Runtime
+
+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.
+
+### Execution order
+
+For the public methods/attribute, the evaluation order is as follows:
+
+1- invariant
+2- preconditions (`expect`)
+3- called property
+4- postconditions (`ensure`)
+5- invariant
+
+For constructors only the 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.