src/model/model_contract.nit

   1 # This file is part of NIT ( http://www.nitlanguage.org ).
   2 #
   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
   6 #
   7 #     http://www.apache.org/licenses/LICENSE-2.0
   8 #
   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.
  14
  15 # The abstract concept of a contract in the model
  16 module model_contract
  17
  18 import model
  19 import scope
  20
  21 # The root of all contracts
  22 abstract class MContract
  23         super MMethod
  24
  25         # Is the contract is it already applied on the given `mfacet`
  26         fun is_already_applied(mfacet: MFacet): Bool is abstract
  27 end
  28
  29 # An expect (precondition) contract representation
  30 class MExpect
  31         super MContract
  32
  33         redef fun is_already_applied(mfacet: MFacet): Bool do return mfacet.has_applied_expect
  34 end
  35
  36 # The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
  37 abstract class BottomMContract
  38         super MContract
  39 end
  40
  41 # A ensure (postcondition) representation
  42 class MEnsure
  43         super BottomMContract
  44
  45         redef fun is_already_applied(mfacet: MFacet): Bool do return mfacet.has_applied_ensure
  46 end
  47
  48 # A facet contract representation
  49 # This class is created to keep the information of which method is a contract facet
  50 class MFacet
  51         super MMethod
  52
  53         # Is there an `expect` contract applied?
  54         var has_applied_expect: Bool = false
  55
  56         # Is there an `ensure` contract applied?
  57         var has_applied_ensure: Bool = false
  58 end
  59
  60 redef class MMethod
  61
  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
  66
  67         # The `MExpect` contract if any
  68         var mexpect: nullable MExpect = null
  69
  70         # The `MEnsure` contract if any
  71         var mensure: nullable MEnsure = null
  72
  73         # Build `mensure` if is not exist and return it
  74         private fun build_ensure: MEnsure
  75         do
  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
  80                 return m_mensure
  81         end
  82
  83         # Is there an ensure contract?
  84         fun has_ensure: Bool
  85         do
  86                 return self.mensure != null
  87         end
  88
  89         # Build `mexpect` if is not exist and return it
  90         private fun build_expect: MExpect
  91         do
  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
  96                 return m_mexpect
  97         end
  98
  99         # Is there an expect contract?
 100         fun has_expect: Bool
 101         do
 102                 return self.mexpect != null
 103         end
 104
 105         # Build `mcontract_facet` if is not exist and return it
 106         private fun build_contract_facet: MFacet
 107         do
 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
 113         end
 114
 115         # Is there an contract facet?
 116         fun has_contract_facet: Bool
 117         do
 118                 return self.mcontract_facet != null
 119         end
 120 end