Abstraction wins: An approach to framing and mutability

Basics

Modern Eiffel has immutable and mutable types. An object of immutable type
cannot be modified, an object of mutable type can be modified. Therefore we
say that an object is mutable or immutable depending on its type.

Immutable objects don’t have an own identity. The identity of an immutable
object is completely determined by its value. Immutable objects are therefore
sometimes called value objects and the corresponding types are called value
types. All mathematical objects like numbers, lists, sets are immutable. We
can assign to a variable a different immutable object, but we cannot modify
the object.

I.e. immutable objects are like numbers. The number “5″ is the number “5″ and
remains forever the number “5″. We can assign the number “5″ to a variable by
“i:=5″. The we can double the content of the variable “i” by the statement
“i:=2*i”. Now the value of the variable is the number “10″. But the assignment
did not change the number “5″.

Real life objects have identity. Your car is your car and your neighbours car
is a different car. The car factory puts a serial number into the chasis to
identify the car. The motor of your car has an identity with its own serial
number. You can put another motor in your car. This does not change the
identity of your car. Your car just got a new motor which is different from
the previous motor. I.e. cars are mutable, you can modify them.

A programming language which wants to be able to model real life objects must
have have mutable objects with identity. Therefore in Modern Eiffel we make
the distinction between immutable and mutable types.

Equality and identity

Since immutable type objects do not have an own identity all immutable type
objects must have an equality relation “=”. The language rules enforce that
“=” must be defined in a way that equality implies identity. I.e. if two
expressions “e1″ and “e2″ return equal objects we can always substitute the
subexpression “e1″ by “e2″ and vice versa in all expressions. This property
is called “referential transparency” sometimes expressed as “substitute equals
for equals”.

This is not true for mutable type objects. For mutable type objects “equality”
does not guarantee “identity”. Two expressions “e1″ and “e2″ of mutable
type might return equal objects. But this is not sufficient to conclude that
both objects are identical. I.e. we cannot substitute the subexpression “e1″
by “e2″ within an expression by knowing only that both objects are equal. The
substitution is allowed only if the expression “e1″ and “e2″ guarantee that
they return the same object.

In order to distinguish equality and identity we have two operators.

  =       -- Equality: reflexive, symmetric and transitive relation

  ~       -- Identity: reflexive, symmetric and transitive relation

The language rules guarantee the following properties:

  all[G](a,b,c:G)
    note built_in ensure
      reflexive:  a~a
      symmetric:  (a~b) => (b~a)
      transitive: (a~b) => (b~c) => (a~c)

      functions:  all[H](f:G->H)  
                      f.is_defined(a) => (a~b) => (f[a]~f[b])
    end

  all[G:COMPARABLE](a,b:G)
    note built_in ensure
      identity:   (a~b) => (a=b)
    end

  all[immutable G](a,b:G)
    note built_in ensure
      no_identity: (a=b) => (a~b)
    end  

In order to enforce these properties Modern Eiffel imposes the following
restrictions on the definition of types.

- For immutable types equality must be defined in a way that “no_identity” is
guaranteed. I.e. equality must use all visible attributes of a type to
defined equality. For inductive types the compiler generates the equality
function in a consistent manner.

- The equality operator “=” can be assigned to a functions only if the
function is inherited from the class COMPARABLE. The operator “=” is
reserved for this function.

- The class COMPARABLE can be inherited multiply, i.e. it is possible to
define various equivalence relations for a type. In order to achieve this
the operator “=” can be renamed (e.g. =.alpha, =.beta, …). But immutable
types must always have one inheritance of COMPARABLE without rename of “=”
which guarantees the property “no_identity”.

Example of a mutable type: BUFFER

User’s view only

In the following we give just the specifications of functions and procedures
i.e. we describe only the view of a potential user of the module.

A complete definition of a routine looks like

  some_routine(a:A)
    require
      pre_1; pre_2; ...
    do
      cmd_1; cmd_2; ...
    ensure
      post_1; post_2; ...
    end

