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.
