# 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 “odered”

The module “ordered” inherits the module “partially_ordered” and gives one

more constraint which is necesary for a total order.

-- file: ordered.e 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 descendant module.