The specification part only contains

  some_routine(a:A)
    require
      pre_1; pre_2; ...
    ensure
      post_1; post_2; ...
    end  

This specification says that “some_routine” is an effective routine (it is not
deferred) and that the implementation is given at a different location.

The basic access functions

For the user a buffer is a generic class.

  class
    BUFFER[G]
       -- A bounded buffer of elements of type G implemented
       -- as contiguous memory cells
  end

A buffer has a certain maximum capacity and a content.

  feature
    capacity(b:CURRENT): NATURAL
        -- The capacity of the buffer.

    content(b:CURRENT): ghost LIST[G]
        -- The content of the buffer.
  end

The content is a ghost function, i.e. it can be used only in
assertions. Having these two basic functions a lot of useful functions can be
specified.

  feature
    count(b:CURRENT): NATURAL
        -- The number of elements in the buffer.
      ensure
        Result = b.content.count
      end

    [] (b:CURRENT, i:NATURAL): G
        -- The i-th element of the buffer.
      require 
        i < b.count
      ensure
        Result ~ b.content[i]
      end

    is_empty(b:CURRENT): BOOLEAN
      ensure
        Result = (b.count = 0)
      end

    is_full(b:CURRENT): BOOLEAN
      ensure
        Result = (b.count = b.capacity)
      end

    first(b:CURRENT): G
      require 
        not b.is_empty  
      ensure
        Result ~ b.content.first
      end

    last(b:CURRENT): G
      require 
        not b.is_empty 
      ensure
        Result ~ b.content.last
      end
  end

Recall that we just give the specification here. The function “count” is
specified based on the function “content”. This says nothing about the
implementation. Certainly the implementation has to do it differently because
“content” is a ghost function and therefore cannot be used in actual
computations.

Framing

The complete set of functions has the following dependency graph (from the
users point of view).

                Dependency graph

                          is_empty    is_full
                            |         /  |
                            |        /   |
    first   last  []       count..../    |
       \     \     \       /             |
        \     \     \     /              |
         \     \     \   /               |
          .......... content          capacity

The dependency graph must reflect a hierarchy, i.e. a partial order. Cyclic
definitions are not allowed. Therefore there are always functions which do not
have a specification i.e. functions which are at the bottom of the dependency
hierarchy.

The dependency graph is used by the user to derive the effect of modifying
procedures. The basic rule in Modern Eiffel: A procedure must not have any
unspecified effects. Let’s assume the following procedure specification

  some_procedure(b:CURRENT)
    ensure
      not b.is_empty
    end

This procedure may change a lot but not everything. It affects “is_empty”,
therefore it must have affected “count” and “content”. A modification of
“content” might affect “first”, “last” and “[]” as well. The only function
which must not be affected by “some_procedure” is “capacity”. This is the
implicit framing condition which the user can derive from the specification or
“some_procedure”.

The verifier augments the above specification to the following complete
specification

  some_procedure(b:CURRENT)
    ensure
      not b.is_empty
      all(a:CURRENT) a.capacity = old a.capacity
      all(a:CURRENT)
        require
          a /~ b
        ensure
          a.is_empty = old a.is_empty
          a.count    = old a.count
          a.content  = old a.content  -- needs to be kept
        end
    end

The algorithm to derive the implicit contract is straightforward. The
postcondition states that “is_empty” might have changed. This has the
following consequences:

- All basic functions at the bottom of the dependency graph on which
“is_empty” does not depend are unchanged.

- The function “is_empty” is only changed for the given argument “b”. For
other arguments it is unchanged.

- The fact that “is_empty” is unchanged for arguments different from “b” is
propagated down the dependency graph (only the conditions for the basic
functions need to be kept, the others are consequences).

