From: Jean Privat <jean@pryen.org>
Date: Mon, 8 Jun 2020 19:58:00 +0000 (-0400)
Subject: Merge: Contract refactoring
X-Git-Url: http://nitlanguage.org?hp=3fe03dff9c095c2a3bd743982fa3a14796d69930

Merge: Contract refactoring

This pr do the following changes:

* Authorize the declaration of identical contracts on the same method in order to facilitate the reading of contracts. Example
```nit
fun foo(x, y: Int)
is
	expect(x > 0)
	expect(y > 0)
do end
```

* Modification of the generation of contracts. In the default mode, the contracts are now generated even if they are not used, only the public facet is generated only if it is necessary. The objective is to provide the contracts verification when you are in a redefinition in a module where contracts must be applied. This solution is a compromise to try to keep acceptable performance in the default mode. Example

```nit
module one
import two
[...]

module two
import three

redef class C
	# Now all calls to foo of c (only in module one or two) check the `expect` property defined in module three (as defined by the default contract rule).
	redef foo ...
end

module three

class C
	fun foo is expect(true), ensure(true)
end
```

* When a contract is not fulfilled the messages displayed to the user are now more explicit. Example:

```nit\
class A
	fun foo(i: Int) is expect(i > 0) do end
end

var a = new A
a.foo(0)
```
This is the output of the program
```
Runtime error: Assert 'expect(i > 0)' failed
```

* Cosmetic modifications have been made to remove useless methods, modify the names and comments of certain methods to be more explicit.

Pull-Request: #2827
---

diff --git a/src/contracts.nit b/src/contracts.nit
index af45112..3d300ff 100644
--- a/src/contracts.nit
+++ b/src/contracts.nit
@@ -124,52 +124,18 @@ private class ContractsVisitor
 	end
 
 	# Define the new contract take in consideration that an old contract exist or not
-	private fun build_contract(n_annotation: AAnnotation, mcontract: MContract, mclassdef: MClassDef): MMethodDef
+	private fun build_contract(n_annotations: Array[AAnnotation], mcontract: MContract, mclassdef: MClassDef)
 	do
-		self.current_location = n_annotation.location
+		var n_conditions = new Array[AExpr]
 		# Retrieving the expression provided in the annotation
-		var n_condition = n_annotation.construct_condition(self)
-		var m_contractdef: AMethPropdef
+		for n_annotation in n_annotations do n_conditions.add n_annotation.construct_condition(self)
 		if is_intro_contract then
 			# Create new contract method
-			m_contractdef = mcontract.create_intro_contract(self, n_condition, mclassdef)
+			mcontract.create_intro_contract(self, n_conditions, mclassdef)
 		else
 			# Create a redef of contract to take in consideration the new condition
-			m_contractdef = mcontract.create_subcontract(self, n_condition, mclassdef)
+			mcontract.create_subcontract(self, n_conditions, mclassdef)
 		end
-		var contract_propdef = m_contractdef.mpropdef
-		# The contract has a null mpropdef, this should never happen
-		assert contract_propdef != null
-		return contract_propdef
-	end
-
-	# Verification if the construction of the contract is necessary.
-	# Three cases are checked for `expect`:
-	#
-	# - Was the `--full-contract` option passed?
-	# - Is the method is in the main package?
-	# - Is the method is in a direct imported package?
-	#
-	fun check_usage_expect(actual_mmodule: MModule): Bool
-	do
-		var main_package = mainmodule.mpackage
-		var actual_package = actual_mmodule.mpackage
-		if main_package != null and actual_package != null then
-			var condition_direct_arc = toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package)
-			return toolcontext.opt_full_contract.value or condition_direct_arc or main_package == actual_package
-		end
-		return false
-	end
-
-	# Verification if the construction of the contract is necessary.
-	# Two cases are checked for `ensure`:
-	#
-	# - Was the `--full-contract` option passed?
-	# - Is the method is in the main package?
-	#
-	fun check_usage_ensure(actual_mmodule: MModule): Bool
-	do
-		return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
 	end
 
 	# Inject the incontract attribute (`_in_contract_`) in the `Sys` class
@@ -265,9 +231,10 @@ private class CallSiteVisitor
 		node.visit_all(self)
 	end
 
-	# Check if the callsite calls a method with a contract.
-	# If it's the case the callsite is replaced by another callsite to the contract method.
-	private fun drive_method_contract(callsite: CallSite): CallSite
+	# Check if the callsite is bound on a property with a contract.
+	# If the property is linked to a contract a new callsite will be created towards the correct facet,
+	# in the other case the returned callsite wall be the same as the given `callsite`
+	private fun drive_callsite_to_contract(callsite: CallSite): CallSite
 	do
 		var contract_facet = callsite.mproperty.mcontract_facet
 		var visited_mpropdef = visited_propdef.mpropdef
@@ -295,32 +262,39 @@ redef class AAnnotation
 		var n_condition = n_args.first
 		n_args.remove_at(0)
 		for n_arg in n_args do n_condition = v.ast_builder.make_and(n_condition, n_arg)
