SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/framing implement

The implementation side of framing in the module "buffer"

The specification

In the previous article the specification of a buffer of elements of a certain type has been described. Let us repeat here shortly the essence of the specification.

  class  BUFFER[G]  feature
      capacity: NATURAL
      content:  ghost LIST[G]
      count:    NATURAL
          ensure Result = content.count end
      [] (i:NATURAL): G
          require i < count ensure
              Result ~ content[i]
          end
      is_empty(CURRENT): BOOLEAN
          ensure Result = (count = 0) end
      is_full(CURRENT): BOOLEAN
          ensure Result = (count = capacity) end
      first: G
          require not is_empty ensure
              Result ~ content.first
          end
      last: G
          require not is_empty ensure
              Result ~ content.last
          end
  invariant
      count <= capacity
  create
      with_capacity(b:CURRENT, c:NATURAL)
          ensure
              content  = nil
              capacity = c
          end
  feature
      extend_rear(e:G)
          require not is_full ensure
              content = old content + e
          end
      extend_front(e:G)
          require not is_full ensure
              content = e :: old content
          end
      put(i:NATURAL, e:G)
          require i < count ensure
              content = old content.take(i) + e + old content.drop(i+1)
          end
      rotate_up
          require not is_empty ensure
              content = old content.last + old content.without_last
          end
  end
 

The functions viewed from the user's perspective have the following dependency graph (higher functions depend on lower functions).

       Dependency graph (specification view)
 
                          is_empty    is_full
                            |         /  |
                            |        /   |
    first   last  []       count..../    |
       \     \     \       /             |
        \     \     \     /              |
         \     \     \   /               |
          .......... content          capacity
 

Implementation

We start to implement the module "buffer". Let us start to develop the implementation view independently from the specification view. In a second step we will make sure that both views are consistent, i.e. that the implementation satisfies the specification.

By "implementation" we mean the contract of the implementation and not the body. This distinction between the contract of a specification and the contract of an implementation might seem strange at first glance. An indeed in many practical cases both contracts coincide. But in order to be able to reason about the specification and the implementation with precise rules it is necessary to distinguish between the contract of the specification and the contract of the implementation.

Any feature block which is introduced by

  feature {NONE}
 

belongs to the implementation. The "{NONE}" specifies that the following is invisible to the users. A similar characterisation is possible for invariants, i.e.

  invariant {NONE}
 

starts an invisible invariant block.

We use the invisibility marker "{NONE}" as well for pre- and postconditions to express the fact that they belong to the implementation contract.

Now back to our example "buffer".

Implementation of the functions

The implementation decides to use "count", "capacity" and "[]" as the basic functions and define the others based on these basic functions. I.e. the implementation of a buffer might look like:

  -- file: "buffer.e.imp"
  class BUFFER[G] feature {NONE}
      count: NATURAL
          note built_in end
      capacity: NATURAL
          note built_in end
      [] (i:NATURAL): G
          require i < count note built_in end
      is_empty: BOOLEAN
          ensure Result = (count=0) end
      is_full: BOOLEAN
          ensure Result = (count=capacity) end
      first: G
          require not is_empty ensure Result = Current[0] end
      last: G
          require not is_empty ensure Result = Current[count-1] end
      content: ghost LIST[G]
          ensure
              Result.count = count
              all(i:NATURAL) i<count => Result[i] ~ Current[i]
          end
  invariant {NONE}
      count <= capacity
  end
 

The basic functions "count", "capacity" and "[]" are built-in functions. A buffer is a built-in type like the types BOOLEAN and NATURAL.

The specifications of the dependent functions are straightforward. Only the function "content" has not been defined by a closed expression like "Result~...". Instead of a closed form, the function "content" has been defined by its properties.

Modern Eiffel allows to define functions with properties. However it creates the proof obligation that such a function must exist and be unique. This is no problem in the case of "content" since a list is uniquely defined by its length and its elements. The existence and uniqueness proof should be done in the module "list". Here we assume that such a proof is available from the module "list".

For completeness we spell out the assertion whose proof is expected from the module "list".

  all[G](c:NATURAL, f:NATURAL->G)
      require
          all(i:NATURAL) i<c => f.is_defined(i)
      ensure
        local
            p := l:LIST[G] -> c=l.count and all(i:NATURAL) i<c => f[i]~l[i]
        then
            exist:  some(l:LIST[G]) l in p
            unique: all(a,b:LIST[G]) a in p => b in p => (a=b)
        end
      end
 

Note how anonymous predicates can be used to express the existence and uniqueness in a very concise way. This assertion states exactly that a list is completely and uniquely determined by its length and its elements.

Dependency graph in the implementation view

