Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!uwm.edu!wuarchive!usc!ucsd!hub.ucsb.edu!eiffel!kimr
From: kimr@eiffel.UUCP (Kim Rochat)
Newsgroups: comp.lang.eiffel
Subject: Re: trouble with variant assertions
Summary: Variant used improperly
Message-ID: <416@eiffel.UUCP>
Date: 29 Sep 90 22:26:04 GMT
References: <1990Sep29.054436.16582@ecn.purdue.edu>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 58

In article <1990Sep29.054436.16582@ecn.purdue.edu>, giacomet@venus.ecn.purdue.edu (Frederic B Giacometti) writes:
> In some cases, whatever be the integer variable or constant I put, my
> own trace indicates that an exception for invariant violation is
> generated when intering the second loop.
>
> Does this means that the variant is not initialized to its value and
> remains zero ?

There seems to be some confusion between variants and invariants here.
An invariant is a boolean expression which must be true after each loop
iteration.  A variant is a non-negative integer expression whose value must 
decrease with each loop iteration.

Page 101 of "Eiffel: the Language" says

"The initialization should set the variant to a non-negative value; and
 the loop_body should decrease it on each iteration, while keeping it
 non-negative.  Since the variant is an integer expression, the iterations
 may not go on forever."

	<loop extracted from feature>
> 
> 	from i:= 1
> 	 variant c_1: 100  -- you can put `dim' or 100000 the result is the same
> 	 until dim < i
> 	 loop
> 	   i := i+1
> 	end

The proper variant for the above loop is

	variant c_1: dim + 1 - i

since i is the loop control variable and dim is one less than the loop limit.

> I get:
> ------------------------------------------------------------------------------
> Object Class        Routine              Nature of exception Effect
> ------------------------------------------------------------------------------
> 1ED764 MATRIX3      unit                 "c_1":
> 		  (From MATRIX_SQ)     Loop variant violated.  Fail  
> ------------------------------------------------------------------------------

This is exactly right.  The fact that the loop variant value had not
decreased after the first loop iteration was detected and an exception
was raised.

> Practically, could ISE post a complete list of the bug reports
> they have received for each platform for the 2.2 version ?
> It could save us further troubles and spare us unexpected discoveries.

A list of all bugs fixed since 2.2 and all known unfixed bugs
will be provided with Eiffel version 2.3, which is scheduled to be
released the last of October.

Kim Rochat
Interactive Software Engineering
replies to: eiffel@eiffel.com