The Eiffel Compiler / Interpreter (tecomp)

Everybody knows linked lists in the form of singly linked lists or doubly linked lists. In a linked list every list element has a reference to the next list element. The last list element does not have any other element linked to it.

A more elaborate linked structure is a tree. In a tree we might have a lot of references. Each tree element except the root might have a unique reference to its parent. Each tree element except a leaf element might have references to the first and/or last child etc. Each tree element might have references to a sibling.

An even more elaborate linked structure is a arbitrary network of elements (a graph).

In elaborate linked structures it is not trivial to keep the references consistent.

Each non trivial linked structure has elements which might refer to objects of the same type. I.e. the most primitive element looks like

class X feature n: X end

Each object of type X can refer with its function "n" to another object of the same type.

Nearly all object oriented languages use pointers to implement the function "n". A null pointer (or void pointer) breaks the chain. An object with null pointers does not refer to other elements.

In Modern Eiffel we have mutable types. Each variable which has the type T (T is a mutable type) is actually a reference to an object of type T. If two variables "v" and "w" refer to the same object then the condition "v~w" is valid.

Modern Eiffel does not have the concept of a null reference. The language rules guarantee that any variable "v" of type T always refers to an object of type T. It is simply not possible to dereference a void reference.

But in order to implement linked structures we need expressions which have the option to refer to another object or to refer to nothing. For this purpose we have inductive types. The inductive type OPTIONAL achieves this goal.

case class OPTIONAL[G] create none value(value:G) end

To implement a chain of Xs, we can declare the above class as

class X feature n: OPTIONAL[X] end

Now the function "n" returns an object which either is "none" or has a value which is another object of type T. The type OPTIONAL[T] implements the concept of a pointer to an object of type T. The value of "n" is accessible only if "n" has been constructed with the "value" creator. I.e. if you want to access "n.value" it must be provable that "n" has been constructed with "value" (for details see the article "reasoning with inductive types").

You might worry about memory footprint and have the question: Does every object of type OPTIONAL[G] need a tag to discriminate between "none" and "value"?. The answer: No! As long as G is a mutable type. The compiler will optimize any object of type OPTIONAL[G] to a pointer if G is mutable.

For immutable objects invariants are meaningless. The objects are immutable anyhow. There is no need for an invariant.

Mutable types can have invariants. These invariants are sometimes called object invariants. Objects are thought of having attributes and the invariants express consistency conditions between the attributes.

This view is ok as long we talk about objects which cannot have references to other objects of the same type. If there are no such references we can require that the invariant is established by the creation procedures and is maintained by all modifying procedures. It is clear that a procedure can modify only attributes of the current object and reachable objects. These objects are disjoint from the reachables of other objects of the same type.

If we have objects with references to objects of the same type the picture changes. Now we can reach from one object other objects of the same type. I.e. a function operating on an object "a" can return attributes of another object "b" of the same type. If we have a procedure which modifies attributes of object "b" it implicitely might modify return values of functions operating on the object "a".

Therefore it does not make sense to talk about an object invariant. Invariants are now global invariants. This fact will become clear if we extract the invariants from the class.

Normally a class with an invariant looks like

class X feature ... invariant inv_1 inv_2 ... end

If we take the invariant out of the class the arguments become explicit. We get

class X feature ... end invariant all(x:X) inv_1 -- all unqualified calls "f" substituted all(x:X) inv_2 -- by "x.f" ... end

In this view there are no implicit arguments. All arguments are explicit and have to be typed within the corresponding universal quantifier.

Having done this it becomes evident that the invariant does not only specify conditions about the current object but conditions which apply to all objects of a certain type.

This global invariant has to be valid at program start up and must be maintained by all procedures -- creation procedures and other procedures as well.

In case that the universal quantifier contains mutable types, the invariant is vacuously valid at program startup. No objects have been created at program startup, therefore for all objects (which do not yet exist) all conditions are valid.

If the universal quantifier of a global invariant contains only immutable types then the condition is not automatically valid. Let us assume that we have the invariant

all(i:SOME_IMMUTABLE) inv

In order to prove the validity of such an invariant at program startup it is sufficient to prove

all(i:SOME_IMMUTABLE) require all(x:SOME_MUTABLE) False ensure inv end

I.e. at program startup we can assume that no mutable object exists, or in the contrapositive that all mutable objects satisfy any condition (ex falso quodlibet).