It would be very tedious to write these complete specifications. Therefore the
compiler has to derive them automatically. I.e. the user of “buffer” has these
conditions available to prove its own routine and the proof engine verifies
that the implementation of “buffer” respects the implicit frame contract.

Invariant

Mutable objects can be created and modified. It is possible to require some
consistency conditions which are always satisfied by any object of a certain
type. These consistency conditions are called invariants.

Each creation procedure has to establish the invariant and each procedure
which modifies the object has to maintain the invariant.

The buffer is supposed to guarantee the invariant that it does not contain
more elements than is allowed by its capacity.

  invariant
    all(b:CURRENT)
      b.count <= b.capacity
  end

Note that an invariant is something different from other assertions. E.g. the
module buffer guarantees the assertion

  feature
    all(b:CURRENT)  b.count = b.content.count
  end

But this is not an invariant. This condition is already guaranteed by the
specification of the function “count” (see declaration above) which any
implementation of “count” has to respect. I.e. this assertion is not a
requirement for creation procedures and other procedures.

Creation

A buffer can be created with the creation procedure “with_capacity”. I.e. the
code snippet

  local
    b: BUFFER[STRING]
  do
    create b.with_capacity(100)
    ...
  end

creates an empty buffer with the capacity to store 100 strings. The creation
procedure is specified as

  create
    with_capacity(b:CURRENT, c:NATURAL)
      ensure
        b.content  = nil
        b.capacity = c
      end
  end

The verifier has to check that “with_capacity” establishes the invariant. The
proof of the invariant “b.count<=b.capacity” is trivial given the
postcondition of “with_capacity”. Since “b.content=nil” and “nil.count=0″ we
have “b.count=0″ which satisfies the invariant.

The compiler derives from the specification of the creation procedure
“with_capacity” the complete contract including framing conditions

  create
    with_capacity(b:CURRENT, c:NATURAL)
      ensure
        b.content  = nil
        b.capacity = c
        all(a:CURRENT)
          require
            a /~ b
          ensure
            a.content  = old a.content
            a.capacity = old a.capacity
          end
      end

Since the object is created by “create b.with_capacity(100)” the compiler
derives the obvious fact that the newly created object is not identical with
any existing object (otherwise it were not new). This fact together with the
complete contract allows the user to verify the code following the creation of
an object. The verifier can derive that no existing object will be changed
after the creation of a new one.

Insert and modify elements

We can insert elements at the rear end and at the front end, we can overwrite
an element at a certain position and we can rotate the whole buffer.

The following code specifies these procedures.

  feature
    extend_rear(b:CURRENT, e:G)
        -- Append element `e' at the end of buffer `b'
      require
        not b.is_full
      ensure
        b.content = old (b.content + e)
      end

    extend_front(b:CURRENT, e:G)
        -- Prepend element `e' at the front of buffer `b'
      require
        not b.is_full
      ensure
        b.content = old (e :: b.content)
      end

    put(b:CURRENT, i:NATURAL, e:G)
        -- Overwrite element at position `i' with `e' within the buffer `b'.
      require
        i < b.count
      ensure
        b.content = old (b.content.take(i) + e + b.content.drop(i+1))
      end

    rotate_up(b:CURRENT)
        -- Rotate the content of the buffer up.
      require
        not b.is_empty
      ensure
        b.content = old (b.content.last + b.content.without_last)
      end
  end

The compiler derives for all these procedures a complete contract. E.g. for
the procedure “extend_rear” it derives the complete frame contract.

  extend_rear(b:CURRENT, e:G)
      -- Append element `e' at the end of buffer `b'
    require
      not b.is_full
    ensure
      -- complete frame contract
      b.content  = old (b.content + e)
      all(a:CURRENT)
        a.capacity = old a.capacity
      all(a:CURRENT)
        require
          a /~ b
        ensure
          a.content  =  old a.content
        end
    end  

