- # The contract facet of the method
- # it's representing the method with contract
- # This method call the contract and the method
- var mcontract_facet: nullable MMethod = null
-
- # The expected contract method
- var mexpect: nullable MExpect = null
-
- # The ensure contract method
- var mensure: nullable MEnsure = null
-
- # Check if the MMethod has no ensure contract
- # if this is the case returns false and built it
- # else return true
- private fun check_exist_ensure: Bool
- do
- if self.mensure != null then return true
- # build a new `MEnsure` contract
- self.mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-
- # Check if the MMethod has no expect contract
- # if this is the case returns false and built it
- # else return true
- private fun check_exist_expect: Bool
- do
- if self.mexpect != null then return true
- # build a new `MExpect` contract
- self.mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-
- # Check if the MMethod has an contract facet
- # If the method has no contract facet she create it
- private fun check_exist_contract_facet(mpropdef : MMethodDef): Bool
- do
- if self.mcontract_facet != null then return true
- # build a new `MMethod` contract
- self.mcontract_facet = new MMethod(intro_mclassdef, "_contract_{name}", intro_mclassdef.location, public_visibility)
- return false
- end
-end
-
-redef class MMethodDef
-
- # 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)
- do
- var exist_contract_facet = mproperty.check_exist_contract_facet(self)
- if exist_contract_facet and exist_contract then return
-
- var contract_facet: AMethPropdef
+ # 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 = 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 n_contract_facet: AMethPropdef