+		n_condition.location = self.location
 		return n_condition
 	end
 end
 
 redef class MContract
 
-	# Define the name of the contract
-	fun contract_name: String is abstract
+	# Should contract be called?
+	# return `true` if the contract needs to be called.
+	private fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool
+	do
+		return v.toolcontext.opt_full_contract.value
+	end
 
 	# Method use to diplay warning when the contract is not present at the introduction
-	private fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)do end
+	private fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])do end
 
 	# Creating specific inheritance block contract
-	private fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr is abstract
+	#
+	# `super_args` : Correspond to the `super` call arguments
+	private fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr is abstract
 
-	# Method to adapt the `n_mpropdef.n_block` to the contract
-	private fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) is abstract
+	# Method to adapt the given `n_mpropdef.n_block` to the contract
+	private fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef) is abstract
 
-	# Adapt the msignature specifically for the contract method
+	# Create and return an adapted `MSignature` specifically for the contract in fonction of the given `m_signature`
 	private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_contract
 
-	# Adapt the nsignature specifically for the contract method
+	# Create and return an adapted `ASignature` specifically for the contract in fonction of the given `n_signature`
 	private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_contract
 
 	# Adapt the `m_signature` to the contract
-	# If it is not null call the specific adapt `m_signature` for the contract
+	# If `m_signature == null` return a new `MSignature` else it calls a specific adapt method see `adapt_specific_msignature`
 	private fun adapt_msignature(m_signature: nullable MSignature): MSignature
 	do
 		if m_signature == null then return new MSignature(new Array[MParameter])
@@ -328,20 +302,13 @@ redef class MContract
 	end
 
 	# Adapt the `n_signature` to the contract
-	# If it is not null call the specific adapt `n_signature` for the contract
+	# If `n_signature == null` return a new `ASignature` else it calls a specific adapt method see `adapt_specific_nsignature`
 	private fun adapt_nsignature(n_signature: nullable ASignature): ASignature
 	do
 		if n_signature == null then return new ASignature
 		return adapt_specific_nsignature(n_signature)
 	end
 
-	# Create a new empty contract
-	private fun create_empty_contract(v: ContractsVisitor, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature)
-	do
-		var n_contract_def = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, msignature, n_signature)
-		n_contract_def.do_all(v.toolcontext)
-	end
-
 	# Create the initial contract (intro)
 	# All contracts have the same implementation for the introduction.
 	#
@@ -353,43 +320,65 @@ redef class MContract
 	# end
 	# ~~~
 	#
-	private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
+	private fun create_intro_contract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef)
 	do
 		var n_block = v.ast_builder.make_block
-		if n_condition != null then
+		for n_condition in n_conditions do
 			# Create a new tid to set the name of the assert for more explicit error
-			var tid = new TId.init_tk(self.location)
-			tid.text = "{self.contract_name}"
-			n_block.add v.ast_builder.make_assert(tid, n_condition, null)
+			var tid = new TId.init_tk(n_condition.location)
+			tid.text = "{n_condition.location.text}"
+			var n_assert = v.ast_builder.make_assert(tid, n_condition, null)
+			# Define the assert location to reference the annoation
+			n_assert.location = n_condition.location
+			n_block.add n_assert
 		end
-		return make_contract(v, n_block, mclassdef)
+		make_contract(v, n_block, mclassdef)
 	end
 
-	# Create a contract with old (super) and the new conditions
-	private fun create_subcontract(v: ContractsVisitor, ncondition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
+	# Create a contract to check the old (super call) and the new conditions
+	#
+	# Example:
+	# ~~~nitish
+	# fun contrat([...])
+	# do
+	#	super # Call the old contracts
+	#	assert new_condition
+	# end
+	# ~~~
+	#
+	private fun create_subcontract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef)
 	do
 		var args = v.n_signature.make_parameter_read(v.ast_builder)
 		var n_block = v.ast_builder.make_block
-		if ncondition != null then n_block = self.create_nblock(v, ncondition, args)
-		return make_contract(v, n_block, mclassdef)
+		n_block = self.create_inherit_nblock(v, n_conditions, args)
+		make_contract(v, n_block, mclassdef)
 	end
 
-	# Build a method with a specific block `n_block` in a specified `mclassdef`
-	private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef): AMethPropdef
+	# Build a new contract method with a specific block `n_block` in a specified `mclassdef`
+	private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef)
 	do
-		var n_contractdef = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, v.m_signature, v.n_signature)
+		var n_contractdef = v.toolcontext.modelbuilder.create_method_from_property(self, mclassdef, false, v.m_signature)
+		# Set the signature to keep the same variable
+		n_contractdef.n_signature = v.n_signature
 		n_contractdef.n_block = n_block
 		# Define the location of the new method for corresponding of the annotation location
 		n_contractdef.location = v.current_location
 		n_contractdef.do_all(v.toolcontext)
-		return n_contractdef
 	end
 end
 
 redef class MExpect
 
