SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/internals/verify eiffel sw/sequences

sequences

A sequence of elements of a certain type are is a very basic structure in information processing. Sequences are indispensable for building containers.

The fundamentals of sequences can be expressed with some features.

Fundamentals of sequences

Let us say that s is a sequence of elements. A sequence can be empty or contain at least one element.

Let us denote the empty sequence by

 []
 with P1 [].is_empty

and the list with the element e by

 [e]

If s is not empty

  s[0]

gives the first element. I.e

  P2:  not [e].is_empty and [e][0] = e

If s is not empty, we can define the tail of the list s

  s[1..]

as the sequence s with the first element removed.

With the operator "+" as the concatenation operator we get the property

  P3: [s[0]] + s[1..] = s

for any non empty list s or

  P4: ([e] + s)[0]   = e
  P5: ([e] + s)[1..] = s

for any list s and element e.

I.e. we have the two constructors [] and [e], the function is_empty, tail (i.e. s[1..]) and the sequence concatenation together with the five properties P1,..,P5. If these functions are available and the properties (which might be called axioms) fulfilled, we can talk about sequences. All other necessary functions for sequences can be built based on these functions.

Derived features

The derived features can be defined recursively.

We can define |s| as the number of elements in the list s recursively:

  s.is_empty     => |s| = 0
  not s.is_empty => |s| = 1 + s[1..]

The function s[i] returning the i-th element can be defined recursively as well (provided 0 <= i < |s|)

  i = 0    => s[i] = s[0]
  i > 0    => s[i] = s[1..][i-1]   

The tail of the sequence starting at element i (provided 0 <= i <= |s|)

  i = 0  => s[i..]  = s
  i > 0  => s[i..]  = s[i-1..][1..]

The first i elements of the list (provided 0 <= i < |s|)

  i = 0  => s[0:i-1] = []
  i > 0  => s[0:i-1] = s[0:i-2] + [s[i-1]]

