1 # This file is part of NIT ( http://www.nitlanguage.org ).
3 # Licensed under the Apache License, Version 2.0 (the "License");
4 # you may not use this file except in compliance with the License.
5 # You may obtain a copy of the License at
7 # http://www.apache.org/licenses/LICENSE-2.0
9 # Unless required by applicable law or agreed to in writing, software
10 # distributed under the License is distributed on an "AS IS" BASIS,
11 # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12 # See the License for the specific language governing permissions and
13 # limitations under the License.
15 # The abstract concept of a contract in the model
21 # The root of all contracts
22 abstract class MContract
25 # Is the contract is it already applied on the given `mfacet`
26 fun is_already_applied
(mfacet
: MFacet): Bool is abstract
29 # An expect (precondition) contract representation
33 redef fun is_already_applied
(mfacet
: MFacet): Bool do return mfacet
.has_applied_expect
36 # The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
37 abstract class BottomMContract
41 # A ensure (postcondition) representation
45 redef fun is_already_applied
(mfacet
: MFacet): Bool do return mfacet
.has_applied_ensure
48 # A facet contract representation
49 # This class is created to keep the information of which method is a contract facet
53 # Is there an `expect` contract applied?
54 var has_applied_expect
: Bool = false
56 # Is there an `ensure` contract applied?
57 var has_applied_ensure
: Bool = false
62 # The contract facet of the method
63 # is representing the method with a contract
64 # This method calls contracts (expect, ensure) and the method
65 var mcontract_facet
: nullable MFacet = null
67 # The `MExpect` contract if any
68 var mexpect
: nullable MExpect = null
70 # The `MEnsure` contract if any
71 var mensure
: nullable MEnsure = null
73 # Build `mensure` if is not exist and return it
74 private fun build_ensure
: MEnsure
76 var m_mensure
= self.mensure
77 # build a new `MEnsure` contract
78 if m_mensure
== null then m_mensure
= new MEnsure(intro_mclassdef
, "_ensure_{name}", intro_mclassdef
.location
, public_visibility
)
79 self.mensure
= m_mensure
83 # Is there an ensure contract?
86 return self.mensure
!= null
89 # Build `mexpect` if is not exist and return it
90 private fun build_expect
: MExpect
92 var m_mexpect
= self.mexpect
93 # build a new `MExpect` contract
94 if m_mexpect
== null then m_mexpect
= new MExpect(intro_mclassdef
, "_expect_{name}", intro_mclassdef
.location
, public_visibility
)
95 self.mexpect
= m_mexpect
99 # Is there an expect contract?
102 return self.mexpect
!= null
105 # Build `mcontract_facet` if is not exist and return it
106 private fun build_contract_facet
: MFacet
108 var m_mcontract_facet
= self.mcontract_facet
109 # build a new `MFacet` contract
110 if m_mcontract_facet
== null then m_mcontract_facet
= new MFacet(intro_mclassdef
, "_contract_{name}", intro_mclassdef
.location
, public_visibility
)
111 self.mcontract_facet
= m_mcontract_facet
112 return m_mcontract_facet
115 # Is there an contract facet?
116 fun has_contract_facet
: Bool
118 return self.mcontract_facet
!= null