From: Florian Deljarry Date: Wed, 9 Oct 2019 00:57:01 +0000 (-0400) Subject: contracts: change the contract syntax X-Git-Url: http://nitlanguage.org contracts: change the contract syntax Replace `ensures` by `ensure` and `expects` `expect` Signed-off-by: Florian Deljarry --- diff --git a/src/contracts.nit b/src/contracts.nit index 98d5eb2..e2bad53 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -50,7 +50,7 @@ redef class AModule # 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 @@ -134,13 +134,13 @@ private class ContractsVisitor 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. # - 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 @@ -152,12 +152,12 @@ private class ContractsVisitor 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 # - 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 @@ -207,7 +207,7 @@ 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) + # 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 @@ -313,7 +313,7 @@ class MExpect 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 @@ -323,15 +323,15 @@ class MExpect # ~~~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 # end @@ -375,7 +375,7 @@ class MExpect 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 @@ -441,7 +441,7 @@ class MEnsure 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 @@ -535,7 +535,7 @@ redef class MMethod 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 @@ -546,7 +546,7 @@ redef class MMethod 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 @@ -660,9 +660,9 @@ redef class MMethodDef # 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 @@ -724,12 +724,12 @@ redef class AMethPropdef # 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 diff --git a/src/frontend/check_annotation.nit b/src/frontend/check_annotation.nit index 41ed278..9dc9cfd 100644 --- a/src/frontend/check_annotation.nit +++ b/src/frontend/check_annotation.nit @@ -112,8 +112,8 @@ after after_all example -expects -ensures +expect +ensure no_contract """ diff --git a/tests/contracts.nit b/tests/contracts.nit index b804288..ead9257 100644 --- a/tests/contracts.nit +++ b/tests/contracts.nit @@ -18,8 +18,8 @@ class MyClass fun foo(x: Int) is - expects(x == 1) - ensures(x > 0) + expect(x == 1) + ensure(x > 0) do x = 0 end @@ -28,8 +28,8 @@ end class MyClass2 fun foo(bool: Bool) is - expects(not bool) - ensures(not bool) + expect(not bool) + ensure(not bool) do if bool then print "Error" end diff --git a/tests/contracts_abstract.nit b/tests/contracts_abstract.nit index de62490..ca54119 100644 --- a/tests/contracts_abstract.nit +++ b/tests/contracts_abstract.nit @@ -15,15 +15,15 @@ # Verification if it's possible to define a contract in different context (abstract class, interface and class) and it's possible to inherit it. class MyClass - fun foo(x: Int, y: Float)is abstract, expects(x != 10) + fun foo(x: Int, y: Float)is abstract, expect(x != 10) end abstract class AbstractClass - fun bar(x: Int, y: Float)is abstract, expects(x >= 1), ensures(y == 10.0) + fun bar(x: Int, y: Float)is abstract, expect(x >= 1), ensure(y == 10.0) end interface Interface - fun baz(x: Int, y: Float)is abstract, ensures(y <= 10.0, y == 42.0) + fun baz(x: Int, y: Float)is abstract, ensure(y <= 10.0, y == 42.0) end diff --git a/tests/contracts_add.nit b/tests/contracts_add.nit index 5ab7621..6f99c88 100644 --- a/tests/contracts_add.nit +++ b/tests/contracts_add.nit @@ -18,14 +18,14 @@ class MyClass fun foo(x: Int) is - expects(x == 1) + expect(x == 1) do x=1 end fun bar(x: Float): Bool is - ensures(result) + ensure(result) do return true end @@ -36,14 +36,14 @@ class MyClass2 redef fun foo(x: Int) is - ensures(x == 0) + ensure(x == 0) do x=0 end redef fun bar(x: Float) is - expects(x == 1) + expect(x == 1) do return true end diff --git a/tests/contracts_attributs.nit b/tests/contracts_attributs.nit index 504f0f9..dae1f23 100644 --- a/tests/contracts_attributs.nit +++ b/tests/contracts_attributs.nit @@ -20,8 +20,8 @@ class MyClass fun foo(x: Int) is - expects(bar == 10) - ensures(x > 0) + expect(bar == 10) + ensure(x > 0) do if bar != 10 then print "Error" end @@ -38,8 +38,8 @@ class MyClass2 fun foo(bool: Bool) is - expects(not self.baz) - ensures(my_class.bar == 11) + expect(not self.baz) + ensure(my_class.bar == 11) do if baz then print "Error" my_class.bar = 11 diff --git a/tests/contracts_constructor.nit b/tests/contracts_constructor.nit index 72eb9a9..7f5a165 100644 --- a/tests/contracts_constructor.nit +++ b/tests/contracts_constructor.nit @@ -17,7 +17,7 @@ class MyClass init construct(test: Int) is - expects(test > 10) + expect(test > 10) do end diff --git a/tests/contracts_ensures.nit b/tests/contracts_ensures.nit index 24a6ffc..0acf9b3 100644 --- a/tests/contracts_ensures.nit +++ b/tests/contracts_ensures.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int) is - ensures(x > 0) + ensure(x > 0) do end @@ -26,7 +26,7 @@ end class MyClass2 fun foo(bool: Bool) is - ensures(not bool) + ensure(not bool) do end diff --git a/tests/contracts_ensures_1.nit b/tests/contracts_ensures_1.nit index be6798e..2e6d02c 100644 --- a/tests/contracts_ensures_1.nit +++ b/tests/contracts_ensures_1.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int) is - ensures(x > 0) + ensure(x > 0) do print "Good" end diff --git a/tests/contracts_ensures_2.nit b/tests/contracts_ensures_2.nit index c102e33..e3828e1 100644 --- a/tests/contracts_ensures_2.nit +++ b/tests/contracts_ensures_2.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int, y: Float) is - ensures(x > 0) + ensure(x > 0) do print "Good" end @@ -28,7 +28,7 @@ class SubClass redef fun foo(x: Int, y: Float) is - ensures(y == 1.2) + ensure(y == 1.2) do print "Good" end diff --git a/tests/contracts_ensures_3.nit b/tests/contracts_ensures_3.nit index 5557ef2..bc3e8f3 100644 --- a/tests/contracts_ensures_3.nit +++ b/tests/contracts_ensures_3.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int): Int is - ensures(result > 0) + ensure(result > 0) do return x end diff --git a/tests/contracts_ensures_4.nit b/tests/contracts_ensures_4.nit index d5cd82d..974d475 100644 --- a/tests/contracts_ensures_4.nit +++ b/tests/contracts_ensures_4.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int): Bool is - ensures(x > 0, result) + ensure(x > 0, result) do return true end @@ -28,7 +28,7 @@ class MySubClass redef fun foo(x: Int) is - ensures(not result) + ensure(not result) do return super end diff --git a/tests/contracts_ensures_sequence.nit b/tests/contracts_ensures_sequence.nit index ab66e57..920ca60 100644 --- a/tests/contracts_ensures_sequence.nit +++ b/tests/contracts_ensures_sequence.nit @@ -15,7 +15,7 @@ class MyClass fun foo(x: Int, y: Float) is - ensures(x > 2) + ensure(x > 2) do end @@ -26,7 +26,7 @@ class MySubClass redef fun foo(x: Int, y: Float) is - ensures(y > 1.0) + ensure(y > 1.0) do end diff --git a/tests/contracts_error.nit b/tests/contracts_error.nit index d103f58..f836751 100644 --- a/tests/contracts_error.nit +++ b/tests/contracts_error.nit @@ -20,8 +20,8 @@ class MyClass fun foo(x: Int) is - expects(bar_no_return) - ensures(assert x == 1) + expect(bar_no_return) + ensure(assert x == 1) do x = 0 end diff --git a/tests/contracts_expects.nit b/tests/contracts_expects.nit index ec2f4d2..b80b150 100644 --- a/tests/contracts_expects.nit +++ b/tests/contracts_expects.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int) is - expects(x > 0) + expect(x > 0) do if x <= 0 then print "FAIL" end @@ -26,7 +26,7 @@ end class MyClass2 fun foo(bool: Bool) is - expects(not bool) + expect(not bool) do if bool then print "FAIL" end diff --git a/tests/contracts_expects_1.nit b/tests/contracts_expects_1.nit index eb923ab..be6897b 100644 --- a/tests/contracts_expects_1.nit +++ b/tests/contracts_expects_1.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int) is - expects(x > 0) + expect(x > 0) do if x <= 0 then print "FAIL" end diff --git a/tests/contracts_expects_2.nit b/tests/contracts_expects_2.nit index 3af9ebb..805c255 100644 --- a/tests/contracts_expects_2.nit +++ b/tests/contracts_expects_2.nit @@ -17,7 +17,7 @@ class MyClass fun foo(x: Int) is - expects(x > 0) + expect(x > 0) do if x <= 0 then print "FAIL" end @@ -28,7 +28,7 @@ class SubClass redef fun foo(x: Int) is - expects(x == 0) + expect(x == 0) do if x < 0 then print "FAIL" end diff --git a/tests/contracts_expects_3.nit b/tests/contracts_expects_3.nit index 63bf318..018ce7b 100644 --- a/tests/contracts_expects_3.nit +++ b/tests/contracts_expects_3.nit @@ -26,7 +26,7 @@ class SubClass redef fun foo(x: Int) is - expects(x == 0) + expect(x == 0) do if x != 0 then print "Good" end diff --git a/tests/contracts_generic_type.nit b/tests/contracts_generic_type.nit index 900d296..44ac0a0 100644 --- a/tests/contracts_generic_type.nit +++ b/tests/contracts_generic_type.nit @@ -18,7 +18,7 @@ class MyGenericClass[E] fun foo(x: E) is - expects(x == 1) + expect(x == 1) do if x != 1 then print "Error x != 1" end @@ -30,7 +30,7 @@ class MyGenericClass2[E] fun add_all(x: Array[Object]) is - expects(x.length != 0) + expect(x.length != 0) do real.add_all x end diff --git a/tests/contracts_inheritance.nit b/tests/contracts_inheritance.nit index 015d483..12c0694 100644 --- a/tests/contracts_inheritance.nit +++ b/tests/contracts_inheritance.nit @@ -29,7 +29,7 @@ class MyArrayInt redef fun toto(e) is - ensures(e == 12) + ensure(e == 12) do print "toto MyArrayInt" super e @@ -41,7 +41,7 @@ class MyArrayInt2 redef fun toto(e) is - ensures(e == 11) + ensure(e == 11) do print "toto MyArrayInt2" super e diff --git a/tests/contracts_same_contract.nit b/tests/contracts_same_contract.nit index a34005f..93e7f65 100644 --- a/tests/contracts_same_contract.nit +++ b/tests/contracts_same_contract.nit @@ -18,8 +18,8 @@ class MyClass fun foo(x: Int) is - expects(x == 10) - expects(x >= 10) + expect(x == 10) + expect(x >= 10) do x = 0 end diff --git a/tests/contracts_virtual_type.nit b/tests/contracts_virtual_type.nit index a765cf8..0e601c7 100644 --- a/tests/contracts_virtual_type.nit +++ b/tests/contracts_virtual_type.nit @@ -20,7 +20,7 @@ class MyClass fun foo(x: VIRTUAL) is - expects(x == 1) + expect(x == 1) do end diff --git a/tests/sav/contracts.res b/tests/sav/contracts.res index 6be0568..fe6b723 100644 --- a/tests/sav/contracts.res +++ b/tests/sav/contracts.res @@ -1 +1 @@ -Runtime error: Assert 'expects' failed (contracts.nit:31) +Runtime error: Assert 'expect' failed (contracts.nit:31) diff --git a/tests/sav/contracts_abstract.res b/tests/sav/contracts_abstract.res index b69a60e..5f6178c 100644 --- a/tests/sav/contracts_abstract.res +++ b/tests/sav/contracts_abstract.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_abstract.nit:26) +Runtime error: Assert 'ensure' failed (contracts_abstract.nit:26) diff --git a/tests/sav/contracts_add.res b/tests/sav/contracts_add.res index f74e59a..a353fc9 100644 --- a/tests/sav/contracts_add.res +++ b/tests/sav/contracts_add.res @@ -1,2 +1,2 @@ -contracts_add.nit:46,3--17: Useless contract: No contract defined at the introduction of the method -Runtime error: Assert 'ensures' failed (contracts_add.nit:39) +contracts_add.nit:46,3--16: Useless contract: No contract defined at the introduction of the method +Runtime error: Assert 'ensure' failed (contracts_add.nit:39) diff --git a/tests/sav/contracts_constructor.res b/tests/sav/contracts_constructor.res index 180b9c7..f0801df 100644 --- a/tests/sav/contracts_constructor.res +++ b/tests/sav/contracts_constructor.res @@ -1 +1 @@ -Runtime error: Assert 'expects' failed (contracts_constructor.nit:20) +Runtime error: Assert 'expect' failed (contracts_constructor.nit:20) diff --git a/tests/sav/contracts_ensures.res b/tests/sav/contracts_ensures.res index b710ec9..5e3bffa 100644 --- a/tests/sav/contracts_ensures.res +++ b/tests/sav/contracts_ensures.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures.nit:29) +Runtime error: Assert 'ensure' failed (contracts_ensures.nit:29) diff --git a/tests/sav/contracts_ensures_1.res b/tests/sav/contracts_ensures_1.res index 99f2817..c947107 100644 --- a/tests/sav/contracts_ensures_1.res +++ b/tests/sav/contracts_ensures_1.res @@ -1,3 +1,3 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_1.nit:20) +Runtime error: Assert 'ensure' failed (contracts_ensures_1.nit:20) Good Fail diff --git a/tests/sav/contracts_ensures_2.res b/tests/sav/contracts_ensures_2.res index a778c12..982613a 100644 --- a/tests/sav/contracts_ensures_2.res +++ b/tests/sav/contracts_ensures_2.res @@ -1,4 +1,4 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_2.nit:31) +Runtime error: Assert 'ensure' failed (contracts_ensures_2.nit:31) Good Good Good diff --git a/tests/sav/contracts_ensures_3.res b/tests/sav/contracts_ensures_3.res index 8bf6416..11ebcc5 100644 --- a/tests/sav/contracts_ensures_3.res +++ b/tests/sav/contracts_ensures_3.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_3.nit:20) +Runtime error: Assert 'ensure' failed (contracts_ensures_3.nit:20) diff --git a/tests/sav/contracts_ensures_4.res b/tests/sav/contracts_ensures_4.res index c0a39ad..e602695 100644 --- a/tests/sav/contracts_ensures_4.res +++ b/tests/sav/contracts_ensures_4.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_4.nit:31) +Runtime error: Assert 'ensure' failed (contracts_ensures_4.nit:31) diff --git a/tests/sav/contracts_ensures_5.res b/tests/sav/contracts_ensures_5.res index fedb42c..b99b0a1 100644 --- a/tests/sav/contracts_ensures_5.res +++ b/tests/sav/contracts_ensures_5.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_5.nit:29) +Runtime error: Assert 'ensure' failed (contracts_ensures_5.nit:29) diff --git a/tests/sav/contracts_ensures_sequence.res b/tests/sav/contracts_ensures_sequence.res index e462610..3cdcc71 100644 --- a/tests/sav/contracts_ensures_sequence.res +++ b/tests/sav/contracts_ensures_sequence.res @@ -1 +1 @@ -Runtime error: Assert 'ensures' failed (contracts_ensures_sequence.nit:18) +Runtime error: Assert 'ensure' failed (contracts_ensures_sequence.nit:18) diff --git a/tests/sav/contracts_error.res b/tests/sav/contracts_error.res index 560ce7a..45e60a6 100644 --- a/tests/sav/contracts_error.res +++ b/tests/sav/contracts_error.res @@ -1,2 +1,2 @@ -contracts_error.nit:23,11--23: Error: expected an expression. -contracts_error.nit:24,11--23: Error: expected an expression. +contracts_error.nit:23,10--22: Error: expected an expression. +contracts_error.nit:24,10--22: Error: expected an expression. diff --git a/tests/sav/contracts_expects_1.res b/tests/sav/contracts_expects_1.res index 1cfc3f6..c265d14 100644 --- a/tests/sav/contracts_expects_1.res +++ b/tests/sav/contracts_expects_1.res @@ -1 +1 @@ -Runtime error: Assert 'expects' failed (contracts_expects_1.nit:20) +Runtime error: Assert 'expect' failed (contracts_expects_1.nit:20) diff --git a/tests/sav/contracts_expects_3.res b/tests/sav/contracts_expects_3.res index 622d67c..034b500 100644 --- a/tests/sav/contracts_expects_3.res +++ b/tests/sav/contracts_expects_3.res @@ -1,3 +1,3 @@ -contracts_expects_3.nit:29,3--17: Useless contract: No contract defined at the introduction of the method +contracts_expects_3.nit:29,3--16: Useless contract: No contract defined at the introduction of the method Good Good diff --git a/tests/sav/contracts_generic_type.res b/tests/sav/contracts_generic_type.res index 656a320..9c7f782 100644 --- a/tests/sav/contracts_generic_type.res +++ b/tests/sav/contracts_generic_type.res @@ -1 +1 @@ -Runtime error: Assert 'expects' failed (contracts_generic_type.nit:33) +Runtime error: Assert 'expect' failed (contracts_generic_type.nit:33) diff --git a/tests/sav/contracts_inheritance.res b/tests/sav/contracts_inheritance.res index 65c6bf5..0abeba3 100644 --- a/tests/sav/contracts_inheritance.res +++ b/tests/sav/contracts_inheritance.res @@ -1,5 +1,5 @@ contracts_inheritance.nit:58,6--9: Warning: conflicting property definitions for property `toto` in `MySubArray`: contracts_inheritance$MyArrayInt$toto contracts_inheritance$MyArrayInt2$toto -Runtime error: Assert 'ensures' failed (contracts_inheritance.nit:32) +Runtime error: Assert 'ensure' failed (contracts_inheritance.nit:32) toto MyArrayInt2 toto MyArrayInt toto ArrayInt diff --git a/tests/sav/contracts_same_contract.res b/tests/sav/contracts_same_contract.res index cf99218..54afbe1 100644 --- a/tests/sav/contracts_same_contract.res +++ b/tests/sav/contracts_same_contract.res @@ -1 +1 @@ -contracts_same_contract.nit:22,3--18: The method already has a defined `expects` contract at line 21 +contracts_same_contract.nit:22,3--17: The method already has a defined `expect` contract at line 21 diff --git a/tests/sav/contracts_virtual_type.res b/tests/sav/contracts_virtual_type.res index 0cc6a25..616e1d0 100644 --- a/tests/sav/contracts_virtual_type.res +++ b/tests/sav/contracts_virtual_type.res @@ -1 +1 @@ -Runtime error: Assert 'expects' failed (contracts_virtual_type.nit:23) +Runtime error: Assert 'expect' failed (contracts_virtual_type.nit:23)