The Eiffel Compiler / Interpreter (tecomp)

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.

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.

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

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

Definition:

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

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.

- Note: The weakest precondition calculus requires referential transparency or in Eiffel terms: the expression `exp' can involve only pure queries (i.e. queries without side effect).

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

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.

- Note: The third condition might be better placed into the invariant. If the sequence has more elements than an INTEGER can store, we get an overflow here. If the condition is placed in the invariant, all commands have to satisfy the no overflow condition.

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: