REAL 64 (issues) - Revision history

Colin-adams: Mark Howard's proposal for dealing with NaNs

2007-09-18T06:55:02Z

Mark Howard's proposal for dealing with NaNs

Peter gummer: /* three_way_comparison */

2007-05-09T03:51:47Z

‎three_way_comparison

Juliant: /* three_way_comparison */

2006-11-27T18:21:11Z

‎three_way_comparison

Juliant: /* three_way_comparison */

2006-11-27T17:16:05Z

‎three_way_comparison

Juliant: /* inherited invariants */

2006-11-27T17:08:47Z

‎inherited invariants

Juliant: /* inherited invariants */

2006-11-27T16:53:10Z

‎inherited invariants

Juliant: /* three_way_comparison */

2006-11-23T00:01:27Z

‎three_way_comparison

Juliant at 19:40, 22 November 2006

2006-11-22T19:40:11Z

Juliant at 22:00, 17 November 2006

2006-11-17T22:00:07Z

Juliant at 21:27, 17 November 2006

2006-11-17T21:27:04Z

← Older revision		Revision as of 06:55, 18 September 2007
Line 32:		Line 32:

	The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is already an object which is a COMPARABLE but cannot be compared...)		The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is already an object which is a COMPARABLE but cannot be compared...)
		+
		+	===A suggestion from Mark Howard===
		+
		+	Mark Howard has told me that his idea to solve the NaN problem is to prefix assertions with "x=x implies ...". This works regardless of the type of object involved, so it is particularly useful in postconditions of routines such as extend.
		+	This does not help for infinities, but I would have thought that this should be tackled by an is_infinite query in NUMERIC.
		+	--[[User:Colin-adams\|Colin-adams]] 08:55, 18 September 2007 (CEST)

← Older revision		Revision as of 03:51, 9 May 2007
Line 31:		Line 31:
	In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE.		In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE.

−	The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is ~~alredy~~ an object which is a COMPARABLE but cannot be compared...)	+	The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is already an object which is a COMPARABLE but cannot be compared...)

← Older revision		Revision as of 18:21, 27 November 2006
Line 30:		Line 30:

	In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE.		In the C# implementation the return value of a three way comparison involving NaN returns always that NaN is smaller compared to any other real value except with NaN itself where it is equal. But when using the comparison operators, NaN compared to any other value is false. Thus this solution cannot be used to uphold the current contract from COMPARABLE.
		+
		+	The cleanest solution would be to introduce an 'is_special_case' feature in COMPARABLE like the one in NUMERIC. That way we could make the contract conditional on this feature. The downside is that you introduce COMPARABLE objects which are not comparable! (Although NaN is alredy an object which is a COMPARABLE but cannot be compared...)

@@ Line 26: / Line 26: @@
 The postcondition of ''three_way_comparison'' is violated in the case where one object is infinity and the other object is NaN:
-The postcondition lists the three cases of ''three_way_comparison''. In the case where one of the two comparables is NaN and the other is INF, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to infinity. What return value should be used is yet unclear.
+The postcondition lists the three cases of ''three_way_comparison''. In the case where one of the two comparables is NaN, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to any other real value (including itself). What return value should be used is yet unclear.
 To uphold the contract it would be sufficent to return any number not equal to -1, 0 or 1. But this is more of a hack than a solution.

@@ Line 20: / Line 20: @@
 ===inherited invariants===
-Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_special_case' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not exceptional.
+Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_special_case' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not a special case.
 ===three_way_comparison===

← Older revision		Revision as of 00:01, 23 November 2006
Line 27:		Line 27:

	The postcondition lists the three cases of ''three_way_comparison''. In the case where one of the two comparables is NaN and the other is INF, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to infinity. What return value should be used is yet unclear.		The postcondition lists the three cases of ''three_way_comparison''. In the case where one of the two comparables is NaN and the other is INF, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to infinity. What return value should be used is yet unclear.
		+	To uphold the contract it would be sufficent to return any number not equal to -1, 0 or 1. But this is more of a hack than a solution.

← Older revision		Revision as of 19:40, 22 November 2006
Line 21:		Line 21:

	Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_exceptional' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not exceptional.		Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_exceptional' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not exceptional.
		+
		+	===three_way_comparison===
		+
		+	The postcondition of ''three_way_comparison'' is violated in the case where one object is infinity and the other object is NaN:
		+
		+	The postcondition lists the three cases of ''three_way_comparison''. In the case where one of the two comparables is NaN and the other is INF, all three cases are violated. Thus the returning value should neither be -1, 0 or 1. Currently in this case 0 is returned which then violates the contract since NaN is not equal to infinity. What return value should be used is yet unclear.

← Older revision		Revision as of 22:00, 17 November 2006
Line 17:		Line 17:

	By providing NaN and INF every real value can be divided by every other real value. Thus a call of 'divisible' should always return true or the precondition of the division should be changed. This arises again in INTEGER.infix "/". A call to 12 / 0 is not allowed by the current contract but should just return INF.		By providing NaN and INF every real value can be divided by every other real value. Thus a call of 'divisible' should always return true or the precondition of the division should be changed. This arises again in INTEGER.infix "/". A call to 12 / 0 is not allowed by the current contract but should just return INF.
		+
		+	===inherited invariants===
		+
		+	Some of the invariants which are inherited from NUMERIC are not applicable if the REAL is eithern NaN or INF. To circumvent this problem we could introduce a 'is_exceptional' feature into NUMERIC and change the invariants form NUMERIC to be only true if the object is not exceptional.

@@ Line 12: / Line 12: @@
 Currently when doing a 'floor', 'ceiling', 'rounded' or 'truncate_to_integer' with a number which is too large (e.g. 2^31) the result is {INTEGER}.min_value.
-The change in the sign is a not expected behavior and violates (informal) contracts.
+The change in the sign is a not expected behavior and violates informal contracts (see comments in EiffelBase REAL_64_REF.truncated_to_integer).
 ===divisible===
-By providing NaN and INF every real value can be divided by every other real value. Thus a call of 'divisible' should always return true. This arises again in INTEGER.infix "/". A call to 12 / 0 is not allowed by the current contract but should just return INF.
+By providing NaN and INF every real value can be divided by every other real value. Thus a call of 'divisible' should always return true or the precondition of the division should be changed. This arises again in INTEGER.infix "/". A call to 12 / 0 is not allowed by the current contract but should just return INF.