The implementation sees the following dependency graph.

          Dependency graph (implementation view)
 
   first  last    content       is_empty   is_full
       \   /      /     \          |       /    |
        \ /      /       \         |      /     |
        []....../         \......count.../   capacity
 

Note that this dependency graph is completely different from the dependency graph of the specification view.

Consistency between the specification and implementation of the functions

A specification and an implementation are consistent if the implementation implements the specification. This consistency can be described by some precise rules.

--specification                      implementation
 
  func(a:A): RT                      func(a:A): RT
    require                            require{NONE}
      spec_pre                           imp_pre
    ensure                             ensure{NONE}
      spec_post                          imp_post
    end                                end
 
 
--                  consistency
 
                 spec_pre => imp_pre
 
                 imp_post => spec_post
 
 

The consistency can be verbally expressed as: The precondition of the implementation must be weaker than the precondition of the specification. The postcondition of the implementation must be stronger than the postcondition of the specification (weaker and stronger include equivalent!).

In case that there is no contract the implicit assertion "True" is assumed.

The contracts of the functions "capacity", "is_empty" and "is_full" are the same in the specification view and the implementation view. Therefore no inconsistency can arise for these functions.

The function "content" does not have a contract in the specification view. The implementation has a postcondition for "content". I.e. the consistency condition is satisfied for "content".

The specification of "count" expects the following contract:

  count: NATURAL
      ensure
          Result = content.count
      end
 

The implementation does not have a contract. Therefore it does not directly satisfy the specification. However it is not necessary to proof the consistency from the contract of the implementation alone. We can use all other already available assertions.

The implementation of "content" gives the following guarantee

  content_implementation:
  all(b:CURRENT)
      ensure
          b.count = b.content.count
          all(i:NATURAL) i<b.count => b.content[i]~b[i]
      end
 

Using this guarantee it is easy to proof the postcondition of the specification of "count". The postcondition of the specification of "count" is an immediate consequence of the guarantee "content_implementation".

The specification of "[]" expects the following contract:

  [] (i:NATURAL): G
      require
          i < count
      ensure
          Result ~ content[i]
      end
 

The preconditions of the specification and the implementation are identical. The postcondition of the specification is an immediate consequence of "content_implementation".

In this manner it can be demonstrated that the implementation satisfies all contracts required by the specification of the functions.

The procedure "extend_rear"

The procedure is implemented as a built-in procedure with the following implementation.

  extend_rear(e:G)
      require {NONE}
          count < capacity
      note
          built_in
      ensure {NONE}
          count = old count + 1
          Current[count-1] ~ e
      end
 

According to the dependency graph of the implementation view the compiler derives the following complete contract including framing conditions.

  extend_rear(e:G)
      require {NONE}
          count < capacity
      note
          built_in
      ensure {NONE}
          count = old count + 1
          Current[count-1] ~ e
 
          all(a:CURRENT) a.capacity = old a.capacity
 
          all(i:NATURAL)
            require
              i /= count-1
              i < count
            ensure
              Current[i] ~ old Current[i]
            end
 
          all(a:CURRENT)
            require
              a /~ Current
            ensure
              a.count = old a.count
              all(i:NATURAL) i<a.count => a[i] ~ old a[i]
            end
      end
 

This complete contract results from the application of the rules to derive the frame contract:

Note how short the implicit contract is and how long the derived complete contract is. Fortunately it is not necessary to spell out the complete contract. The compiler derives the complete contract behind the scenes.

From the complete contract the following proof obligations are generated:

Both proofs are straightforward and can be done by the proof engine automatically.

The procedure "put"

The procedure "put" is implemented as a built-in procedure.

  put(i:NATURAL, e:G)
      require {NONE}
          i < count
      note
          built_in
      ensure {NONE}
          Current[i] ~ e
      end
 

The compiler derives from this contract the following complete contract with framing conditions.

  put(i:NATURAL, e:G)
      require {NONE}
          i < count
      note
          built_in
      ensure {NONE}
          Current[i] ~ e
 
          all(a:CURRENT)
           ensure
               a.count    = old a.count
               a.capacity = old a.capacity
           end
 
          all(j:NATURAL) i/=j => Current[j] ~ old Current[j]
 
          all(a:CURRENT, j:NATURAL)
            require
                a /~ Current
                j < a.count
            ensure
                a[j] ~ old a[j]
            end
      end
 

There is no magic in these complete contracts. The contract says that "[]" is modified at the arguments "Current,i". "[]" is a basic function. Therefore "[]" is not modified at all other argument positions. Neither "count" nor "capacity" are modified neither for "Current" nor for any other object. All objects different from "Current" are not modified at all. The dependency graph is sufficient to generate the complete contract.

The procedure "rotate_up"

The implementation of "rotate_up" decides to use the contract

  rotate_up
      require {NONE}
          not is_empty
      do
        ...
      ensure {NONE}
          content = old (content.last :: content.without_last)
      end
 

i.e. the implementation has the same contract as the specification. We use the contract to derive the complete contract in the implementation view.

  rotate_up
      require {NONE}
          not is_empty
      do
        ...
      ensure {NONE}
          content = old (content.last :: content.without_last)
 
          all(a:CURENT) a.capacity = old a.capacity
 
          all(a:CURRENT, i:NATURAL)
            require
                a /~  Current
            ensure
                a.content = old a.content
                a.count = old a.count
                i<a.count => a[i] ~ old a[i]
            end
      end
 

According to our rules the complete contract of the specification looks like

  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)
 
      all(a:CURRENT) a.capacity = old a.capacity
 
      all(a:CURRENT)
        require
          a /~ Current
        ensure
          a.content = old a.content
        end
    end
 

This example makes clear that even if the contracts of the specification and the implementation coincide, the complete contracts can differ. The difference stems from the fact that the specification view and the implementation view see different functions at the bottom of the dependency graph. Since the unmodified parts are always expressed in terms of the basic functions both complete contracts look different.

But as long as the contracts coincide even if the complete contracts differ, the derivation of the complete contracts cannot introduce any inconsistency between both views. This has the following reason.

The complete contracts differ only in the part which specifies unmodified functions. The complete contract is derived by propagating the unmodified functions down the dependency graph. Both views might arrive at different basic functions. But the condition that they are unmodified imply that all upper functions are unmodified as well (recall that the upper functions depend completely on the lower functions).

Body of "rotate_up"

We want to write the body of

  rotate_up
      require {NONE}
          not is_empty
      do
        ...
      ensure {NONE}
          content = old (content.last :: content.without_last)
      end
 

Clearly we have to write a loop to achieve this. We copy the last element to a temporary variable and then shift all elements one position up starting from the end (in order not to overwrite elements before having them copied). I.e. we want a loop with the loop index "i" and the invariant

  local
      c0: ghost LIST[G] := old content
      i: NATURAL
  then
      i < b.count
      content = c0.take(i+1) + c0.drop(i).without_last
  end
 
  -- c0.take(i+1): The first i+1 elements of c0
  -- c0.drop(i):   c0 with the first i elements dropped
  -- all(k:NATURAL) k<=c0.count => c0 = c0.take(k) + c0.drop(k)
 

We start the loop with "i+1=count". "c0.take(i+1)" represents the original list. "c0.drop(i)" is a one element list with the last element of the original list. "c0.drop(i).without_last" is empty. I.e. the invariant is valid at the start of the loop.

We terminate the loop with "i=0". "c0.take(i+1)" is a list with only one element i.e. the first element of the original list. "c0.drop(i)" is the original list and "c0.drop(i).without_last" is the original list without the last element. I.e. "i=0" is exactly the situation where we are ready with shifting up. The first element is duplicated and all elements are shifted one position up and the position of the last one has been overwritten.

The following implementation establishes the required result.

  rotate_up(b:CURRENT)
      require
          not b.is_empty
      local
          c0: ghost LIST[G] := content
          i:  NATURAL       := count - 1
          t:  G             := last
      do
          from invariant
              i < count
              content = c0.take(i+1) + c0.drop(i).without_last
          variant
              i
          until
              i = 0
          loop
              Current[i] := Current[i-1]  -- i.e. put(i, Current[i-1])
              i := i - 1
          end
          check
              content = c0.first :: c0.without_last
          end
          put(0, t)
      ensure
          content = old (content.last :: content.without_last)
      end
 

In some later articles I will give a more detailed description of how to reason with loops and loop invariants. But even without detailed knowledge it should be clear that the loop invariant is valid at the start of the loop and that the loop invariant is reestablished at the end of each iteration. At the end of the loop the invariant and the exit condition are valid. The loop invariant and the exit condition imply the desired result at the end of the loop.

In the last step we just need to overwrite the first element with the value of "t" (i.e. the last element of the original content).

Note how ghost variables and ghost functions can be used to express the loop invariant exactly and readable at the same time.

Procedure "extend_front"

For completeness we give the complete implementation of "extend_front".

  extend_front(e:G)
      require
          is_extendible
      do
          extend_rear(e)
          if 1 < count then
              rotate_up
          end
      ensure
          content = old (e::content)
      end
 

Emacs suffix

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

- The specification

- Implementation

- Implementation of the functions

- Dependency graph in the implementation view

- Consistency between the specification and implementation of the functions

- The procedure "extend_rear"

- The procedure "put"

- The procedure "rotate_up"

- Body of "rotate_up"

- Procedure "extend_front"

- Emacs suffix


ip-location