[comp.lang.eiffel] trouble with variant assertions

giacomet@venus.ecn.purdue.edu (Frederic B Giacometti) (09/29/90)

I have the 2.2B version on a SunSparc. Has this feature ever been
tested before its release ? 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 ?

How can this happen ?

My feature is:

unit: like Current is
	local i: INTEGER
    do
	Result.Create( dim );
	from i:= 1
	 variant c_1: 100  -- you can put `dim' or 100000 the result is the same
	 until dim < i
	 loop
	   Result.set_cell( field_unit, i, i );
	   io.putint(i); io.new_line;
	   i := i+1
	end
    end;

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

when entering the second loop (i=2)

It's the most trivial iteration. It works perfectly if I remove the
variant. Although similar, some loops work, other don't. I ended up
removing all my variants to see that everything was OK.

I don't want to be nasty; so far I've been much impressed by
most capabilities of the eiffel compiler; but does ISE test its
releases uniformly on all machines ?
I remember, for the silliest one, encountering a "rabs" fonction from the
library which would turn its non-zero negative arguments into zero's.

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.

Thanks,

Frederic Giacometti
School of Industrial Engineering
Purdue University

kimr@eiffel.UUCP (Kim Rochat) (09/30/90)

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

sommar@enea.se (Erland Sommarskog) (10/02/90)

Kim Rochat (kimr@eiffel.UUCP) writes:
)) 	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
>...
>
>This <the exception> 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.

To which one could add that the compiler could have flagged this
error. Putting a constant in the variant must obviously be a
mistake. (Or?)
-- 
Erland Sommarskog - ENEA Data, Stockholm - sommar@enea.se
"Nelly Nilsson n|jer sig numera n{ppeligen med nio n|tter till natten"