Difference between revisions of "Covariance through renaming"

(Syntax and pattern update)
(general syntax and pattern update)
Line 13: Line 13:
  
 
feature -- Access
 
feature -- Access
   last_food: FOOD
+
   last_food: detachable FOOD
  
 
feature -- Eating
 
feature -- Eating
   eat (f: FOOD) is
+
   eat (f: FOOD)
    require
+
      not_void: f /= Void
+
 
     do
 
     do
 
       last_food := f
 
       last_food := f
Line 24: Line 22:
 
       last_food = f
 
       last_food = f
 
     end
 
     end
 +
 
end
 
end
 
</e>
 
</e>
Line 35: Line 34:
 
feature -- Access
 
feature -- Access
 
   is_vegetarian: BOOLEAN
 
   is_vegetarian: BOOLEAN
 +
 
end
 
end
 
</e>
 
</e>
Line 51: Line 51:
  
 
feature -- Eating
 
feature -- Eating
   eat (g: GRASS) is
+
   eat (g: GRASS)
 
     do
 
     do
 
       last_food := g
 
       last_food := g
Line 64: Line 64:
 
interface class
 
interface class
 
   GRASS
 
   GRASS
 +
    redefine
 +
      is_vegetarian
 +
    end
  
 
inherit
 
inherit
 
   FOOD
 
   FOOD
  
invariant
+
feature
   grass_is_vegetarian: is_vegetarian
+
   is_vegetarian: BOOLEAN = True
 +
 
 
end
 
end
 
</e>
 
</e>
Line 78: Line 82:
 
local
 
local
 
   a_cow: COW
 
   a_cow: COW
   a_animal: ANIMAL
+
   an_animal: ANIMAL
 
do
 
do
 
   create a_cow
 
   create a_cow
 
   an_animal := a_cow
 
   an_animal := a_cow
   an_animal.eat (create {FOOD}) -- CAT call!
+
   an_animal.eat (create {FOOD}) -- CAT call
 
end
 
end
 
</e>
 
</e>
Line 107: Line 111:
  
 
feature -- Eating
 
feature -- Eating
   eat (g: GRASS) is
+
   eat (g: GRASS)
    require
+
      not_void: g /= Void
+
 
     do
 
     do
 
       last_food := g
 
       last_food := g
Line 116: Line 118:
 
     end
 
     end
  
   animal_eat (f: FOOD) is
+
   animal_eat (f: FOOD)
    local
+
      g: GRASS
+
 
     do
 
     do
       g ?= f
+
       if attached {GRASS} f as g then
      if g /= Void then
+
 
         eat (g)
 
         eat (g)
 
       else
 
       else
         raise (1,"CAT call")
+
         raise (1, "CAT call")
 
       end
 
       end
 
     end
 
     end
  
 
invariant
 
invariant
   only_eats_vegetarian: last_food.is_vegetarian
+
   only_eats_vegetarian: (attached last_food as food) implies food.is_vegetarian
 
end
 
end
 
</e>
 
</e>

Revision as of 03:53, 7 May 2013


Covariant arguments are part of the Eiffel language, introducing the known problems of CAT calls and global analysis. This page summarizes how to solve a classic covariant problem purely through the well-known and understood renaming mechanism in Eiffel. We will see that this solution is more verbose than the covariant solution, but has a set of advantages, including the explicit need to rework the contract, define handlers for CAT calls or the explicit creation of exceptions.

Example

A class ANIMAL defines a command called 'eat' with an argument 'food':

class 
  ANIMAL
 
feature -- Access
  last_food: detachable FOOD
 
feature -- Eating
  eat (f: FOOD)
    do
      last_food := f
    ensure
      last_food = f
    end
 
end

And we introduce the food class:

interface class
  FOOD
 
feature -- Access
  is_vegetarian: BOOLEAN
 
end

Now we want to model the fact that cows only eat grass, a vegetarian food.

class 
  COW
 
inherit
  ANIMAL
    redefine
      eat
    end
 
feature -- Eating
  eat (g: GRASS)
    do
      last_food := g
    end
 
invariant
  only_eats_vegetarian: last_food.is_vegetarian
