Difference between revisions of "Covariance-aware assertions"
(→Possible solutions) |
(→Unsatisfiable postcondition on catcalls) |
||
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 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). | ||
− | + | 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: | |
+ | |||
+ | * Normal assertion: <e>True</e> | ||
+ | * Covariant-aware assertion: <e>({y: STRING} x) implies (True)</e> | ||
== Possible solutions == | == Possible solutions == |
Revision as of 07:19, 23 April 2007
ECMA Eiffel introduces covariance-aware assertions (section 8.10.4)). This is a change in assertions when covariant redefinition of feature argument occurs.
Contents
Why do we need this?
When covariant argument redefinition occurs, some assertions may be invalidated through the change of an attached to a detached type. For example an assertion x.is_empty
is not valid anymore after x is covariantly redefined since it is of a detachable type and could be Void.
Todo: Add other examples
Problems with the mechanism
Let's look at an example:
class A feature f (x: ? ANY) do ensure True end end class B inherit A redefine f end feature f (x: ? STRING) do end end
Since the feature is covariantly redefined, the postcondition will go through the process described in section 8.10.4. The consequences are that each assertion will be changed to check for potential catcalls in the following way:
- Normal assertion:
True
- Covariant-aware assertion:
({y: STRING} x) and then (True)
So the full interface of the inherited feature is:
f (x: ? STRING) ensure -- From A ({y: STRING} x) and then (True)
Note: The postcondition True
could be replaced by any other postcondition. This just illustrates that the problem occurs on any feature since all features have an implicit postcondition True.
Unsatisfiable postcondition on Void arguments
Now consider the following code block:
local a: A b: B do a := b a.f (Void) end
The caller of feature f in class A makes a valid call by passing Void as an argument. But the postcondition of the redefined feature f in class B will evaulate to false since the object test on the argument will evaluate to false.
In general, every covariance-aware assertion on an argument where Void would have been allowed (namely detached arguments) will invalidate the postcondition for a Void argument.
The problem is that the object test which actually should check for invalid arguments through cat calls will fail for Void even if it would be legal as an argument. Thus the covariance-aware assertion rule has to be changed to take Void into account if the argument which gets covariantly redefined is not an attached type and allows Void values.
For this the rule should make an object test for arguments which get redefined covariantly, but additionally allow Void values for detachable argument types. Thus the covariance-aware assertion has to look like:
- Normal assertion:
True
- Covariant-aware assertion:
({y: STRING} x or x = Void) and then (True)
Unsatisfiable postcondition on catcalls
Consider a second example where the argument type is attached in the parent feature:
class A feature g (x: ANY) do ensure True end end class B inherit A feature g (x: ? STRING) do if {y: STRING} x then -- Do something with y else -- We had a catcall or a Void argument. -- There is nothing to do here since -- the inherited postcondition is 'True' end end end
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:
- Normal assertion:
True
- Covariant-aware assertion:
({y: STRING} x) and then (True)
Now consider the following code block with a catcall:
local a: A b: B do a := b a.g (5) b.g (Void) end
The covariance-aware postcondition again evaluates to False
, 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 Void
is passed legally, the postcondition is violated (as described in the previous section).
This problem can be solved by changing the and then
which is used to combine the object test and the original assertion with an implies
clause. That way, if wrong arguments are passed the assertion will evaluate to True
no matter what and won't affect the contract anymore. The new assertion would look like this:
- Normal assertion:
True
- Covariant-aware assertion:
({y: STRING} x) implies (True)
Possible solutions
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 can be changed to use an implies
rather than and and then
clause to combine the object test with the original assertion.
Catcalls in general
Todo: This part probably should get it's own page
The question remains what the system is supposed to do in a catcall at all:
- 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 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.