-	# Define the name of the contract
-	redef fun contract_name: String do return "expect"
+	redef fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool
+	do
+		var main_package = v.mainmodule.mpackage
+		var actual_package = mpropdef.mclassdef.mmodule.mpackage
+		if main_package != null and actual_package != null then
+			var condition_direct_arc = v.toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package)
+			return super or main_package == actual_package or condition_direct_arc
+		end
+		return false
+	end
 
 	# Display warning if no contract is defined at introduction `expect`,
 	# because if no contract is defined at the introduction the added
@@ -415,58 +404,68 @@ redef class MExpect
 	# end
 	# ~~~~
 	#
-	redef fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)
+	redef fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])
 	do
-		v.toolcontext.warning(a.location,"","Useless contract: No contract defined at the introduction of the method")
+		v.toolcontext.warning(a.first.location,"useless_contract","Useless contract: No contract defined at the introduction of the method")
 	end
 
-	redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
+	redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr
 	do
-		# Creating the if expression with the new condition
-		var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype)
-		# Creating and adding return expr to the then case
-		if_block.n_then = v.ast_builder.make_return(null)
-		# Creating the super call to the contract and adding this to else case
-		if_block.n_else = v.ast_builder.make_super_call(args,null)
 		var n_block = v.ast_builder.make_block
-		n_block.add if_block
+		for n_condition in n_conditions do
+			# Creating the if expression with the new condition
+			var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype)
+			# Creating and adding return expr to the then case
+			if_block.n_then = v.ast_builder.make_return
+			if_block.location = n_condition.location
+			n_block.add if_block
+		end
+		n_block.add v.ast_builder.make_super_call(super_args)
 		return n_block
 	end
 
-	redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef)
+	redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef)
 	do
 		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true)
-		var n_self = new ASelfExpr
 		var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder)
-		var n_callexpect = v.ast_builder.make_call(n_self,callsite,args)
+		var n_callexpect = v.ast_builder.make_call(new ASelfExpr, callsite,args)
 		# Creation of the new instruction block with the call to expect condition
 		var actual_expr = n_mpropdef.n_block
 		var new_block = new ABlockExpr
-		new_block.n_expr.push n_callexpect
+		new_block.n_expr.push v.encapsulated_contract_call(n_mpropdef, [n_callexpect])
 		if actual_expr isa ABlockExpr then
 			new_block.n_expr.add_all(actual_expr.n_expr)
 		else if actual_expr != null then
 			new_block.n_expr.push(actual_expr)
 		end
 		n_mpropdef.n_block = new_block
+		mfacet.has_applied_expect = true
 	end
 end
 
 redef class BottomMContract
 
-	redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
+	redef fun is_called(v: ContractsVisitor, mpropdef: MPropDef): Bool
+	do
+		return super or v.mainmodule.mpackage == mpropdef.mclassdef.mmodule.mpackage
+	end
+
+	redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_args: Array[AExpr]): ABlockExpr
 	do
-		var tid = new TId.init_tk(v.current_location)
-		tid.text = "{contract_name}"
-		# Creating the assert expression with the new condition
-		var assert_block = v.ast_builder.make_assert(tid,n_condition,null)
-		# Creating the super call to the contract
-		var super_call = v.ast_builder.make_super_call(args,null)
 		# Define contract block
 		var n_block = v.ast_builder.make_block
-		# Adding the expressions to the block
+
+		var super_call = v.ast_builder.make_super_call(super_args)
+
 		n_block.add super_call
-		n_block.add assert_block
+		for n_condition in n_conditions do
+			var tid = new TId.init_tk(n_condition.location)
+			tid.text = "{n_condition.location.text}"
+			# Creating the assert expression with the new condition
+			var n_assert = v.ast_builder.make_assert(tid, n_condition)
+			n_assert.location = n_condition.location
+			n_block.add n_assert
+		end
 		return n_block
 	end
 
@@ -474,27 +473,20 @@ redef class BottomMContract
 	#
 	# The purpose of the variable is to capture return values to use it in contracts.
 	private fun inject_result(v: ContractsVisitor, n_mpropdef: AMethPropdef, ret_type: MType): Variable
+	is
+		expect(n_mpropdef.n_signature.n_type != null)
 	do
 		var actual_block = n_mpropdef.n_block
 		# never happen. If it's the case the problem is in the contract facet building
 		assert actual_block isa ABlockExpr
 
-		var return_var: nullable Variable = null
-
 		var return_expr = actual_block.n_expr.last.as(AReturnExpr)
 
 		var returned_expr = return_expr.n_expr
 		# The return node has no returned expression
 		assert returned_expr != null
 
-		# Check if the result variable already exit
-		if returned_expr isa AVarExpr then
-			if returned_expr.variable.name == "result" then
-				return_var = returned_expr.variable
-			end
-		end
-
-		return_var = new Variable("result")
+		var return_var = new Variable("result")
 		# Creating a new variable to keep the old return of the method
 		var assign_result = v.ast_builder.make_var_assign(return_var, returned_expr)
 		# Remove the actual return
@@ -514,9 +506,6 @@ end
 
 redef class MEnsure
 
-	# Define the name of the contract
-	redef fun contract_name: String do return "ensure"
-
 	redef fun adapt_specific_msignature(m_signature: MSignature): MSignature
 	do
 		return m_signature.adapt_to_ensurecondition