end
interface class
  GRASS
    redefine
      is_vegetarian
    end
 
inherit
  FOOD
 
feature
  is_vegetarian: BOOLEAN = True
 
end

We have a potential CAT call, as we can regard a COW as an ANIMAL. An ANIMAL can be fed with any food:

local
  a_cow: COW
  an_animal: ANIMAL
do
  create a_cow
  an_animal := a_cow
  an_animal.eat (create {FOOD}) -- CAT call
end

What is the origin of the CAT call? The error comes from strengthening the precondition of eat through the type system. The precondition in ANIMAL states something like "I will eat everything, as long as it is FOOD", while the precondition in COW states: "I will eat everything, as long as it is GRASS." - so we are facing a miss-use of the inheritance relation, as a COW is not an ANIMAL - at least not when it comes to food consumption.

It is a very typical problem of object-oriented modelling, as the subtype relation not only describes a 'COW is an ANIMAL' (observation) but also a 'what we can do to an ANIMAL, we can also do to a COW' (modification) relation.

Solution 1: explicit exception

We start by clearly stating through the code when a CAT call happens. This solution does not require any further thinking and could be regarded as a flattened form of covariance (though this should be rejected, as this would take away the benefits of making exceptions explicit).

class
  COW
 
inherit
  ANIMAL
    rename
      eat as animal_eat
    redefine
      animal_eat
    end
 
feature -- Eating
  eat (g: GRASS)
    do
      last_food := g
    ensure
      last_food = f
    end
 
  animal_eat (f: FOOD)
    do
      if attached {GRASS} f as g then
        eat (g)
      else
        raise (1, "CAT call")
      end
    end
 
invariant
  only_eats_vegetarian: (attached last_food as food) implies food.is_vegetarian
end

We have renamed 'eat' to 'animal_eat', to create space for a different feature 'eat' that is adequate for cows. We implement 'animal_eat' in terms of 'eat' if the supplied food is the right one. Otherwise, we have the conditions of a CAT call and raise an exception.

The advantage of this solution is that it does clearly show that it is possible to get an exception through calling 'animal_eat' in COWs. It does not help preventing the exception from occurring, but it shows that there is a deficiency in the code that needs to be taken care of.

Solution 2: stronger precondition

The deeper insight is that ANIMAL is not a correct model of an animal. The contract is too weak: we know from reality that not every animal will eat every food. Animals are picky. We model this by a test predicate that checks if the animal will actually like our food.

class 
  ANIMAL
 
feature -- Access
  last_food: detachable FOOD
 
feature -- Status report
  likes (f: FOOD): BOOLEAN
    do
      Result := True
    end
 
feature -- Eating
  eat (f: FOOD)
    require
      likes (f)
    do
      last_food := f
    ensure
      last_food = f
    end
 
end
class 
  COW
 
inherit
  ANIMAL
    rename
      eat as animal_eat
    redefine
      animal_eat,
      likes
    end
 
feature -- Status report
  likes (f: FOOD): BOOLEAN
    do
      Result := attached {GRASS} f
    end
 
feature -- Eating
  eat (g: GRASS)
    do
      last_food := g
    ensure
      last_food = g
    end
 
  animal_eat (f: FOOD)
    do
      check attached {GRASS} f as g then
        eat (g)
      end
    end
 
invariant
  only_eats_vegetarian: (attached last_food as food) implies food .is_vegetarian
end

Discussion

From the perspective of the interface, the covariant and the renaming solutions all have the same interface, with the exception that in the renaming cases, COW also has an `animal_eat' command that it inherits from ANIMAL. Though this may seem unwanted, it makes the generation of flattened forms easier and also shows that the 'eat' of ANIMAL and 'eat' of COW are not the same features.

Also, we do not address the problems of CAT calls through genericity and change of export status. These problems need a different treatment (for example through the restriction of the interface through readonly types).

Interestingly, the approach can be used to model any change of signature, including covariant, contravariant arguments, covariant and contravariant return types and even the change of existing or the introduction of new arguments. It is thus more powerful than the covariant mechanisms available in Eiffel.