Sometimes we have to prove assertions of the following form.

assertion_to_prove: all(stmt:PROGRAM_STATEMENT, pre,post:BOOLEAN) require pre do stmt ensure all(x:G) post end

In order to prove this assertion it is sometimes convenient to move the universal quantifier "all(x:G)" up. I.e. instead of "assertion_to_prove" it is sufficient to prove

sufficient_to_prove: all(x:G, stmt:PROGRAM_STATEMENT, pre,post:BOOLEAN) require pre do stmt ensure post end

This transformation is possible if the identifier "x" does not occur free neither in the statement "stmt" nor in the precondition "pre".

I.e. we have the general rule:

universal_quantifier_up: all(stmt: PROGRAM_STATEMENT, pre,post:BOOLEAN) require all(x:G) require pre do stmt ensure post end ensure require pre do stmt ensure all(x:G) post end end

The most basic building block for linked structures is the type LINK.

-- module "link" deferred class LINK feature next: OPTIONAL[CURRENT] create put(n:OPTIONAL[CURRENT]) ensure next = n end end

Objects of this type have an optional reference to another object of the same type. We can use this basic type to build arbitrary elaborate structures like doubly linked lists, trees, graphs, etc. We can use replication to have any number of links to objects of the same type, e.g.

class TREE_LINK inherit LINK rename next as parent, put as put_parent end LINK rename next as first_child, put as put_first_child end LINK rename next as sibling, put as put_sibling end end

But before building such complex structures we study the behaviour of simple link elements.

The procedure "put" is marked as a creation procedure. This might seem strange at first glance becaues the class LINK is an abstract type and no objects can be created of an abstract type, only of its effective descendants.

Marking a procedure as a creation procedure puts a special requirement on them. Normal procedures can assume that the attributes of the object are already initialized and in a consistent state. Creation procedures cannot make this assumption. On the contrary, they have the additional requirement to initialize all attributes into a consistent state (i.e. a state which is compatible with the invariants).

If we have an object of type LINK we can follow the "next" function until the end or until we meet an object which we have already encountered before.

There are two cases possible:

Two basic topologies r ~~~> a ~~~> b ~~~> c -- The "next" link of the last element is "none" -- Sequence of reachables: -- a, b, c r ~~~> a ~~~> b ~~~> c -- The sequence of links chases its own tail ^ | -- Sequence of reachables: \....... / -- a, b, c, b, c, b, c, ...

In the first case we start from a reference "r" and reach the elements "a", "b" and "c". The "next" of "c" is "none".

In the second case we start from a reference "r" and reach the same sequence of elements. But in this case "c.next" is not "none" but refers to "b" which is already in the sequence. If "c.next" refers to "a" then the links form a cycle. But a cycle is not the most general case. The most general case is depicted above.

Bifurcation is not possible, because the type LINK has only one function "next" to reach other objects of the same type.

We say a list of link elements is linked if all subsequent elements are linked.

is_linked(l:LIST[CURRENT]): ghost BOOLEAN ensure Result = all(a,b:CURRENT) require [a,b] in l.tail_zipped ensure a.next /= none a.next.value ~ b end end

Note: l.tail_zipped is a list zipped with its own tail.

A list of link elements is closed if no link element in the list refers to an element outside the list.

is_closed(l:LIST[CURRENT]): ghost BOOLEAN ensure Result = all(e:CURRENT) require e in l e.next /= none ensure e.next.value in l end end

We design a ghost predicate "reaches(r:OPTIONAL[CURRENT],l:LIST[CURRENT])" which tells whether a list "l" contains exactly the link elements which can be reached from "r" without duplicates. The predicate has the definition

reaches(r:OPTIONAL[CURRENT], l:LIST[CURRENT]): ghost BOOLEAN ensure Result = check start_1: (r=none) = (l=nil) start_2: r/=none => l/=nil and r.value~l.first linked: l.is_linked closed: l.is_closed minimal: not l.has_duplicates end end

This seems to be a complicated definition. But the postcondition expresses in a clear manner what we expect from this list which contains the link elements reachable from "r".

- The list has to start with the element referenced by "r" or be empty if the reference "r" is empty.
- Each consecutive elements of the list are linked.
- Each element in the list is linked to another element in the list (i.e. no element in the list refers to an element outside the list).
- The list does not contain duplicates.