@@ -527,14 +516,12 @@ redef class MEnsure
 		return n_signature.adapt_to_ensurecondition
 	end
 
-	redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef)
+	redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef)
 	do
 		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true)
 		var n_self = new ASelfExpr
 		# argument to call the contract method
 		var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder)
-		# Inject the variable result
-		# The cast is always safe because the online adapted method is the contract facet
 
 		var actual_block = n_mpropdef.n_block
 		# never happen. If it's the case the problem is in the contract facet building
@@ -542,117 +529,118 @@ redef class MEnsure
 
 		var ret_type = n_mpropdef.mpropdef.mproperty.intro.msignature.return_mtype
 		if ret_type != null then
+			# Inject the variable result
 			var result_var = inject_result(v, n_mpropdef, ret_type)
 			# Expr to read the result variable
 			var read_result = v.ast_builder.make_var_read(result_var, ret_type)
 			var return_expr = actual_block.n_expr.pop
 			# Adding the read return to argument
 			args.add(read_result)
-			var n_callcontract = v.ast_builder.make_call(n_self,callsite,args)
-			actual_block.add_all([n_callcontract,return_expr])
+			var n_call_contract = v.ast_builder.make_call(n_self, callsite, args)
+			actual_block.add_all([v.encapsulated_contract_call(n_mpropdef, [n_call_contract]), return_expr])
 		else
 			# build the call to the contract method
-			var n_callcontract = v.ast_builder.make_call(n_self,callsite,args)
-			actual_block.add n_callcontract
+			var n_call_contract = v.ast_builder.make_call(n_self, callsite, args)
+			actual_block.add v.encapsulated_contract_call(n_mpropdef, [n_call_contract])
 		end
+		n_mpropdef.do_all(v.toolcontext)
+		mfacet.has_applied_ensure = true
 	end
 end
 
-redef class MClass
-
-	# This method create an abstract method representation with this MMethodDef an this AMethoddef
-	private fun create_abstract_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef
-	do
-		# new methoddef definition
-		var m_def = new MMethodDef(mclassdef, mproperty, v.current_location)
-		# set the signature
-		if msignature != null then m_def.msignature = msignature.clone
-		# set the abstract flag
-		m_def.is_abstract = true
-		# Build the new node method
-		var n_def = v.ast_builder.make_method(null,null,m_def,n_signature,null,null,null,null)
-		# Define the location of the new method for corresponding of the actual method
-		n_def.location = v.current_location
-		# Association new npropdef to mpropdef
-		v.toolcontext.modelbuilder.unsafe_add_mpropdef2npropdef(m_def,n_def)
-		return n_def
-	end
-
-	# Create method with an empty block
-	# the `mproperty` i.e the global property definition. The mclassdef to set where the method is declared and it's model `msignature` and ast `n_signature` signature
-	private fun create_empty_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef
-	do
-		var n_def = create_abstract_method(v, mproperty, mclassdef, msignature, n_signature)
-		n_def.mpropdef.is_abstract = false
-		n_def.n_block = v.ast_builder.make_block
-		return n_def
-	end
-end
-
-redef class MMethodDef
+redef class MMethod
 
-	# Verification of the contract facet
-	# Check if a contract facet already exists to use it again or if it is necessary to create it.
-	private fun check_contract_facet(v: ContractsVisitor, n_signature: ASignature, classdef: MClassDef, mcontract: MContract, exist_contract: Bool)
+	# Define contract facet for MMethod in the given mclassdef. The facet represents the entry point with contracts (expect, ensure) of the method.
+	# If a contract is given adapt the contract facet.
+	#
+	# `classdef`: Indicates the class where we want to introduce our facet
+	# `exist_contract`: Indicates if it is necessary to define a new facet for the contract. If `exist_contract_facet and exist_contract` it's not necessary to add a facet.
+	#
+	# Exemple:
+	# ~~~nitish
+	# from:
+	#	classe A
+	#		i :Int
+	#		fun add_one is ensure(old(i) + 1 == i)
+	#	end
+	# to:
+	#	classe A
+	#		fun add_one is ensure(old(i) + 1 == i)
+	#
+	#		# The contract facet
+	#		fun contract_add_one do
+	#			add_one
+	#			ensure_add_one(old_add_one)
+	#		end
+	#	end
+	# ~~
+	private fun define_contract_facet(v: ContractsVisitor, classdef: MClassDef, mcontract: nullable MContract)
 	do
-		var exist_contract_facet = mproperty.has_contract_facet
-		if exist_contract_facet and exist_contract then return
+		var exist_contract_facet = has_contract_facet
+		var contract_facet = build_contract_facet
+		# Do nothing the contract and the contract facet already exist
+		if mcontract != null and mcontract.is_already_applied(contract_facet) then return
 
-		var contract_facet: AMethPropdef
+		var n_contract_facet: AMethPropdef
 		if not exist_contract_facet then
 			# If has no contract facet in intro just create it
