# 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