Note that the constructs "check a;b;c;... end" and "a and b and c and ..." are equivalent. However the check construct allows us to label the individual conditions and make the expression more readable. In the same manner we use the fact that "require a;b;... ensure p;q;... end" is equivalent to "a=>b=>...=> (p and q and ...)" to document the intent in a more readable manner.

We say that a reference "r" reaches a link element "e" if "e" is contained in a list which which can be reached from "r".

reaches(r:OPTIONAL[CURRENT], e:CURRENT): ghost BOOLEAN ensure Result = some(l:LIST[CURRENT]) r.reaches(l) and e in l end

We use this predicate "reaches" to define a function which returns the list of reachable link elements given a reference.

list(r:OPTIONAL[CURRENT]): ghost LIST[CURRENT] ensure r.reaches(Result) end

This function does not have a closed form definition with the usual pattern "Result=...". The result is specified with a predicate. The verifier accepts such a definition only if it can be proved that such a list exists and that the list is unique. I.e. the verifier generates the proof obligations

existence: all(r:OPTIONAL[CURRENT]) some(l:LIST[CURRENT]) r.reaches(l) uniqueness: all(r:OPTIONAL[CURRENT], a,b:LIST[CURRENT]) r.reaches(a) => r.reaches(b) => a=b

The uniqueness can be proved by using the definition of the predicate "reaches". We present a proof in the next chapter.

However there is no chance to prove the existence from the given definitions up to now. The reason: From the definition it cannot be excluded that infinitely many objects can be encountered starting from a reference.

The only chance we have is to state the existence condition as a global invariant and prove that the invariant is valid at program startup and is maintained by all procedures (including creation procedures). I.e. we state the invariant

invariant{NONE} all(r:OPTIONAL[CURRENT]) r.has_list end

with the ghost function "has_list"

feature {NONE} has_list(r:OPTIONAL[CURRENT]): ghost BOOLEAN ensure Result = some(l:LIST[CURRENT]) r.reaches(l) end end

Note that the invariant and the ghost function "has_list" can be private. For the user of the class LINK the ghost function "list" is visible. Having such a function has the implicit consequence that such a function exists and its result is unique.

We have to prove: "Whenever there are two list a and b satisfying r.reaches(a) and r.reaches(b), then both list are equal". I.e. we have to prove the following.

all(a:LIST[CURRENT]) ensure all(r:OPTIONAL[CURRENT], b:LIST[CURRENT]) r.reaches(a) => r.reaches(b) => a=b end

The prove can be done by induction on one of the lists. In order to keep the proof short and readable we state two lemmas.

feature{NONE} initial: all(r:OPTIONAL[CURRENT]) -- case "a = nil" require r: r.reaches(nil) check c1: r=none -- r, def "reaches" ensure all(l:LIST[CURRENT]) r.reaches(l) => l=nil -- def "reaches", c1 end induction_step: all(r:OPTIONAL[CURRENT], f:CURRENT, t:LIST[CURRENT]) -- case "a = f::t" require r: r.reaches(f::t) ensure e1: r/=none -- r, def "reaches:start_1 e2: r.value ~ f -- e1, r, def "reaches:start_2 e3: all(b:LIST[CURRENT]) require r.reaches(b) ensure b/=nil -- e1, def "reaches:start_1 b.first ~ f -- e1, def "reaches:start_2 end end end

Both lemmas are evident consequences of the definition of "reaches". The proof can be done by the proof engine automatically.

With these lemmas the proof of uniqueness is easy.

feature{NONE} all(a:LIST[CURRENT]) check inspect a case nil then c1: all(r:OPTIONAL[CURRENT], b:LIST[CURRENT]) r.reaches(nil) => r.reaches(b) => nil=b -- immediate consequence of "initial" case f::t then induction_hypothesis: all(r2:OPTIONAL[CURRENT], bt:LIST[CURRENT]) r2.reaches(t) => r2.reaches(bt) => t=bt c2: all(r:OPTIONAL[CURRENT], b:LIST[CURRENT] require r.reaches(a) r.reaches(b) check r.reaches(f::t) b/=nil -- because "r/=none" and "r.reaches(b)" a.first ~ b.first -- i.e. "f" r.value.next.reaches(a.tail) => r.value.next.reaches(b.tail) => a.tail = b.tail -- from induction hypothesis a.tail = b.tail ensure a=b end end ensure all(r:OPTIONAL[CURRENT], b:LIST[CURRENT]) r.reaches(a) => r.reaches(b) => a=b -- c1,c2 end end

The fact that a reference "r" can reach a link element "e" has some easy to prove consequences.

prop_1: all(r:OPTIONAL[CURRENT], e:CURRENT, u:LIST[CURRENT]) require r: r.reaches(e) check c1: some(l:LIST[CURRENT]) r.reaches(l) and e in l -- r, def "reaches" c2: all(l:LIST[CURRENT] r.reaches(l) and e in l => r/=none -- "l" has elements, therefore not "nil", therefore "r/=none" ensure e1: r/=none -- c1,c2 e2: r.reaches(u) => e in u -- c1, uniqueness e3: r.reaches(u) => u /= nil -- e2 e4: r.reaches(u) => r.value ~ u.first -- e1, def "reaches" end

If a list of link elements is linked, then all elements in the list except the last one are linked.

prop_2: all(l:LIST[CURRENT]) require r1: l.is_linked r2: l/=nil check c1: all(a,b:CURRENT) [a,b] in l.tail_zipped => a in l.without_last -- proved within module "list" c2: all(a,b:CURRENT) [a,b] in l.tail_zipped => a.next/=none -- def "is_linked c3: all(a,b:CURRENT) [a,b] in l.tail_zipped => b in l.tail -- proved within module "list" ensure e1: all(e:CURRENT) e in l => e/~l.last => e.next/=none -- c1,c2 e2: all(e:CURRENT) e in l => e/~l.last => e.next.value in l -- c1, c3, def "is_linked" end

Furthermore it is evident that the property "l.is_linked" of a list of link elements is already "nearly closed". If the list is linked then all elements but the last one must point to an element within the list. By looking at the last element it can be decided whether the list is completely closed.

prop_3: all(l:LIST[CURRENT]) require l.is_linked ensure l=nil => l.is_closed -- def "is_closed" l/=nil => l.last.next=none => l.is_closed -- def "is_closed", prop_2 l/=nil => l.last.next/=none => l.last.next in l => l.is_closed -- def "is_closed", prop_2 end

The property of a list of link elements of being linked is rather strong. If paired with the property of having duplicates this implies that all elements in the list are not void (i.e. "e.next/=none"). Remember that according to "prop_2" only the last element in a linked list of linkables can be void. Now for each list having duplicates we have the property (already proved in the module "list")

prop_4: all(l:LIST[CURRENT]) -- Already proved within module "list" require l.has_duplicates ensure l /= nil some(u,v,w:LIST[CURRENT], e:CURRENT) check l = u + e + v + e + w not (e in v) not (e in w) end end

Now let's assume that "l.is_linked". This implies that "e.next/=none" because there are elements after "e" within the list to which "e" has to be linked. All the elements in "v" have to be linked as well for the same reason. By induction on "w" it can be shown that "w" must be a prefix of "v". Therefore all elements in "w" have to be linked as well. The last element of "l" is either an element of "w" or the element "e". With this reasoning we get the property

prop_5: all(l:LIST[CURRENT]) require l.is_linked ensure l.has_duplicates => l.last.next/=none end

Sometimes the contrapositive of this property is more interesting

prop_6: all(l:LIST[CURRENT]) require l.is_linked l /= nil ensure l.last.next=none => not l.has_duplicates end

For completeness we give the proof by induction on "w".

all(w:LIST[CURRENT]) check inspect w case nil then ca: all(v:LIST[CURRENT]) nil.is_prefix(v) case f::t then induction_hypothesis: all(u,v:LIST[CURRENT], e:CURRENT) ensure (u+e+v+e+t).is_linked => not (e in v) => not (e in t) => t.is_prefix(v) end cb: all(u,v:LIST[CURRENT], e:CURRENT) require r1: (u+e+v+e+w).is_linked r2: not (e in v) r3: not (e in w) check c1: e.next.value ~ f -- r1 c2: f /~ e -- r1, r3 c3: v/=nil and v.first ~ f -- r1, r2, c1, c2 c4: u+e+v+e+w = u+e+f+v.tail+e+f+t -- c3 c5: t.is_prefix(v.tail) -- c4, induction_hypothesis, r2, r3 c6: (f::t).is_prefix(v) -- c5 ensure w.is_prefix(v) -- c6 end end ensure all(u,v:LIST[CURRENT], e:CURRENT) ensure (u+e+v+e+w).is_linked => not (e in v) => not (e in w) => w.is_prefix(v) end -- ca,cb end

A list of linked link elements is chain if the last element in the chain is not linked.

is_chain(l:LIST[CURRENT]): ghost BOOLEAN ensure Result = check l.is_linked l/=nil => l.last.next=none end end

The property of being a chain is stronger that the property of being linked. A chain is always closed and cannot have duplicates.

all(l:LIST[CURRENT]) require l.is_chain ensure l.is_closed -- def "is_chain", prop_3 not l.has_duplicates -- def "is_chain", prop_6 end

If a list of linked link elements which is closed and does not have duplicates and is not a chain then it either contains a cycle or it is a cycle.

has_cycle(l:LIST[CURRENT]): ghost BOOLEAN ensure Result = check l.is_linked l/=nil => l.last.next/=none and l.last.next.value in l end end is_cycle(l:LIST[CURRENT]): ghost BOOLEAN ensure Result = check l.is_linked l/=nil => l.last.next/=none and l.last.next.value ~ l.first end end all(l:LIST[CURRENT]) ensure l.has_cycle => l.is_closed l.is_cycle => l.has_cycle l.is_cycle => l.is_closed end all(u,v:LIST[CURRENT], e:CURRENT) ensure (e::u).is_cycle => (u+e).is_cycle (u+v).is_cycle => (v+u).is_cycle end

The proof of the invariant at startup is easy since we can use the fact that at startup no mutable object exists (or in other words that all mutable objects satisfy any condition).

feature {NONE} all(ref:OPTIONAL[CURRENT]) require r: all(e:CURRENT) False -- At startup no object of type CURRENT exists check inspect ref case none then c1: ref.reaches(nil) case value(v) then some(e:CURRENT) True -- witness "v" all(e:CURRENT) True => False -- r c2: False -- "exist" elimination end ensure some(l:LIST[CURRENT]) ref.reaches(l) -- c1, c2 end end

The class LINK has only one modifying procedure: "put". The proof engine of Modern Eiffel generates the proof obligation

all(e:CURRENT, n:OPTIONAL[CURRENT]) require all(r:OPTIONAL[CURRENT]]) r.has_list do e.put(n) ensure all(r:OPTIONAL[CURRENT]) r.has_list end

which is equivalent to

all(e:CURRENT, n,r:OPTIONAL[CURRENT]) require all(r:OPTIONAL[CURRENT]]) r.has_list do e.put(n) ensure r.has_list end

because "r" does not occur free neither in the precondition nor in the statement "e.put(n)" (see chapter "Needed prove techniques above").

class LINK create make ensure next = none end feature put(n:OPTIONAL[CURRENT]) ensure next = n end end

The procedures with derived complete contracts

class LINK create make ensure next = none all(x:CURRENT) x/~Current => x.next = old x.next end feature put(n:OPTIONAL[CURRENT]) ensure next = n all(x:CURRENT) x/~Current => x.next = old x.next end end

The invariant:

invariant all(r:OPTIONAL[CURRENT]) some(l:LIST[CURRENT]) r.reaches(l) end

The invariant must be maintained by all procedures. I.e. the following is to be proved ("put" is the only procedure):

all(e:CURRENT, n:REF) require all(r:REF]) r.has_list do e.put(n) ensure all(r:REF) r.has_list end

We can transform the proof obligation into the form by moving the universal quantifier of the postcondition up:

all(e:CURRENT, n,r:REF) require all(r:REF]) r.has_list do e.put(n) ensure r.has_list end

This is possible because the identifier "r" does not occur free in the precondition nor in the statement.

Now we make a case split:

all(e:CURRENT, n,r:REF) require all(r:REF]) r.has_list do e.put(n) check r.reaches(e) or not r.reaches(e) -- excluded middle r.reaches(e) => r.has_list not r.reaches(e) => r.has_list end ensure r.has_list end

The general form:

all[G,H](e:BOOLEAN) all(x:G) some(y:H) e

It might be proved with the help of the following lemma.

all[G,H](e:BOOLEAN) require some(a:G) True -- Some object of type G exists all(a,x:G) p[a,x] => some(y:H) e all(a,x:G) not p[a,x] => some(y:H) e check all(a,x:G) require True check if p[a,x] then some(y:H) e else some(y:H) e end ensure some(y:H) e end all(a:G) True => all(x:G) some(y:H) e ensure all(x:G) some(y:H) e end

