View source for Covariance-aware assertions

You do not have permission to edit this page, for the following reasons:
The action you have requested is limited to users in one of the groups: Autoconfirmed users, emailconfirmed, editors.
You must confirm your email address before editing pages. Please set and validate your email address through your user preferences.
You can view and copy the source of this page:
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 <e>x.is_empty</e> 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:

<e>
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
</e>

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: <e>True</e>
* Covariant-aware assertion: <e>({y: STRING} x) and then (True)</e>

So the full interface of the inherited feature is:

<e>
f (x: ? STRING)
  ensure -- From A
    ({y: STRING} x) and then (True)
</e>

{{Note|The postcondition <e>True</e> 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:

<e>
local
  a: A
  b: B
do
  a := b
  a.f (Void)
end
</e>

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: <e>True</e>
* Covariant-aware assertion: <e>({y: STRING} x or x = Void) and then (True)</e>


=== Unsatisfiable postcondition on catcalls ===

Consider a second example where the argument type is attached in the parent feature:

<e>
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
</e>

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: <e>True</e>
* Covariant-aware assertion: <e>({y: STRING} x) and then (True)</e>

Now consider the following code block with a catcall:

<e>
local
  a: A
  b: B
do
  a := b
  a.g (5)
  b.g (Void)
end
</e>

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.

== 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 [[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.
Templates used on this page:
Return to Covariance-aware assertions.
Retrieved from "https://dev.eiffel.com/Covariance-aware_assertions"
View source for Covariance-aware assertions

Navigation

Development

Wiki

Search

Tools