The complete frame contract is a requirement for the implementation. The user
of “extend_rear” can rely on the complete frame contract. Since the complete
frame contract is derived automatically there is no need to type it in. The
basic contract “b.content = old b.content + e” is sufficient.

Even if the implementation is not yet available it is possible to proof that
the invariant is maintained (i.e. the invariant is valid at the end if it has
been valid at the entry point. The proof can be done by the proof engine so
there is no need to provide a proof. We give an explicit pedantic proof here
in order to demonstrate that the proof is a triviality.

  all(b:CURRENT, e:G)
    require
      not is_full
      b.count <= b.capacity
    do
      check
        b.count /= b.capacity  -- "not is_full"
        b.count <  b.capacity
        b.content.count < b.capacity
        b.content.count + 1 <= b.capacity
        (b.content+e).count <= b.capacity
      end

      extend_rear(e)

      check
        b.content.count <= b.capacity
      end
    ensure
      b.count <= b.capacity
    end

Multiple equivalence relations with multiple inheritance

For the type BUFFER there are two equivalence relations which make
sense. Either consider two buffers equal if they have the same content or
consider them equal if they have the same content and the same size.

In Modern Eiffel we have multiple inheritance with replication. This allows us
to have both relations in the same type.

Remember that the abstract class COMPARABLE defines an equivalence
relation. The module “comparable” looks like

  deferred class COMPARABLE end

  feature
    = (a,b:CURRENT): BOOLEAN
      deferred end

    all(a,b,c:CURRENT) 
      deferred
      ensure
        a=a
        (a=b) => (b=a)
        (a=b) => (b=c) => (a=c)
      end
  end

This module has a deferred predicate “=” and some deferred proofs. An
effective module which implements COMPARABLE has to implement “=” and provide
the proofs for reflexivity, symmetry and transitivity.

In the class BUFFER we just inherit COMPARABLE twice.

  class
    BUFFER[G]
  inherit
    COMPARABLE
    COMPARABLE
      rename = as =.content end
  end

  feature
    =.content (a,b:CURRENT): BOOLEAN
      ensure
        Result = (a.content = b.content)
      end

    = (a,b: CURRENT): BOOLEAN
      ensure
        Result = (a.content=b.content and a.capacity=b.capacity)
      end
  end

The proofs of reflexivity, symmetry and transitivity are trivial and derived
automatically. Clearly the predicates “=” and “=.content” need an
implementation because their specification is based on ghost functions
i.e. not executable.

Having these two equivalence relations we can use expressions of the form

  local
    a,b: BUFFER[NATURAL]
  do
    ...
    if a = b then
      ... 
    end

    if a =.content b then
      ...
    end
  end

For those who prefer unqualified calls

In the above code all procedures and functions have been taken out of the
class in order to make the arguments more explicit. This is not necessary. As
long as the first argument of a function or a procedure is of the current
type, we can put these routines back into the class. I.e. it is possible (and
maybe more convenient) to write specifications like

  class BUFFER[G] feature
    count: NATURAL
        -- The number of elements in the buffer.
      ensure
        Result = content.count
      end

    [] (i:NATURAL): G
        -- The i-th element of the buffer.
      require 
        i < count
      ensure
        Result ~ content[i]
      end
    ...
  invariant
    count <= capacity  
  end


  class BUFFER[G] feature
    extend_rear(e:G)
        -- Append element `e' at the end of the buffer
      require
        not is_full
      ensure
        content = old (content + e)
      end
  end

Note that the file “buffer.e” can have more than one class block with the same
class. The class declarations are handled cumulatively. The first class block
might just declare the class “class X end”. A second block might specify the
inheritance relation “class X inherit P end. Other blocks can specify
features, invariants, assertions, etc.

Standalone feature blocks can be used to specify static features
(i.e. routines which do not have an implicit first argument of type CURRENT).

One block might just specify a routine, another block (in the corresponding
implementation file) can implement the routine.

This gives a lot of flexibility in declaring, specifying and implementing
classes.

About these ads