Editing Loop invariant (section)

==Programming language support==

===Eiffel===
The [[Eiffel (programming language)|Eiffel]] programming language provides native support for loop invariants.<ref>[[Bertrand Meyer|Meyer, Bertrand]], ''Eiffel: The Language,'' [[Prentice Hall]], 1991, pp. 129–131.</ref> A loop invariant is expressed with the same syntax used for a [[class invariant]]. In the sample below, the loop invariant expression <code>x&nbsp;<=&nbsp;10</code> must be true following the loop initialization, and after each execution of the loop body; this is checked at runtime.

<syntaxhighlight lang="eiffel">    from
        x := 0
    invariant
        x <= 10
    until
        x > 10
    loop
        x := x + 1
    end</syntaxhighlight>

===Whiley===
The [[Whiley (programming language)|Whiley]] programming language also provides first-class support for loop invariants.<ref>{{cite journal|title=Designing a Verifying Compiler: Lessons Learned from Developing Whiley | doi=10.1016/j.scico.2015.09.006 | volume=113 | journal=Science of Computer Programming | pages=191–220| year=2015 | last1=Pearce | first1=David J. | last2=Groves | first2=Lindsay | doi-access= }}</ref> Loop invariants are expressed using one or more <code>where</code> clauses, as the following illustrates:

<syntaxhighlight lang="whiley">
function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires |items| > 0
// (1) Result is not smaller than any element
ensures all { i in 0..|items| | items[i] <= r }
// (2) Result matches at least one element
ensures some { i in 0..|items| | items[i] == r }:
    //
    nat i = 1
    int m = items[0]
    //
    while i < |items|
    // (1) No item seen so far is larger than m
    where all { k in 0..i | items[k] <= m }
    // (2) One or more items seen so far matches m
    where some { k in 0..i | items[k] == m }:
        if items[i] > m:
            m = items[i]
        i = i + 1
    //
    return m
</syntaxhighlight>

The <code>max()</code> function determines the largest element in an integer array.  For this to be defined, the array must contain at least one element.  The [[postconditions]] of <code>max()</code> require that the returned value is: (1) not smaller than any element; and, (2) that it matches at least one element.  The loop invariant is defined inductively through two <code>where</code> clauses, each of which corresponds to a clause in the postcondition.  The fundamental difference is that each clause of the loop invariant identifies the result as being correct up to the current element <code>i</code>, whilst the postconditions identify the result as being correct for all elements.