A loop's variant is an expression that serves to convince software
developers, the readers of their software, and proof tools if available,
that a loop will terminate.

Mathematically, a loop variant should for full generality take its values
in any set that is "well-founded". A set equipped with an order relation
"<" is called well-founded (this is also known as the Descending Chain
Condition or DCC) if any decreasing sequence is stationary, based on the
following definitions:

        - A *sequence* is a total function from N (the set of natural
          integers) to S.

        - A sequence s is *decreasing* if, for any integer i, s (i+1) <= s (i)
          where <= denotes the order relation on S. (Note the use of "<=", not
          "<": "decreasing" here does not necessarily mean "strictly decreasing";
          two successive elements of a decreasing sequence may be equal.)

        - A sequence s is *stationary* if there exists some integer n such
          that s (i) = s (n) for all i >= n.

An example of a well-founded set is N itself with the usual order
relation: any  decreasing sequence, such as 25, 21, 21, 12, 6, ...
cannot go on strictly decreasing forever, so it has to be stationary -
e.g. it can go down to 0 and stay there forever.

As another example, involving a partial order rather than a total one,
consider a tree, finite or infinite, where the relation "<=" between nodes
is defined by: a <= b if node a is an ancestor of node b (that is to say,
a is either b or, recursively, the parent of an ancestor of b). Then every
decreasing sequence is stationary: starting from any node, you will
either stay forever at some intermediate ancestor or, sooner or later,
end up at the root.

On the other hand, the set of non-negative real (or rational) numbers
with the usual "<=" is not well-founded; see e.g. the sequence
1, 1/2, 1/3, 1/4, ..., i.e. s (i) = 1/(i+1), which is decreasing but
not stationary.

Now for the application to software and to the Eiffel loop structure.
Assume that we have a loop and we can associate with it an expression ev
(the variant expression) such that:

        1. - The value of ev at any time is an element of a set V that is
          well-founded for a certain relation <=.

        2. - Every execution of the loop body replaces the value bv that ev
          has before the loop by a new value av (`a' for `after') such that
          av < bv (that is to say, av <= bv and av /= bv).

Then the loop, by the very definition of "well-founded", will
terminate - i.e. will have a finite number of iterations.

[Note: if you are an undergraduate student in computing science and your
school doesn't teach these things as part of the first two years of
the curriculum, you should ask your teachers why - or choose
another school. Also note that for anyone who wants to probe further
there are many good introductory books on the theoretical basis for
programming.]

One could of course define a class WELL_FOUNDED (which, by the way,
would have no connection whatsoever with NUMERIC, as the tree example
shows). But from a sofware engineering perspective that seems overkill.
Assume someone gives you a loop backed by an argument claiming that
the loop will terminate, based on a variant that takes its value
in some strange set. It would be natural for you to reply:

        "Very impressive. But could you please you give me an estimate - no,
        actually just an upper bound will do - on the number of iterations there
        will be, depending of course on the state in which the loop is started?"

If the loop author gives you an answer (a correct one), then that answer
is an alternative variant - an integer variant. Remember that the answer
doesn't have to be precise; it just has to be an upper bound (e.g. something
on the order of 2^n, where n is the real number of iterations, is OK as a
variant - although in practice you will probably not be happy as a
performance-conscious software engineer until you have a better estimate!).

But assume the loop author is unable to answer the above request. You
probably will think that there is something fishy. Few people would
trust a loop for which termination is claimed but no one is able to give
an integer upper bound on the number of iterations.

Thus variants are, and should remain, integers (see ETL pp. 130-131).

        The [**] lapel pin in the header marks adherence to the SELF-DISCIPLINE
        program for quality News exchanges. See http://www.eiffel.com
        or ftp://eiffel.com/pub/discipline.

--

Michael Schweitzer, Swissoft      Geismar Landstr. 16  D-37083 Goettingen
Fax : +49 551 770 35 44           email : eif...@swissoft.h.provi.de

* A loop's variant is an expression that serves to convince software
* developers, the readers of their software, and proof tools if available,
* that a loop will terminate.

* Mathematically, a loop variant should for full generality take its values
* in any set that is "well-founded". A set equipped with an order relation
* "<" is called well-founded (this is also known as the Descending Chain
* Condition or DCC) if any decreasing sequence is stationary, based on the
* following definitions:

*       - A *sequence* is a total function from N (the set of natural
*         integers) to S.

*       - A sequence s is *decreasing* if, for any integer i, s (i+1) <= s (i)
*         where <= denotes the order relation on S. (Note the use of "<=", not
*         "<": "decreasing" here does not necessarily mean "strictly decreasing";
*         two successive elements of a decreasing sequence may be equal.)

*       - A sequence s is *stationary* if there exists some integer n such
*         that s (i) = s (n) for all i >= n.

* An example of a well-founded set is N itself with the usual order
* relation: any  decreasing sequence, such as 25, 21, 21, 12, 6, ...
* cannot go on strictly decreasing forever, so it has to be stationary -
* e.g. it can go down to 0 and stay there forever.

* As another example, involving a partial order rather than a total one,
* consider a tree, finite or infinite, where the relation "<=" between nodes
* is defined by: a <= b if node a is an ancestor of node b (that is to say,
* a is either b or, recursively, the parent of an ancestor of b). Then every
* decreasing sequence is stationary: starting from any node, you will
* either stay forever at some intermediate ancestor or, sooner or later,
* end up at the root.

* On the other hand, the set of non-negative real (or rational) numbers
* with the usual "<=" is not well-founded; see e.g. the sequence
* 1, 1/2, 1/3, 1/4, ..., i.e. s (i) = 1/(i+1), which is decreasing but
* not stationary.

* Now for the application to software and to the Eiffel loop structure.
* Assume that we have a loop and we can associate with it an expression ev
* (the variant expression) such that:

*       1. - The value of ev at any time is an element of a set V that is
*         well-founded for a certain relation <=.

*       2. - Every execution of the loop body replaces the value bv that ev
*         has before the loop by a new value av (`a' for `after') such that
*         av < bv (that is to say, av <= bv and av /= bv).

* Then the loop, by the very definition of "well-founded", will
* terminate - i.e. will have a finite number of iterations.

* [Note: if you are an undergraduate student in computing science and your
* school doesn't teach these things as part of the first two years of
* the curriculum, you should ask your teachers why - or choose
* another school. Also note that for anyone who wants to probe further
* there are many good introductory books on the theoretical basis for
* programming.]

* One could of course define a class WELL_FOUNDED (which, by the way,
* would have no connection whatsoever with NUMERIC, as the tree example
* shows). But from a sofware engineering perspective that seems overkill.
* Assume someone gives you a loop backed by an argument claiming that
* the loop will terminate, based on a variant that takes its value
* in some strange set. It would be natural for you to reply:

*       "Very impressive. But could you please you give me an estimate - no,
*       actually just an upper bound will do - on the number of iterations there
*       will be, depending of course on the state in which the loop is started?"

* If the loop author gives you an answer (a correct one), then that answer
* is an alternative variant - an integer variant. Remember that the answer
* doesn't have to be precise; it just has to be an upper bound (e.g. something
* on the order of 2^n, where n is the real number of iterations, is OK as a
* variant - although in practice you will probably not be happy as a
* performance-conscious software engineer until you have a better estimate!).

* But assume the loop author is unable to answer the above request. You
* probably will think that there is something fishy. Few people would
* trust a loop for which termination is claimed but no one is able to give
* an integer upper bound on the number of iterations.

* Thus variants are, and should remain, integers (see ETL pp. 130-131).

This is all right. There is another reason why variants should remain
integers. Allowing WELL_FOUNDED class brings us into a logical loop. The
problem with it is that the question whether a certain class that
inherits from WELL_FOUNDED  really is well-founded is not
computationally decidable. No preconditions or class invariants will
help.

The intention of variants is to let the computer (or a human) decide
whether the loop is OK or not by simply looking at the value of
variant.  If, however, variant could be any object with its class
inheriting from WELL_FOUNDED, observing variant would do us little
good, because the nature of that variant can be questioned.

The whole purpose of variants would be defeated.

If {x_n} is a sequence of floating-point numbers such that every x_n
is positive and such that x_{n+1} < x_n, then the sequence must
be finite.  A floating-point variable could, then, be used as
a loop variant and would give assurance that the loop would
terminate, just as an integer loop variant would.

So fl.pt. expression that decreases each time through loop on m/c
with 24-bit mantissa may not change at all for several iterations
on m/c with 20 bit mantissa.  Whereas monotonic decreasing integer
expression will decrease on *all* architectures.