-			if classdef != mproperty.intro_mclassdef then create_contract_facet(v, mproperty.intro_mclassdef, n_signature)
-			# If has no contract facet just create it
-			contract_facet = create_contract_facet(v, classdef, n_signature)
+			if classdef != intro_mclassdef then
+				create_facet(v, intro_mclassdef, contract_facet, self)
+			end
+			n_contract_facet = create_facet(v, classdef, contract_facet, self)
 		else
 			# Check if the contract facet already exist in this context (in this classdef)
-			if classdef.mpropdefs_by_property.has_key(mproperty.mcontract_facet) then
-				# get the define
-				contract_facet = v.toolcontext.modelbuilder.mpropdef2node(classdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef)
+			if classdef.mpropdefs_by_property.has_key(contract_facet) then
+				# get the definition
+				n_contract_facet = v.toolcontext.modelbuilder.mpropdef2node(classdef.mpropdefs_by_property[contract_facet]).as(AMethPropdef)
 			else
 				# create a new contract facet definition
-				contract_facet = create_contract_facet(v, classdef, n_signature)
+				n_contract_facet = create_facet(v, classdef, contract_facet, self)
 				var block = v.ast_builder.make_block
 				# super call to the contract facet
-				var n_super_call = v.ast_builder.make_super_call(n_signature.make_parameter_read(v.ast_builder), null)
+				var args = n_contract_facet.n_signature.make_parameter_read(v.ast_builder)
+				var n_super_call = v.ast_builder.make_super_call(args)
 				# verification for add a return or not
-				if contract_facet.mpropdef.msignature.return_mtype != null then
+				if self.intro.msignature.return_mtype != null then
 					block.add(v.ast_builder.make_return(n_super_call))
 				else
 					block.add(n_super_call)
 				end
-				contract_facet.n_block = block
+				n_contract_facet.n_block = block
 			end
 		end
-		contract_facet.adapt_block_to_contract(v, mcontract, contract_facet)
-		contract_facet.location = v.current_location
-		contract_facet.do_all(v.toolcontext)
-	end
+		if mcontract != null then mcontract.adapt_method_to_contract(v, contract_facet, n_contract_facet)
 
-	# Method to create a contract facet of the method
-	private fun create_contract_facet(v: ContractsVisitor, classdef: MClassDef, n_signature: ASignature): AMethPropdef
-	do
-		var contract_facet = mproperty.build_contract_facet
-		# Defines the contract phase is an init or not
-		# it is necessary to use the contracts on constructor
-		contract_facet.is_init = self.mproperty.is_init
-
-		# check if the method has an `msignature` to copy it.
-		var m_signature: nullable MSignature = null
-		if mproperty.intro.msignature != null then m_signature = mproperty.intro.msignature.clone
+		n_contract_facet.location = v.current_location
+		n_contract_facet.do_all(v.toolcontext)
+	end
 
-		var n_contractdef = classdef.mclass.create_empty_method(v, contract_facet, classdef, m_signature, n_signature)
+	# Method to create a facet of the method.
+	# See `define_contract_facet` for more information about two types of facets.
+	#
+	# `called` : is the property to call in this facet.
+	private fun create_facet(v: ContractsVisitor, classdef: MClassDef, facet: MFacet, called: MMethod): AMethPropdef
+	is
+		expect( called.is_same_instance(self) or called.is_same_instance(self.mcontract_facet) )
+	do
+		# Defines the contract facet is an init or not
+		# it is necessary to use the contracts with in a constructor
+		facet.is_init = is_init
+		var n_contractdef = v.toolcontext.modelbuilder.create_method_from_property(facet, classdef, false, self.intro.msignature)
 		# FIXME set the location because the callsite creation need the node location
 		n_contractdef.location = v.current_location
 		n_contractdef.validate
 
 		var block = v.ast_builder.make_block
-		var n_self = new ASelfExpr
-		var args = n_contractdef.n_signature.make_parameter_read(v.ast_builder)
-		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, mproperty, true)
-		var n_call = v.ast_builder.make_call(n_self, callsite, args)
 
-		if m_signature.return_mtype == null then
+		# Arguments to call the `called` property
+		var args: Array[AExpr]
+		args = n_contractdef.n_signature.make_parameter_read(v.ast_builder)
+
+		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, called, true)
+		var n_call = v.ast_builder.make_call(new ASelfExpr, callsite, args)
+
+		if self.intro.msignature.return_mtype == null then
 			block.add(n_call)
 		else
 			block.add(v.ast_builder.make_return(n_call))
@@ -662,49 +650,48 @@ redef class MMethodDef
 		n_contractdef.do_all(v.toolcontext)
 		return n_contractdef
 	end
+end
+
+redef class MMethodDef
 
 	# Entry point to build contract (define the contract facet and define the contract method verification)
-	private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotation: AAnnotation, mcontract: MContract, exist_contract: Bool)
+	private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotations: Array[AAnnotation], mcontract: MContract, exist_contract: Bool)
 	do
-		if check_same_contract(v, n_annotation, mcontract) then return
-		if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation)
 		v.define_signature(mcontract, n_signature, mproperty.intro.msignature)