The head of the list (i.e. the list without the last element (provided |s|>0)

  s.head = s[0:|s|-2]      Note: s = s[0:|s|-1]

The sequence with the i-th element removed (provided 0<=i<|s|)

  s.removed(i) = s[0:i-1] + s[i+1..]

and with element e inserted at position i (provided 0<=i<=|s|)

  s.inserted(e,i) = s[0:i-1] + [e] + s[i..]

Sequence as an abstract Eiffel class

deferred class
	SEQUENCE_FL[G]
 
feature -- fundamental features
 
	empty: like Current
		deferred
		ensure
			Result.is_empty
		end
 
	is_empty: BOOLEAN
		deferred
		end
 
	first: G
		require
			not is_empty
		deferred
		end
 
	tail: like Current
		require
			not is_empty
		deferred
		ensure
			tail +| first ~ Current
		end
 
	front_extended alias "+|" (e: G)
                require
                        no_overflow: count + 1 > count
		deferred
		ensure
			not Result.is_empty
			Result.tail  ~ Current
			Result.first ~ e
		end
 
feature -- derived features
 
	count: INTEGER
		do
			if is_empty then
				Result := 0
			else
				Result := 1 + tail.count
			end
		ensure
			is_empty     implies Result = 0
			not is_empty implies Result = 1 + tail.count
			Result >= 0 -- better placed within the invariant
		end
 
 
	one(e:G): like Current
		do
			Result := empty +| e
		ensure
			not Result.is_empty
			Result.first ~ e
			Result.tail  ~ empty
			Result.tail.is_empty
			Result ~ empty +| e
			Result.count = 1
		end
 
	tail_from(i: INTEGER): like Current
			-- Sequence containing the elements from the `i'-th element
			-- to the end of `Current'.
		require
			0 <= i and i <= count
		do
			if i = 0 then
				Result := Current
			else
				Result := tail.tail_from(i-1)
			end
		ensure
			i = 0 implies Result ~ Current
			i > 0 implies Result ~ tail.tail_from(i-1)
			Result.count = count - i
		end
 
 
	head_to(i:INTEGER): like Current
			-- Sequence containing the first i elements of `Current'.
		require
			0 <= i and i <= count
		do
			if i = 0 then
				Result := empty
			else
				check i > 0; not is_empty end
				Result := tail.head_to(i-1) +| first
			end
		ensure
			i = 0  implies   Result.is_empty
			i > 0  implies   Result ~ tail.head_to(i-1) +| first
                        Result.count = i
		end
 
	plus alias "+" (other: like Current): like Current
                require
                        no_overflow: count + other.count >= count
		do
			if is_empty then
				Result := other
			else
				Result := (|tail + other|) +| first
			end
		ensure
			is_empty     implies Result ~ other
			not is_empty implies Result ~ (|tail + other|) +| first
		end
 
        item alias "[]" (i:INTEGER): G
                require
                        0 <= i and i < count
                do
                        Result := tail_from(i).first
                ensure
                        Result ~ tail_from(i).first
                end
 
	subsequence(i,j: INTEGER): like Current
		require
			0 <= i and i <= j and j <= count
		do
			Result := tail_from(i).head_to(j-i)
		ensure
			Result ~ tail_from(i).head_to(j-i)
		end
 
	removed(i: INTEGER): like Current
		require
			0 <= i and i < count
		do
			Result := head_to(i) + tail_from(i+1)
		ensure
			Result ~ head_to(i) + tail_from(i+1)
		end
 
	inserted(e: G; i: INTEGER): like Current
		require
			0 <= i and i <= count
		do
			Result := head_to(i) + (tail_from(i) +| e)
		ensure
			Result ~ head_to(i) + (tail_from(i) +| e)
		end
invariant
        count >= 0
end
 

Proving some features

Definition:

 a[x:=exp]:  Assertion a, where each occurrence of x has been substituted by
 the expression exp.

Assignment statement

Weakest precondition of an assignment:

  wp("x:=exp", a) = domain(exp) and then a[x:=exp]

or in Eiffel notation

    check a[x:=exp] end
    x := exp
    check a end
 

where domain(exp) means that all preconditions of the queries in exp are fulfilled i.e. the expression can be evaluated without causing an exception.

In other words: If we want that assertion a is true after an assignment expression, then the assertion a[x:=exp] has to be true before the assignment.

Conditional statement

The following shows an annotated conditional statement.

  check  -- assertions necessary to prove res
     c1 implies wp("cmp1", res)
     not c1 and c2 implies wp("cmp2", res)
     ...
     not c1 and not c2 and not c3 and ... implies wp("cmpn", res)
  end
 
  if c1 then
      check c1  end 
      cmp1
      check res end
  elseif c2 then
      check not c1; c2 end 
      cmp2
      check res end
  elseif 
      ...
  else
      check not c1; not c2; ... end
      cmpn
      check res end
  end
 
  check res end  --assertion to be proved after the conditional 
 

In order to prove the assertion res after the conditional, we have to prove the check assertion before the conditional.

The necessary expressions are

  wp("cmp1", res)
  wp("cmp2", res)
  ...
  wp("cmpn", res)

It depends on the nature of the corresponding compounds, if they can be calculated. If the compounds only consist of assignments, the weakest preconditions can be calculated by textual substitution.

We can put the proof obligations also inside the branches.

  check pre end
  if c1 then
      check pre; c1  end 
      check wp("cmp1", res) end  -- proof obligation
      cmp1
      check res end
  elseif c2 then
      check pre; not c1; c2 end 
      check wp("cmp2", res) end  -- proof obligation
      cmp2
      check res end
  elseif 
      ...
  else
      check pre; not c1; not c2; ... end
      check wp("cmpn", res) end  -- proof obligation
      cmpn
      check res end
  end
 
  check res end  -- assertion after the conditional to be proven 
 

Proof of feature count

Now let us try to prove the feature count. We annotate the feature for later reference.

	count: INTEGER
		do
			if is_empty then                  -- a1
				Result := 0
			else
                                check not is_empty end    -- a2
				Result := 1 + tail.count
			end
		ensure
			e1: is_empty     implies Result = 0
			e2: not is_empty implies Result = 1 + tail.count
			e3: Result >= 0
		end
 

At position a1 we must satisfy

  e1[Result:=0]:  is_empty implies 0 = 0 <=> is_empty implies True <=> True
  e2[Result:=0]:  not is_empty implies 0 = 1 + tail.count
  e3[Result:=0]:  0 >= 0 <=> True
 

The first and the third are trivially satisfied. The second one requires some thinking.

We know from the if condition that at a1 we have is_empty. Therefore we have to prove

   is_empty implies (not is_empty implies 0 = 1+tail.count)
 

or with a shorthand

   a implies (not a implies x)
 
   not a or else ( a or else x )
 
   not a or else a or else x
 
   (not a or else a) or else x
 
   True  or else x
 
   True
 

Therefore the formula a implies (not a implies x) is always true, regardless of x.

At position a2 we must satisfy:

  e1[Result:=1+tail.count]:  is_empty implies 1+tail.count = 0
  e2[Result:=1+tail.count]:  not is_empty implies 1+tail.count = 1+tail.count
                             <=> not is_empty implies True <=> True
  e3[Result:=1+tail.count]:  1 + tail.count >= 0 <= tail.count >= 0
 

The second condition is trivially satisfied. The third is satisfied, because by definition count always returns something non-negative.

The first condition requires the same reasoning as above. We have to prove

   not is_empty  implies (is_empty implies 1+tail.count = 0)
 

which is always true because it fits into the a implies (not a implies x) pattern which has already been proved above.

I.e. count satisfies its own specification.

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

- Fundamentals of sequences

- Derived features

- Sequence as an abstract Eiffel class

- Proving some features

- Assignment statement

- Conditional statement

- Proof of feature count


ip-location