PR# 2916 ARRAY.put(QNAN) fails postcondition in MSVC v7

The post condition on 'put' in ARRAY (inherited from INDEXABLE) is:

	insertion_done: item (k) = v

This test fails when v is the IEEE quiet not-a-number (QNAN) and Visual C++ V7 is used.  The C code that you generate is essentially 'if (a==b)...'.  The assembly code generated by Microsoft uses the FCOMP instruction which sets three condition code - C0 (less than), C3 (equal to), C2 (unordered).  When one of the operands is QNAN, all three codes are set, even when QNAN is compared to itself.  In v6, the compiler only check C3 and will happily proclaim that any value is equal to QNAN (defeating the purpose of the ensure).  In v7 they are more careful and now QNAN==x is always 'false'.  Specifically QNAN==QNAN is 'false' and therefore the postcondition fails.


We propose that the postcondition on 'put' in INDEXABLE be changed to:

	insertion_done: item (k) = v or else (v/=v and item(k)/=item(k))

This essentially says that the item retrieved must be equal to the item inserted, however, the test can only be applied if 'v' is comparable in equality (and we check that the returned value was just as non-comparable).  The new code is only executed in the case where the old condition fails (only with v7 and only with QNAN) so it should not be onerous.

You may well wonder if the C compiler will optimize 'v/=v' into 'false'.  It does in v6 but not in v7 (probably because Microsoft has realized that this would be a mistake with QNAN).  However, if some combination of optimization flags does turn up, some alternate test could be devised like 'v/=clone(v)'.

Alternatively, you could make a function that performs a bitwise compare:

	insertion_done: bitwise_equal(item (k), v)
or perhaps:
	insertion_done: v.bitwise_equal(item (k))		-- What if 'v' is Void?

The function 'bitwise_equal' (in ANY) would be implemented as '==' in C for everything except REAL and DOUBLE.

Notice that the true meaning of all of this is that DOUBLE should not inherit from COMPARABLE!  However, I don't think you will want to go that far.

			Randy and Mark

p.s.  Note that if the FPP is set to trap on invalid operations (not the default on W2K) then any comparison of a QNAN (even with itself) will trap (at the next floating point operation).  People will just have to make sure to mask this exception when 'ensure' is on if they want to use 'put'.

p.p.s.  Although we do not use IEEE on VMS/Alpha, the behavior of equality for QNAN is the same but the optimizer would be a problem.


	QNAN : DOUBLE is
	-- Quiet Not-A-Number.  When used in an expression, the result is QNAN.
	local
		string : STRING
		l_area : ANY
	once
		string := "12345678"
		string.put('%/0/', 1)
		string.put('%/0/', 2)
		string.put('%/0/', 3)
		string.put('%/0/', 4)
		string.put('%/0/', 5)
		string.put('%/0/', 6)
		string.put('%/248/', 7)
		string.put('%/127/', 8)
		l_area := string.area
		copy_from_pointer($Result, $l_area, 8)
	end

   copy_from_pointer(target_:POINTER; source_:POINTER; length:INTEGER) is
	  external
		 "C"
	  alias
		 "memcpy"
	  end

State-Changed-From-To: open-open
State-Changed-By: Manu
State-Changed-When: Sun Sep 16 15:17:16 PDT 2001
State-Changed-Why:

Dear Randy,

I've been reading a few things about NaN and I'm not sure we should
fix the post-condition violation. I've learned that because NaN values
are unordered, they are not comparable. And thus if you really want to
keep those values it does not make much sense, but since I don't know
the background of your application I don't know how you are using them

It makes sense to store infinity values since they compare.

Also you solution to change INDEXABLE is not complete. They are so many
post-condition of the style: v = new_value where new_value can be a
NAN that we should do it everywhere and it does not become nice.

Another solution is to let the compiler treat `v = new_value' for doubles in the way you described, but I would say it will translate it
into:

 v = new_value <=> (is_nan (v) and is_nan (new_value)) || (v = new_value)

That way every where we compare 2 doubles we get
....
Output truncated, Click download to get the full message