+
+ # Verification if the construction of the contract is necessary.
+ # Three cases are checked for `expects`:
+ #
+ # - 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.
+ #
+ fun check_usage_expects(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 `ensures`:
+ #
+ # - Is the `--full-contract` option it's use?
+ # - Is the method is in the main package
+ #
+ fun check_usage_ensures(actual_mmodule: MModule): Bool
+ do
+ return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
+ end
+