-
-		var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef)
-		check_contract_facet(v, n_signature.clone, mclassdef, mcontract, exist_contract)
-		has_contract = true
+		if not exist_contract and not is_intro then no_intro_contract(v, mcontract, n_annotations)
+		v.build_contract(n_annotations, mcontract, mclassdef)
+		# Check if the contract must be called to know if it's needed to construct the facet
+		if mcontract.is_called(v, self) then mproperty.define_contract_facet(v, mclassdef, mcontract)
 	end
 
 	# Create a contract on the introduction classdef of the property.
 	# Display an warning message if necessary
-	private fun no_intro_contract(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, n_annotation: AAnnotation)
+	private fun no_intro_contract(v: ContractsVisitor, mcontract: MContract, n_annotations: Array[AAnnotation])
 	do
-		mcontract.create_empty_contract(v, mcontract.intro_mclassdef, mcontract.adapt_msignature(self.mproperty.intro.msignature), mcontract.adapt_nsignature(n_signature))
-		mcontract.no_intro_contract(v, n_annotation)
-		mproperty.intro.has_contract = true
+		v.toolcontext.modelbuilder.create_method_from_property(mcontract, mcontract.intro_mclassdef, false, v.m_signature)
+		mcontract.no_intro_contract(v, n_annotations)
 	end
 
-	# Is the contract already defined in the context
-	#
-	# Exemple :
-	# fun foo is expect([...]), expect([...])
-	#
-	# Here `check_same_contract` display an error when the second expect is processed
-	private fun check_same_contract(v: ContractsVisitor, n_annotation: AAnnotation ,mcontract: MContract): Bool
+	# Apply the `no_contract` annotation to the contract. This method removes the inheritance by adding an empty contract method.
+	# Display a warning if the annotation is not needed
+	private fun no_contract_apply(v: ContractsVisitor, n_signature: ASignature)
 	do
-		if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then
-			v.toolcontext.error(n_annotation.location, "The method already has a defined `{mcontract.contract_name}` contract at line {self.mclassdef.mpropdefs_by_property[mcontract].location.line_start}")
-			return true
+		var mensure = mproperty.mensure
+		var mexpect = mproperty.mexpect
+		if mensure == null and mexpect == null then
+			v.toolcontext.warning(location, "useless_nocontract", "Useless `no_contract`, no contract was declared for `{name}`. Remove the `no_contract`")
+		end
+		if mensure != null then
+			# Add an empty ensure method to replace the actual definition
+			v.toolcontext.modelbuilder.create_method_from_property(mensure, mclassdef, false, mensure.intro.msignature)
+		end
+		if mexpect != null then
+			# Add an empty expect method to replace the actual definition
+			v.toolcontext.modelbuilder.create_method_from_property(mexpect, mclassdef, false, mexpect.intro.msignature)
 		end
-		return false
 	end
 end
 
-redef class MPropDef
-	# flag to indicate is the `MPropDef` has a contract
-	var has_contract = false
-end
-
 redef class APropdef
 	redef fun check_callsite(v)
 	do
@@ -718,59 +705,58 @@ redef class AMethPropdef
 	redef fun create_contracts(v)
 	do
 		v.ast_builder.check_mmodule(mpropdef.mclassdef.mmodule)
-
 		v.current_location = self.location
 		v.is_intro_contract = mpropdef.is_intro
-
-		if n_annotations != null then
-			for n_annotation in n_annotations.n_items do
-				check_annotation(v,n_annotation)
-			end
-		end
-
-		if not mpropdef.is_intro and not v.find_no_contract then
-			self.check_redef(v)
-		end
-
-		# reset the flag
-		v.find_no_contract = false
+		check_annotation(v)
+		if not mpropdef.is_intro then check_redef(v)
 	end
 
 	# Verification of the annotation to know if it is a contract annotation.
 	# If this is the case, we built the appropriate contract.
-	private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation)
+	private fun check_annotation(v: ContractsVisitor)
 	do
