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

← 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)

Peter gummer: /* three_way_comparison */

2007-05-09T03:51:47Z

three_way_comparison

← 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...)

Juliant: /* three_way_comparison */

2006-11-27T18:21:11Z

three_way_comparison

← 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...)

Juliant: /* three_way_comparison */

2006-11-27T17:16:05Z

three_way_comparison

← Older revision		Revision as of 17:16, 27 November 2006
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 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.		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.

			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.

Juliant: /* inherited invariants */

2006-11-27T17:08:47Z

inherited invariants

← Older revision		Revision as of 17:08, 27 November 2006
Line 20:		Line 20:
	===inherited invariants===		===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===		===three_way_comparison===

Juliant: /* inherited invariants */

2006-11-27T16:53:10Z

inherited invariants

← Older revision		Revision as of 16:53, 27 November 2006
Line 20:		Line 20:
	===inherited invariants===		===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.		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.

	===three_way_comparison===		===three_way_comparison===

Juliant: /* three_way_comparison */

2006-11-23T00:01:27Z

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.

Juliant at 19:40, 22 November 2006

2006-11-22T19:40:11Z

← 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.

Juliant at 22:00, 17 November 2006

2006-11-17T22:00:07Z

← 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.

Juliant at 21:27, 17 November 2006

2006-11-17T21:27:04Z

← Older revision		Revision as of 21:27, 17 November 2006
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.		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===		===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.