SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/linked structures

Linked structures (draft)

Introduction

What are linked structures?

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.

References to objects of the same type

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.

Needed proof techniques

Invariants

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).

Universally quantified expression in the postcondition of an assertion

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
 

A link element

Basic declaration

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).

Reachable link elements

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".

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.

Uniqueness of the list of link elements

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
 

Some interesting properties

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
 

Chains and cycles

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 invariant of the link elements

Invariant at startup

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
 

Maintaining the invariant

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").

Link element creation and modification

  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
 

Invariant

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
 

Linked list

Emacs suffix

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

- Introduction

- What are linked structures?

- References to objects of the same type

- Needed proof techniques

- Invariants

- Universally quantified expression in the postcondition of an assertion

- A link element

- Basic declaration

- Reachable link elements

- Uniqueness of the list of link elements

- Some interesting properties

- Chains and cycles

- The invariant of the link elements

- Invariant at startup

- Maintaining the invariant

- Link element creation and modification

- Invariant

- Linked list

- Emacs suffix


ip-location