Covariance-aware assertions - Revision history

Conaclos: syntax updated

2013-05-20T10:41:55Z

syntax updated

2007-05-30T18:40:53Z

Added category

2007-04-23T15:19:55Z

‎Unsatisfiable postcondition on catcalls

2007-04-23T15:15:45Z

‎Possible solutions

2007-04-23T08:46:56Z

‎Unsatisfiable postcondition on catcalls

2007-04-23T08:45:21Z

‎Unsatisfiable postcondition on catcalls

2007-04-23T01:21:12Z

‎Catcalls in general

2007-04-23T01:20:41Z

‎Catcalls in general

2007-04-23T01:19:06Z

‎Possible solutions

2007-04-22T19:04:21Z

‎Unsatisfiable postcondition on catcalls

@@ Line 17: / Line 17: @@
 feature
-   f (x: ? ANY)
+   f (x: detachable ANY)
      do
      ensure
@@ Line 33: / Line 33: @@
 feature
-   f (x: ? STRING)
+   f (x: detachable STRING)
      do
      end
@@ Line 48: / Line 48: @@
 <e>
-f (x: ? STRING)
+f (x: detachable  STRING)
    ensure -- From A
-     ({y: STRING} x) and then (True)
+     (attached x and then (True)
 </e>
@@ Line 106: / Line 106: @@
 feature
-   g (x: ? STRING)
+   g (x: detachable STRING)
      do
-       if {y: STRING} x then
+       if attached x as y then
          -- Do something with y
        else
@@ Line 145: / Line 145: @@
 * Normal assertion: <e>True</e>
-* Covariant-aware assertion: <e>({y: STRING} x) implies (True)</e>
+* Covariant-aware assertion: <e>attached x implies (True)</e>
 == Possible solutions ==

← Older revision		Revision as of 18:40, 30 May 2007
Line 1:		Line 1:
		+	[[Category:ECMA]]
	ECMA Eiffel introduces covariance-aware assertions (section 8.10.4)). This is a change in assertions when covariant redefinition of feature argument occurs.		ECMA Eiffel introduces covariance-aware assertions (section 8.10.4)). This is a change in assertions when covariant redefinition of feature argument occurs.

@@ Line 141: / Line 141: @@
 The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).
-The question here is, if we want to allow catcalls at all. Should they go through then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.
+This problem can be solved by changing the <e>and then</e> which is used to combine the object test and the original assertion with an <e>implies</e> clause. That way, if wrong arguments are passed the assertion will evaluate to <e>True</e> no matter what and won't affect the contract anymore. The new assertion would look like this:
 == Possible solutions ==

@@ Line 147: / Line 147: @@
 To solve the first problem shown - when a valid Void argument is passed the covariance-aware assertion fails - the rules to create covariance-aware assertions have to be changed to take detachable arguments into account and allow the valid use of Void arguments.
-To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules also have to be changed ...
+To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules can be changed to use an <e>implies</e> rather than and <e>and then</e> clause to combine the object test with the original assertion.
-{{Todo|changed to what?}}
 == Catcalls in general ==

@@ Line 141: / Line 141: @@
 The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).
-The question here is, if we want to allow catcalls at all. Should they go trough then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.
+The question here is, if we want to allow catcalls at all. Should they go through then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.
 == Possible solutions ==

@@ Line 119: / Line 119: @@
 </e>
-The argument get's detached, and any meaningful code in the redefined feature has to check for the type of the argument.
+The argument gets detached, and any meaningful code in the redefined feature has to check for the type of the argument.
 But again, the inherited assertion goes through the process to become covariance-aware:

@@ Line 157: / Line 157: @@
 * If catcalls have to be detected statically, the whole mechanism of redefining detachable is not necessary anyway and covariance-aware assertions have to be revised.
 * If catcalls should be handled dynamically, there are two ways to do so:
-** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call]] for an argument against this). Problems are raised with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.
+** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call]] for an argument against this). Problems arise with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.
 ** The program raises an exception on a catcall. If an exception should be raised, this better be the case on the entry to the call and not in the postcondition. So a runtime check could be introduced on any problematic feature call and raise an exception. This would also imply that the mechanism of redefining covariant features detachable is not necessary anymore since the runtime guarantees that all arguments are valid.