-		if n_annotation.name == "expect" then
-			if not v.check_usage_expect(mpropdef.mclassdef.mmodule) then return
+		var annotations_expect = get_annotations("expect")
+		var annotations_ensure = get_annotations("ensure")
+		var annotation_no_contract = get_annotations("no_contract")
+
+		if (not annotations_expect.is_empty or not annotations_ensure.is_empty) and not annotation_no_contract.is_empty then
+			v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`")
+			return
+		end
+
+		var nsignature = n_signature or else new ASignature
+
+		if not annotation_no_contract.is_empty then
+			mpropdef.no_contract_apply(v, nsignature.clone)
+			return
+		end
+
+		if not annotations_expect.is_empty then
 			var exist_contract = mpropdef.mproperty.has_expect
-			mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.build_expect, exist_contract)
-		else if n_annotation.name == "ensure" then
-			if not v.check_usage_ensure(mpropdef.mclassdef.mmodule) then return
+			mpropdef.construct_contract(v, nsignature.clone, annotations_expect, mpropdef.mproperty.build_expect, exist_contract)
+		end
+
+		if not annotations_ensure.is_empty then
 			var exist_contract = mpropdef.mproperty.has_ensure
-			mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.build_ensure, exist_contract)
-		else if n_annotation.name == "no_contract" then
-			# no_contract found set the flag to true
-			v.find_no_contract = true
+			mpropdef.construct_contract(v, nsignature.clone, annotations_ensure, mpropdef.mproperty.build_ensure, exist_contract)
 		end
 	end
 
 	# Verification if the method have an inherited contract to apply it.
 	private fun check_redef(v: ContractsVisitor)
 	do
-		# Check if the method has an attached contract
-		if not mpropdef.has_contract then
-			if mpropdef.mproperty.intro.has_contract then
-				mpropdef.has_contract = true
-			end
-		end
-	end
+		var mexpect = mpropdef.mproperty.mexpect
+		var mensure = mpropdef.mproperty.mensure
+		var mcontract_facet = mpropdef.mproperty.mcontract_facet
 
-	# Adapt the block to use the contracts
-	private fun adapt_block_to_contract(v: ContractsVisitor, contract: MContract, n_mpropdef: AMethPropdef)
-	do
-		contract.adapt_block_to_contract(v, n_mpropdef)
-		mpropdef.has_contract = true
-		n_mpropdef.do_all(v.toolcontext)
+		if mexpect != null then
+			if mcontract_facet != null and mcontract_facet.has_applied_expect then return
+			if mexpect.is_called(v, mpropdef.as(not null)) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mexpect)
+		end
+		if mensure != null then
+			if mcontract_facet != null and mcontract_facet.has_applied_ensure then return
+			if mensure.is_called(v, mpropdef.as(not null)) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mensure)
+		end
 	end
 end
 
@@ -845,7 +831,7 @@ redef class ASendExpr
 	do
 		var actual_callsite = callsite
 		if actual_callsite != null then
-			callsite = v.drive_method_contract(actual_callsite)
+			callsite = v.drive_callsite_to_contract(actual_callsite)
 		end
 	end
 end
@@ -855,7 +841,7 @@ redef class ANewExpr
 	do
 		var actual_callsite = callsite
 		if actual_callsite != null then
-			callsite = v.drive_method_contract(actual_callsite)
+			callsite = v.drive_callsite_to_contract(actual_callsite)
 		end
 	end
 end
diff --git a/tests/sav/contracts.res b/tests/sav/contracts.res
index fe6b723..c9b0553 100644
--- a/tests/sav/contracts.res
+++ b/tests/sav/contracts.res
@@ -1 +1 @@
-Runtime error: Assert 'expect' failed (contracts.nit:31)
+Runtime error: Assert 'expect(not bool)' failed (contracts.nit:31)
diff --git a/tests/sav/contracts_abstract.res b/tests/sav/contracts_abstract.res
index 5f6178c..738f3f0 100644
--- a/tests/sav/contracts_abstract.res
+++ b/tests/sav/contracts_abstract.res
@@ -1 +1 @@
-Runtime error: Assert 'ensure' failed (contracts_abstract.nit:26)
+Runtime error: Assert 'ensure(y <= 10.0, y == 42.0)' failed (contracts_abstract.nit:26)
diff --git a/tests/sav/contracts_add.res b/tests/sav/contracts_add.res
index a353fc9..6d21df2 100644
--- a/tests/sav/contracts_add.res
+++ b/tests/sav/contracts_add.res
@@ -1,2 +1,2 @@
 contracts_add.nit:46,3--16: Useless contract: No contract defined at the introduction of the method
-Runtime error: Assert 'ensure' failed (contracts_add.nit:39)
+Runtime error: Assert 'ensure(x == 0)' failed (contracts_add.nit:39)
diff --git a/tests/sav/contracts_constructor.res b/tests/sav/contracts_constructor.res
index f0801df..94dfe03 100644
--- a/tests/sav/contracts_constructor.res
+++ b/tests/sav/contracts_constructor.res
@@ -1 +1 @@
-Runtime error: Assert 'expect' failed (contracts_constructor.nit:20)
+Runtime error: Assert 'expect(test > 10)' failed (contracts_constructor.nit:20)
diff --git a/tests/sav/contracts_ensures.res b/tests/sav/contracts_ensures.res
index 5e3bffa..34f0938 100644
--- a/tests/sav/contracts_ensures.res
+++ b/tests/sav/contracts_ensures.res
@@ -1 +1 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures.nit:29)
+Runtime error: Assert 'ensure(not bool)' failed (contracts_ensures.nit:29)
diff --git a/tests/sav/contracts_ensures_1.res b/tests/sav/contracts_ensures_1.res
index c947107..698c7dc 100644
--- a/tests/sav/contracts_ensures_1.res
+++ b/tests/sav/contracts_ensures_1.res
@@ -1,3 +1,3 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures_1.nit:20)
+Runtime error: Assert 'ensure(x > 0)' failed (contracts_ensures_1.nit:20)
 Good
 Fail
diff --git a/tests/sav/contracts_ensures_2.res b/tests/sav/contracts_ensures_2.res
index 982613a..213d864 100644
--- a/tests/sav/contracts_ensures_2.res
+++ b/tests/sav/contracts_ensures_2.res
@@ -1,4 +1,4 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures_2.nit:31)
+Runtime error: Assert 'ensure(y == 1.2)' failed (contracts_ensures_2.nit:31)
 Good
 Good
 Good
diff --git a/tests/sav/contracts_ensures_3.res b/tests/sav/contracts_ensures_3.res
index 11ebcc5..06c56eb 100644
--- a/tests/sav/contracts_ensures_3.res
+++ b/tests/sav/contracts_ensures_3.res
@@ -1 +1 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures_3.nit:20)
+Runtime error: Assert 'ensure(result > 0)' failed (contracts_ensures_3.nit:20)
diff --git a/tests/sav/contracts_ensures_4.res b/tests/sav/contracts_ensures_4.res
index e602695..6c8805e 100644
--- a/tests/sav/contracts_ensures_4.res
+++ b/tests/sav/contracts_ensures_4.res
@@ -1 +1 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures_4.nit:31)
+Runtime error: Assert 'ensure(not result)' failed (contracts_ensures_4.nit:31)
diff --git a/tests/sav/contracts_ensures_sequence.res b/tests/sav/contracts_ensures_sequence.res
index 3cdcc71..b62c05a 100644
--- a/tests/sav/contracts_ensures_sequence.res
+++ b/tests/sav/contracts_ensures_sequence.res
@@ -1 +1 @@
-Runtime error: Assert 'ensure' failed (contracts_ensures_sequence.nit:18)
+Runtime error: Assert 'ensure(x > 2)' failed (contracts_ensures_sequence.nit:18)
diff --git a/tests/sav/contracts_error.res b/tests/sav/contracts_error.res
index 45e60a6..3847129 100644
--- a/tests/sav/contracts_error.res
+++ b/tests/sav/contracts_error.res
@@ -1,2 +1,2 @@
-contracts_error.nit:23,10--22: Error: expected an expression.
-contracts_error.nit:24,10--22: Error: expected an expression.
+contracts_error.nit:23,3--23: Error: expected an expression.
+contracts_error.nit:24,3--23: Error: expected an expression.
diff --git a/tests/sav/contracts_expects_1.res b/tests/sav/contracts_expects_1.res
index c265d14..555a497 100644
--- a/tests/sav/contracts_expects_1.res
+++ b/tests/sav/contracts_expects_1.res
@@ -1 +1 @@
-Runtime error: Assert 'expect' failed (contracts_expects_1.nit:20)
+Runtime error: Assert 'expect(x > 0)' failed (contracts_expects_1.nit:20)
diff --git a/tests/sav/contracts_generic_type.res b/tests/sav/contracts_generic_type.res
index 9c7f782..6d36851 100644
--- a/tests/sav/contracts_generic_type.res
+++ b/tests/sav/contracts_generic_type.res
@@ -1 +1 @@
-Runtime error: Assert 'expect' failed (contracts_generic_type.nit:33)
+Runtime error: Assert 'expect(x.length != 0)' failed (contracts_generic_type.nit:33)
diff --git a/tests/sav/contracts_inheritance.res b/tests/sav/contracts_inheritance.res
index 0abeba3..5736913 100644
--- a/tests/sav/contracts_inheritance.res
+++ b/tests/sav/contracts_inheritance.res
@@ -1,5 +1,5 @@
 contracts_inheritance.nit:58,6--9: Warning: conflicting property definitions for property `toto` in `MySubArray`: contracts_inheritance$MyArrayInt$toto contracts_inheritance$MyArrayInt2$toto
-Runtime error: Assert 'ensure' failed (contracts_inheritance.nit:32)
+Runtime error: Assert 'ensure(e == 12)' failed (contracts_inheritance.nit:32)
 toto MyArrayInt2
 toto MyArrayInt
 toto ArrayInt
diff --git a/tests/sav/contracts_same_contract.res b/tests/sav/contracts_same_contract.res
index 54afbe1..e69de29 100644
--- a/tests/sav/contracts_same_contract.res
+++ b/tests/sav/contracts_same_contract.res
@@ -1 +0,0 @@
-contracts_same_contract.nit:22,3--17: The method already has a defined `expect` contract at line 21
diff --git a/tests/sav/contracts_static.res b/tests/sav/contracts_static.res
index 95b94d6..445cb2e 100644
--- a/tests/sav/contracts_static.res
+++ b/tests/sav/contracts_static.res
@@ -1,2 +1,2 @@
-Runtime error: Assert 'ensure' failed (contracts_static.nit:29)
+Runtime error: Assert 'ensure(x > 10)' failed (contracts_static.nit:29)
 Error
diff --git a/tests/sav/contracts_virtual_type.res b/tests/sav/contracts_virtual_type.res
index 616e1d0..ada2d2b 100644
--- a/tests/sav/contracts_virtual_type.res
+++ b/tests/sav/contracts_virtual_type.res
@@ -1 +1 @@
-Runtime error: Assert 'expect' failed (contracts_virtual_type.nit:23)
+Runtime error: Assert 'expect(x == 1)' failed (contracts_virtual_type.nit:23)