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
If s is not empty
gives the first element. I.e
P2: not [e].is_empty and [e] = e
If s is not empty, we can define the tail of the list s
as the sequence s with the first element removed.
With the operator "+" as the concatenation operator we get the property
P3: [s] + s[1..] = s
for any non empty list s or
P4: ([e] + s) = 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 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
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
domain(exp) means that all preconditions of the queries in
are fulfilled i.e. the expression can be evaluated without causing an
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
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
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,
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: