The implementation side of framing

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:

– A basic function which is not mentioned in the postcondition (and none of
its dependents either) is unchanged for all possible arguments.

– A basic function mentioned in the postcondition (or any of its dependents)
is changed only for the arguments mentioned in the postcondition (including
the implicit argument “Current”). For all other arguments the function is
unmodified.

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:

– The precondition “not is_full” of the specification must imply the
precondition of the implementation.

– The complete postcondition of the implementation must imply the complete
postcondition of the specification.

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.tail)
      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.tail)
      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
Advertisements
  1. Leave a comment

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: