SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/inheritance

Simple examples of inheritance

Introduction

In the following the three modules "comparable", "partially_ordered" and "ordered" are used to demostrate inheritance within Modern Eiffel.

Like all object oriented languages abstract or deferred classes can be defined within Modern Eiffel.

A module with a deferred current class is deferred as well. A module "a" whose current class inherits from the current class of module "b" is called a heir of "a". Therefore it makes sense to say that module "a" inherits from module "b".

Deferred modules can have deferred routines and assertions with deferred proofs. All assertions with deferred proofs are treated within the current module as valid assumptions.

Any effective descendant of a deferred module has to effect the deferred routines and has to give valid proofs for the assertions with deferred proofs.

The module "comparable"

The module "comparable" is an abstract (or deferred) module which describes the properties of types which have a comparison function "is_equal". I.e. the module contains the declarations

  -- file: "comparable.e"
  deferred class
    COMPARABLE
  end
 
  feature
    is_equal alias "=" (a,b:CURRENT): BOOLEAN
      deferred end
  end
 
  ...
 

Remark: As opposed to previous articles we define "is_equal" explicitly with the operator alias "=". There is no reason to treat "=" differently from other operators.

The keyword "deferred" indicates that COMPARABLE is an abstract datatype. The function "is_equal" is declared as deferred as well. I.e. any module inheriting from "comparable" can provide a specification and an implementation for this function.

However there are constraints. We expect that "is_equal" is an equivalence relation, i.e. it has to be reflexive, symmetric and transitive. We state these conditions within the module "comparable".

  feature
    all(a,b,c:CURRENT) check
      reflexive: a=a
        proof deferred end
 
      symmetric: (a=b) => (b=a) 
        proof deferred end
 
      transitive: (a=b) => (b=c) => (a=c)
        proof deferred end
 
      -- remark: parentheses are not strictly necessary, because "=>" has
      --         lower precedence; they are inserted for readability
    end
  end
 

No proof is provided for these assertions. Any effective descendant of "comparable" has to provide a proof. Within the module "comparable" they are treated as valid assumptions.

We can draw some conclusions from these assumptions.

  all(a,b,c:CURRENT) check
    (a=b) = (b=a)
      proof
        premise(a=b => b=a, b=a => a=b)
        remove(2)
      end
 
    (a=b) => (b/=c) => (a/=c)
      proof
        enter_all
        contradiction(b=c)
        premise(b=a, a=c)
        premise(a=b); remove
        remove
      end
  end
 

It is sufficient to provide the proofs within the module "comparable". Every module inheriting from "comparable" inherits all its proved asssertions.

The module "partially_ordered"

Based on the module "comparable" we can define another abstract module "partially_ordered" which defines a partial order. It has the outline

  -- file: "partially_odered.e"
  deferred class
    PARTAILLY_ORDERED
  inherit
    COMPARABLE
  end
 
  feature
    is_less_equal alias "<=" (a,b:CURRENT): BOOLEAN
      deferred end
 
    is_less alias "<" (a,b:CURRENT): BOOLEAN
      deferred end
  end
 

The module "partially_ordered" does not effect the function "is_equal". It leaves it as deferred. It does not provide any proof for reflexivity, symmetry or transitivity. Since the module is not effective, it is not necessary to do this.

The module declares the two deferred functions "<=" and "<". Any descendant can effect these functions.

However the module states some constraints:

  feature
    all(a,b,c:CURRENT) check
      reflexive: a <= a   
        proof deferred end
 
      antisymmetric: (a<=b) => (b=>a) => (a=b)
        proof deferred end
 
      transitive: (a<=b) => (b<=a) => (a<=c)
        proof deferred end
 
      strict: (a<b) = (a<=b and a/=b)
        proof deferred end
    end
  end
 

Based on these assertions we can proof some consequences within the module.

  feature
    all(a,b,c:CURRENT) check
      (a<b) => (a<=b)
 
      (a<b) => (a/=b)
 
      (a<=b) => (a/=b) => (a<b)
 
      (a<=b) => (a<b or a=b)
        proof
          enter
          case_split(a=b, a/=b)
          enter; remove
          premise(a<=b,a/=b); remove(2)
        end
 
      (a<b or a=b) => (a<=b)
        proof
          enter
          case_split(a<b, a=b)
          resolve(2)
        end
 
      (a<=b) = (a<b or a=b)
 
      not (a<a)
        proof
          contradiction(a=a)
          remove(2)
        end
 
      (a<=b) => (b=c) => (a<=c)
        proof
          enter_all
          premise(a<=b, b<=c)
          remove(2)
        end
 
      (a=b) => (b<=c) => (a<=c)
        proof
         enter_all
         premise(a<=b, b<=c)
         remove(2)
        end
 
      (a<=b) => (b<c) => (a<c)
        proof
          enter_all
          premise(a<=c, a/=c)
          resolve
          contradiction(b=c)
          premise(b<=c, c<=a)
          remove
          premise(c=a, a<=b)
          resolve(2)
        end
 
      (a<b) => (b<c) => (a<c)
    end
  end
 

These are already a lot of useful laws which any descendant inherits for free. Note that an assertion without explicit proof is proved by the implicit sequence "proof resolve end".

The module "ordered"

The module "ordered" inherits the module "partially_ordered" and gives one more constraint which is necesary for a total order.

  -- file: ordered.e
  deferred class
    ORDERED
  inherit
    PARTIALLY_ORDERED
  end
 
  feature
    all(a,b:CURRENT) check
      total: a<=b or b<=a
        proof deferred end
    end
  end
 

The assertion "total" can be used to prove the "reflexivity" assertion inherited from the module "partially_ordered".

  all(a:CURRENT) check
    a<=a
      proof
        case_split(a<=a, a<=a)
        resolve(2)
      end
  end
 

With this the proof of "reflexivity" is no longer deferred. We have an effective proof now. I.e. modules inheriting from "ordered" only have to provide a proof for "antisymmetric", "transitive", "strict" and "total". All the assertions which have already a proof based on these deferred assertions are then valid in the descendent module.

Emacs suffix

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- Introduction

- The module "comparable"

- The module "partially_ordered"

- The module "ordered"

- Emacs suffix


ip-location