m formatting.

Author:halw
Date:2011-07-14T22:56:22.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@940 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2011-07-14 22:56:22 +00:00
parent 181463e881
commit f2c443d15e

View File

@@ -164,7 +164,7 @@ Because the argument <code>my_separate_argument</code> is of a separate type, th
Valid targets for separate calls, like <code>a_arg</code> in <code>enclosing_routine</code> above are said to be ''controlled''.
{{definition|Controlled expression|An expression is '''controlled''' if it is attached and either:<br/>1) It is of a non-separate type<br/>2) It is of a separate type and it is handled by the same processor as one of the separate arguments to the enclosing routine.<br/>Otherwise it is '''uncontrolled'''.}}
{{definition|Controlled/uncontrolled expression|An expression is '''controlled''' if it is attached and either:<br/>1) It is of a non-separate type<br/>2) It is of a separate type and it is handled by the same processor as one of the separate arguments to the enclosing routine.<br/><br/>Otherwise it is '''uncontrolled'''.}}
What the definition of ''controlled expression'' means is that such an expression is controlled with respect to the processor handling the context in which the expression is used (the current context) ... and that means that all objects necessary to the expression are under control of (locked for exclusive access by) the current processor and cannot be modified by other processors.
@@ -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 an [[Concurrent Eiffel with SCOOP#Controlled expressions|uncontrolled]] 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 <code>f</code> is controlled if, after substitution of actual arguments for formal arguments, <code>f</code> involves only calls on entities which are controlled in the context of the routine which is the caller of <code>f</code>. Otherwise it is an '''uncontrolled assertion (precondition or postcondition) clause'''. }}
{{definition|Controlled/uncontrolled assertion''' (precondition or postcondition) '''clause| A precondition or postcondition clause for a feature <code>f</code> is controlled if, after substitution of actual arguments for formal arguments, <code>f</code> involves only calls on entities which are controlled in the context of the routine which is the caller of <code>f</code>. <br/><br/>Otherwise it is an '''uncontrolled assertion''' (precondition or postcondition) '''clause'''. }}
Uncontrolled precondition clauses demand an adaptation of precondition semantics: