Covariance-aware assertions - Revision history

Conaclos: syntax updated

2013-05-20T10:41:55Z

syntax updated

← Older revision		Revision as of 10:41, 20 May 2013
Line 17:		Line 17:
	feature		feature

	f (x: ? ANY)		f (x: detachable ANY)
	do		do
	ensure		ensure
Line 33:		Line 33:
	feature		feature

	f (x: ? STRING)		f (x: detachable STRING)
	do		do
	end		end
Line 48:		Line 48:

	<e>		<e>
	f (x: ? STRING)		f (x: detachable STRING)
	ensure -- From A		ensure -- From A
	(~~{y: STRING}~~ x) and then (True)		(attached x and then (True)
	</e>		</e>

Line 106:		Line 106:
	feature		feature

	g (x: ? STRING)		g (x: detachable STRING)
	do		do
	if {y~~: STRING} x~~ then		if attached x as y then
	-- Do something with y		-- Do something with y
	else		else
Line 145:		Line 145:

	* Normal assertion: <e>True</e>		* Normal assertion: <e>True</e>
	* Covariant-aware assertion: <e>~~({y: STRING}~~ x) implies (True)</e>		* Covariant-aware assertion: <e>attached x implies (True)</e>

	== Possible solutions ==		== Possible solutions ==

Manus: Added category

2007-05-30T18:40:53Z

Added category

← Older revision		Revision as of 18:40, 30 May 2007
Line 1:		Line 1:
			[[Category:ECMA]]
	ECMA Eiffel introduces covariance-aware assertions (section 8.10.4)). This is a change in assertions when covariant redefinition of feature argument occurs.		ECMA Eiffel introduces covariance-aware assertions (section 8.10.4)). This is a change in assertions when covariant redefinition of feature argument occurs.

Juliant: /* Unsatisfiable postcondition on catcalls */

2007-04-23T15:19:55Z

Unsatisfiable postcondition on catcalls

← Older revision		Revision as of 15:19, 23 April 2007
Line 141:		Line 141:
	The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).		The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).

	~~The question here~~ is~~, if we want~~ to ~~allow catcalls at all. Should they go through then~~ the ~~programmer has to check them~~ with an ~~object test (which does not work~~ if ~~Void is~~ passed~~), or should an exception be triggered by~~ the ~~runtime system. In~~ the ~~second case it surely should not be a postcondition violation~~.		This problem can be solved by changing the <e>and then</e> which is used to combine the object test and the original assertion with an <e>implies</e> clause. That way, if wrong arguments are passed the assertion will evaluate to <e>True</e> no matter what and won't affect the contract anymore. The new assertion would look like this:

			* Normal assertion: <e>True</e>
			* Covariant-aware assertion: <e>({y: STRING} x) implies (True)</e>

	== Possible solutions ==		== Possible solutions ==

Juliant: /* Possible solutions */

2007-04-23T15:15:45Z

Possible solutions

← Older revision		Revision as of 15:15, 23 April 2007
Line 147:		Line 147:
	To solve the first problem shown - when a valid Void argument is passed the covariance-aware assertion fails - the rules to create covariance-aware assertions have to be changed to take detachable arguments into account and allow the valid use of Void arguments.		To solve the first problem shown - when a valid Void argument is passed the covariance-aware assertion fails - the rules to create covariance-aware assertions have to be changed to take detachable arguments into account and allow the valid use of Void arguments.

	To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules ~~also have to~~ be changed ...		To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules can be changed to use an <e>implies</e> rather than and <e>and then</e> clause to combine the object test with the original assertion.
	~~{{Todo\|changed to what?}}~~

	== Catcalls in general ==		== Catcalls in general ==

Peter gummer: /* Unsatisfiable postcondition on catcalls */

2007-04-23T08:46:56Z

Unsatisfiable postcondition on catcalls

← Older revision		Revision as of 08:46, 23 April 2007
Line 141:		Line 141:
	The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).		The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).

	The question here is, if we want to allow catcalls at all. Should they go ~~trough~~ then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.		The question here is, if we want to allow catcalls at all. Should they go through then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.

	== Possible solutions ==		== Possible solutions ==

Peter gummer: /* Unsatisfiable postcondition on catcalls */

2007-04-23T08:45:21Z

Unsatisfiable postcondition on catcalls

← Older revision		Revision as of 08:45, 23 April 2007
Line 119:		Line 119:
	</e>		</e>

	The argument ~~get's~~ detached, and any meaningful code in the redefined feature has to check for the type of the argument.		The argument gets detached, and any meaningful code in the redefined feature has to check for the type of the argument.

	But again, the inherited assertion goes through the process to become covariance-aware:		But again, the inherited assertion goes through the process to become covariance-aware:

