# The implementation of the contracts is done in two visits.
#
# - First step, the visitor analyzes and constructs the contracts
- # for each class (invariant) and method (expects, ensures).
+ # for each class (invariant) and method (expect, ensure).
#
# - Second step the visitor analyzes each `ASendExpr` to see
# if the callsite calls a method with a contract. If this is
end
end
-# This visitor checks the `AMethPropdef` and the `AClassDef` to check if they have a contract annotation or it's a redefinition with a inheritance contract
+# Visitor to build all contracts.
private class ContractsVisitor
super Visitor
+ # Instance of the toolcontext
var toolcontext: ToolContext
# The main module
var current_location: Location is noinit
# Is the contrat is an introduction or not?
+ # This attribute has the same value as the `is_intro` of the propdef attached to the contract.
+ # Note : For MClassDef `is_intro_contract == false`. This is due to the fact that a method for checking invariants is systematically added to the root object class.
var is_intro_contract: Bool is noinit
# Actual visited class
end
# Verification if the construction of the contract is necessary.
- # Three cases are checked for `expects`:
+ # Three cases are checked for `expect`:
#
- # - Is the `--full-contract` option it's use?
- # - Is the method is in the main package
- # - Is the method is in a direct imported package.
+ # - 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_expects(actual_mmodule: MModule): Bool
+ fun check_usage_expect(actual_mmodule: MModule): Bool
do
var main_package = mainmodule.mpackage
var actual_package = actual_mmodule.mpackage
end
# Verification if the construction of the contract is necessary.
- # Two cases are checked for `ensures`:
+ # Two cases are checked for `ensure`:
#
- # - Is the `--full-contract` option it's use?
- # - Is the method is in the main package
+ # - Was the `--full-contract` option passed?
+ # - Is the method is in the main package?
#
- fun check_usage_ensures(actual_mmodule: MModule): Bool
+ fun check_usage_ensure(actual_mmodule: MModule): Bool
do
return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
end
private class CallSiteVisitor
super Visitor
+
+ # Instance of the toolcontext
var toolcontext: ToolContext
# Actual visited method
redef class AAnnotation
- # Returns the conditions of annotation parameters in the form of and expr
- # exemple:
- # the contract ensures(true, i == 10, f >= 1.0)
- # return this condition (true and i == 10 and f >= 1.0)
+ # Returns the conditions of annotation parameters. If there are several parameters, the result is an `AAndExpr`
+ # Example:
+ # the contract `ensure(true, i == 10, f >= 1.0)`
+ # return this condition `(true and i == 10 and f >= 1.0)`
private fun construct_condition(v : ContractsVisitor): AExpr
do
var n_condition = n_args.first
private fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) is abstract
# Adapt the msignature specifically for the contract method
- private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_condition
+ private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_contract
# Adapt the nsignature specifically for the contract method
- private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_condition(null)
+ 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
# Create the initial contract (intro)
# All contracts have the same implementation for the introduction.
#
+ # Example:
+ # ~~~nitish
# fun contrat([...])
# do
# assert contract_condition
# end
+ # ~~~
#
private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
do
super MContract
# Define the name of the contract
- redef fun contract_name: String do return "expects"
+ redef fun contract_name: String do return "expect"
# Display warning if no contract is defined at introduction `expect`,
# because if no contract is defined at the introduction the added
# contracts will not cause any error even if they are not satisfied.
#
- # exemple
+ # Example:
# ~~~nitish
# class A
# fun bar [...]
- # fun _bar_expects([...])
+ # fun _bar_expect([...])
# do
# [empty contract]
# end
# end
#
# redef class A
- # redef fun bar is expects(contract_condition)
- # redef fun _bar_expects([...])
+ # redef fun bar is expect(contract_condition)
+ # redef fun _bar_expect([...])
# do
- # if not (contract_condition) then super
+ # if (contract_condition) then return
+ # super
# end
# end
# ~~~~
end
end
-# The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`).
+# The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
abstract class BottomMContract
super MContract
return n_block
end
- # Inject the result variable in the `n_block` of the given `n_mpropdef`.
+ # Inject the `result` variable into the `n_block` of the given n_mpropdef`.
+ #
+ # 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
do
var actual_block = n_mpropdef.n_block
super BottomMContract
# Define the name of the contract
- redef fun contract_name: String do return "ensures"
+ redef fun contract_name: String do return "ensure"
redef fun adapt_specific_msignature(m_signature: MSignature): MSignature
do
do
if self.mensure != null then return true
# build a new `MEnsure` contract
- self.mensure = new MEnsure(intro_mclassdef, "_ensures_{name}", intro_mclassdef.location, public_visibility)
+ self.mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility)
return false
end
do
if self.mexpect != null then return true
# build a new `MExpect` contract
- self.mexpect = new MExpect(intro_mclassdef, "_expects_{name}", intro_mclassdef.location, public_visibility)
+ self.mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility)
return false
end
# Is the contract already defined in the context
#
# Exemple :
- # fun foo is expects([...]), expects([...])
+ # fun foo is expect([...]), expect([...])
#
- # Here `check_same_contract` display an error when the second expects is processed
+ # 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
do
if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then
# If this is the case, we built the appropriate contract.
private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation)
do
- if n_annotation.name == "expects" then
- if not v.check_usage_expects(mpropdef.mclassdef.mmodule) then return
+ if n_annotation.name == "expect" then
+ if not v.check_usage_expect(mpropdef.mclassdef.mmodule) then return
var exist_contract = mpropdef.mproperty.check_exist_expect
mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mexpect.as(not null), exist_contract)
- else if n_annotation.name == "ensures" then
- if not v.check_usage_ensures(mpropdef.mclassdef.mmodule) then return
+ else if n_annotation.name == "ensure" then
+ if not v.check_usage_ensure(mpropdef.mclassdef.mmodule) then return
var exist_contract = mpropdef.mproperty.check_exist_ensure
mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mensure.as(not null), exist_contract)
else if n_annotation.name == "no_contract" then
redef class MSignature
- # Adapt signature for a expect condition
- # Removed the return type is it not necessary
- private fun adapt_to_condition: MSignature do return new MSignature(mparameters.to_a, null)
+ # Adapt signature for an contract
+ #
+ # The returned `MSignature` is the copy of `self` without return type.
+ private fun adapt_to_contract: MSignature do return new MSignature(mparameters.to_a, null)
- # Adapt signature for a ensure condition
+ # Adapt signature for a ensure contract
#
- # Create new parameter with the return type
+ # The returned `MSignature` is the copy of `self` without return type.
+ # The return type is replaced by a new parameter `result`
private fun adapt_to_ensurecondition: MSignature
do
var rtype = return_mtype
- var msignature = adapt_to_condition
+ var msignature = adapt_to_contract
if rtype != null then
msignature.mparameters.add(new MParameter("result", rtype, false))
end
return msignature
end
- # Adapt signature for a expect condition
- # Removed the return type is it not necessary
+ # The returned `MSignature` is the exact copy of `self`.
private fun clone: MSignature do return new MSignature(mparameters.to_a, return_mtype)
end
return args
end
- # Return a copy of self adapted for the expect condition
- # npropdef it is use to define the parent of the parameters
- private fun adapt_to_condition(return_type: nullable AType): ASignature
+ # Create a new ASignature adapted for contract
+ #
+ # The returned `ASignature` is the copy of `self` without return type.
+ private fun adapt_to_contract: ASignature
do
var adapt_nsignature = self.clone
- adapt_nsignature.n_type = return_type
+ if adapt_nsignature.n_type != null then adapt_nsignature.n_type.detach
return adapt_nsignature
end
- # Return a copy of self adapted for postcondition on npropdef
+ # Create a new ASignature adapted for ensure
+ #
+ # The returned `ASignature` is the copy of `self` without return type.
+ # The return type is replaced by a new parameter `result`
private fun adapt_to_ensurecondition: ASignature do
- var nsignature = adapt_to_condition(null)
+ var nsignature = adapt_to_contract
if ret_type != null then
- var n_id = new TId
- n_id.text = "result"
- var new_param = new AParam
- new_param.n_id = n_id
- new_param.variable = new Variable(n_id.text)
- new_param.variable.declared_type = ret_type
- nsignature.n_params.add new_param
+ var variable = new Variable("result")
+ variable.declared_type = ret_type
+ nsignature.n_params.add new AParam.make(variable, ret_type.create_ast_representation)
end
return nsignature
end
nitlanguage / nit.git / blobdiff