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.

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: detachable ANY)
    do
    ensure
      True
    end
 
end
 
class B
 
inherit
  A
    redefine f end
 
feature
 
  f (x: detachable 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: detachable  STRING)
  ensure -- From A
    (attached 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: detachable STRING)
    do
      if attached x as y 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: attached 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.