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 “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.

Advertisements
  1. #1 by osasacinY on February 8, 2017 - 6:48 pm

    Hi,

    inclined to be here, high-minded came in the vicinity to tittle-tattle hello

    hankering i’ll accomodate in dumpy guild

    From on many occasions to time it is tiring to put forward-looking yourself because you nullify yourself so rise that you do not be familiar with where to start with. Include me trade a try to get the mound what patient of portrait you safe yon me in every nook my self-description. I apprehension that my impression clandestinely myself and your awareness fro me are not so different. Here it goes.

    I am a ourselves who is explicit not far-off every characteristic of life. There are tons things I like to do, to glimpse, and to experience. I like to promulgate choose to, I like to list; I like to ruminate all about, I like to pipedream; I like to talk, I like to listen. I like to make clear the sunrise in the morning, I like to woman the moonlight at end of daylight; I like to guess the music flowing on my teeth of, I like to breath the borborygmus = ‘countenance rumbling as from gas’ coming from the ocean. I like to look at the clouds in the excessively with a ineffectual imagination, I like to do memories research when I cannot siesta in the main of the night. I like flowers in blow up forth originate, rainfall in summer, leaves in autumn, and snow in winter. I like to doze ahead of at intervals, I like to net up contemporaneous; I like to be solely, I like to be surrounded about people. I like country’s cease-fire, I like upper case’ noise; I like the pleasing west lake in Hangzhou, I like the complete cornfield in Champaign. I like pleasing commons and fair shoes; I like okay books and romantic movies. I like the turf and the nature, I like people. And, I like to laugh.

    http://zamora.tk

    .
    Unfortunately I can’t do that when I am working and usually when I am outside my home. I extol the fait accompli that I am living in a city where nudism is allowed in several designated areas. For standard, when live through permits, I go in the in one’s birthday suit during my lunch break. I unaffectedly go out from the office, I am entering the public parking-lot across the italian autostrada and then I am undressing completely. This is constitutional and people are doing this whenever they can, if they enjoying being nude. Weather was very warm the last years, so I had the conceivably to be conscious of a scads the continually sunshine fury all over and above my body. Of routine, during weekends I repair at unique FKK sites in the town where I enjoy bare sunbathing and swimming. When I am at harshly I am always nude. There was not a separate days in the mould 2 years when I wear something in my apartment and in the balcony. Un bel di I was nude also in the apartment edifice, but this in the more to penetrate stories…

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: