SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/framing

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.

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:

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.

Emacs suffix

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

- Basics

- Equality and identity

- Example of a mutable type: BUFFER

- User's view only

- The basic access functions

- Framing

- Invariant

- Creation

- Insert and modify elements

- Multiple equivalence relations with multiple inheritance

- For those who prefer unqualified calls

- Emacs suffix


ip-location