We use some definitions and a helper function to express the invariant more compact

feature {NONE} REF = OPTIONAL[CURRENT] LST = LIST[CURRENT] has_list(r:REF): ghost BOOLEAN ensure Result = some(l:LST) r.reaches(l) end reaches(r:REF, e:LNK): ghost BOOLEAN ensure Result = some(l:LIST) r.reaches(l) and e in l end end

An additional lemma to apply a case split:

case_split_lemma_forward: all(e:CURRENT) require all(r:REF) r.reaches(e) => r.has_list all(r:REF) not r.reaches(e) => r.has_list check all(r:REF) check r.reaches(e) or not r.reaches(e) r.reaches(e) => r.has_list not r.reaches(e) => r.has_list ensure r.has_list end ensure all(r:REF) r.has_list end

More general form

case_split_lemma_forward: all[G](a,b:BOOLEAN) require all(x:G) a => b all(x:G) not a => b check all(x:G) check a or not a a => b not a => b ensure b end ensure all(x:G) b end

The reverse is a triviality

We apply this lemma and try to prove the invariant

all(e:CURRENT, n:REF) require all(r:REF]) r.has_list do check case_1: all(r:REF) r.reaches(e) => r.has_list case_2: all(r:REF) not r.reaches(e) => r.has_list end e.put(n) check case_1: all(r:REF) r.reaches(e) => r.has_list case_2: all(r:REF) not r.reaches(e) => r.has_list end ensure all(r:REF) r.has_list end

all(e:CURRENT, n:REF) require all(r:REF]) r.has_list do all(r:REF) r.reaches(e) => r.has_list all(r:REF) not r.reaches(e) => r.has_list e.put(n) check e.next = n all(x:CURRENT) x/~e => x.next = old x.next end check some(n:REF) True all(n:REF) True => all(r:REF) check r.reaches(e) or not r.reaches(e) if r.reaches(e) then some(l,u,v:LST) r.reaches(l) and l = u+e+v ??? else ??? end ensure r.has_list end all(n:REF) True => all(r:REF) r.has_list end ensure all(r:REF]) r.has_list end

{A or B} S {R} = ({A} S {R} and {B} S {R}) A or B => wp(S,R)

Let us scrutinize the two interesting cases:

all(e:CURRENT, n,r:OPTIONAL[CURRENT], rl:LIST[CURRENT]) require r.reaches(rl) not (e in rl) do e.put(n) ensure r.reaches(rl) end

all(e:CURRENT, n,r:OPTIONAL[CURRENT], rl,nl,u,v:LIST[CURRENT]) require r.reaches(rl) n.reaches(nl) rl = u + e + v -- rl and nl might have a common suffix do e.put(n) -- operation closes a cycle, if "rl" and "nl" have -- a common suffix ensure r.reaches((u+e+nl).reduced) -- duplicates removed end

The most complicated case is that "r" and "n" can reach "e". This implies that both list "meet" at the element "e" or before. If one list is a chain then both lists are chains and they just share a common tail.

If "n" reaches "e" then the operation "e.put(n)" introduces a cycle. The list "n.list" ends in "e" and "n.is_cycle" is valid. If before "n.reaches(x+e+y)" has been valid then after the operation "n.reaches(x+e)" is valid, i.e. the tail "y" has been cut off.

If "r.reaches(e)" then "r.list=u+e+v" for some "u,v". The list "u" and "x" have a common suffix (which might be empty). The operation "e.put(n)" will certainly cut off "v". It cannot cut off "u". If we introduce the common suffix "s" of "x" and "u" we can rewrite the pre- and postconditions as

all(x,y,s,u,v:LIST[CURRENT], e:CURRENT) require n.reaches(x+s+e+y) r.reaches(u+s+e+v) disjoint(x,u) -- x `disjoint' u do e.put(n) ensure n.reaches(x+s+e) -- "e.next" points to the first element of "x+s+e" (x+s+e).is_cycle (s+e+x).is_cycle r.reaches(u+s+e+x) end

Complete framing condition of the procedure "put":

put(e:CURRENT, n:OPTIONAL[CURRENT]) ensure e.next = n all(f:CURRENT) f/~e => f.next = old f.next end

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