Juliant: /* Catcalls in general */

2007-04-23T01:21:12Z

Catcalls in general

← Older revision		Revision as of 01:21, 23 April 2007
Line 157:		Line 157:
	* If catcalls have to be detected statically, the whole mechanism of redefining detachable is not necessary anyway and covariance-aware assertions have to be revised.		* If catcalls have to be detected statically, the whole mechanism of redefining detachable is not necessary anyway and covariance-aware assertions have to be revised.
	* If catcalls should be handled dynamically, there are two ways to do so:		* If catcalls should be handled dynamically, there are two ways to do so:
	** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call]] for an argument against this). Problems ~~are raised~~ with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.		** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call]] for an argument against this). Problems arise with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.
	** The program raises an exception on a catcall. If an exception should be raised, this better be the case on the entry to the call and not in the postcondition. So a runtime check could be introduced on any problematic feature call and raise an exception. This would also imply that the mechanism of redefining covariant features detachable is not necessary anymore since the runtime guarantees that all arguments are valid.		** The program raises an exception on a catcall. If an exception should be raised, this better be the case on the entry to the call and not in the postcondition. So a runtime check could be introduced on any problematic feature call and raise an exception. This would also imply that the mechanism of redefining covariant features detachable is not necessary anymore since the runtime guarantees that all arguments are valid.

Juliant: /* Catcalls in general */

2007-04-23T01:20:41Z

Catcalls in general

← Older revision		Revision as of 01:20, 23 April 2007
Line 157:		Line 157:
	* If catcalls have to be detected statically, the whole mechanism of redefining detachable is not necessary anyway and covariance-aware assertions have to be revised.		* If catcalls have to be detected statically, the whole mechanism of redefining detachable is not necessary anyway and covariance-aware assertions have to be revised.
	* If catcalls should be handled dynamically, there are two ways to do so:		* If catcalls should be handled dynamically, there are two ways to do so:
	** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call~~\|this~~]] ~~page~~ for an argument against this). Problems are raised with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.		** The program does not raise an exception on a catcall. In this case the programmer has to do an object-test to use covariantly redefined features (See also [[New CAT call]] for an argument against this). Problems are raised with the covariance-aware assertions and their rules have to be changed not to invalidate postconditions in all cases.
	** The program raises an exception on a catcall. If an exception should be raised, this better be the case on the entry to the call and not in the postcondition. So a runtime check could be introduced on any problematic feature call and raise an exception. This would also imply that the mechanism of redefining covariant features detachable is not necessary anymore since the runtime guarantees that all arguments are valid.		** The program raises an exception on a catcall. If an exception should be raised, this better be the case on the entry to the call and not in the postcondition. So a runtime check could be introduced on any problematic feature call and raise an exception. This would also imply that the mechanism of redefining covariant features detachable is not necessary anymore since the runtime guarantees that all arguments are valid.

Juliant: /* Possible solutions */

2007-04-23T01:19:06Z

Possible solutions

← Older revision		Revision as of 01:19, 23 April 2007
Line 147:		Line 147:
	To solve the first problem shown - when a valid Void argument is passed the covariance-aware assertion fails - the rules to create covariance-aware assertions have to be changed to take detachable arguments into account and allow the valid use of Void arguments.		To solve the first problem shown - when a valid Void argument is passed the covariance-aware assertion fails - the rules to create covariance-aware assertions have to be changed to take detachable arguments into account and allow the valid use of Void arguments.

	To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules also have to be changed ... (Todo: changed to what?)		To solve the second problem shown - on a catcall the postcondition is violated in every case - the rules also have to be changed ...
			{{Todo\|changed to what?}}

	== Catcalls in general ==		== Catcalls in general ==

Seilerm: /* Unsatisfiable postcondition on catcalls */

2007-04-22T19:04:21Z

Unsatisfiable postcondition on catcalls

← Older revision		Revision as of 19:04, 22 April 2007
Line 141:		Line 141:
	The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).		The covariance-aware postcondition again evaluates to <e>False</e>, no matter what the feature does. Thus in case of a cat-call the postcondition is violated in every case. Even in the case where <e>Void</e> is passed legally, the postcondition is violated (as described in the previous section).

	The question here is, if we want to allow catcalls at all. Should they go trough ~~than~~ the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.		The question here is, if we want to allow catcalls at all. Should they go trough then the programmer has to check them with an object test (which does not work if Void is passed), or should an exception be triggered by the runtime system. In the second case it surely should not be a postcondition violation.


	== Possible solutions ==		== Possible solutions ==