From 05828911b18cb95f38c734fb4835c3740d0c821b Mon Sep 17 00:00:00 2001 From: halw Date: Wed, 13 Jul 2011 21:46:56 +0000 Subject: [PATCH] Tweak definition of Controlled assertion. Author:halw Date:2011-07-13T21:46:56.000000Z git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@934 abb3cda0-5349-4a8f-a601-0c33ac3a8c38 --- .../concurrent-computing/concurrent-eiffel-scoop/index.wiki | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki b/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki index 8182b73f..c3b43472 100644 --- a/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki +++ b/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki @@ -239,7 +239,7 @@ The role of the precondition is somewhat different in SCOOP than in sequential E In concurrent Eiffel, the same correctness conditions are still valid, but there are cases in which we must view the clients role here a little differently. In the case of a precondition clause that depends upon a separate object, even if the client tests the condition ahead of the call, there is no assurance that action by some other concurrent processor may have invalidated the precondition clause between the time that the check was made and the time that the feature application takes place. So, the client cannot be held responsible establishing that this clause holds. This type of precondition clause is called an '''uncontrolled precondition clause'''. -{{definition|Controlled assertion (precondition or postcondition) clause| A precondition or postcondition clause for a feature f is controlled if, after substitution of actual arguments for formal arguments, f involves only calls on entities which are controlled in the context of routine in which f is called. Otherwise it is an '''uncontrolled assertion (precondition or postcondition) clause'''. }} +{{definition|Controlled assertion (precondition or postcondition) clause| A precondition or postcondition clause for a feature f is controlled if, after substitution of actual arguments for formal arguments, f involves only calls on entities which are controlled in the context of the routine which is the caller of f. Otherwise it is an '''uncontrolled assertion (precondition or postcondition) clause'''. }} Uncontrolled precondition clauses demand an adaptation of precondition semantics: