Covariance-aware assertions
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 get's 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).
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.
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 also have to be changed ... (Todo: changed to what?)
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 this page 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 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.