mirrors/eiffel-org
1
0
Fork 0
mirror of https://github.com/EiffelSoftware/eiffel-org.git synced 2025-12-07 15:22:31 +01:00
Code Issues Packages Projects Releases Wiki Activity

Added "uncontrolled" to explanation of preconditions.

Browse Source 
Author:halw
Date:2011-07-14T22:41:59.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@938 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2011-07-14 22:41:59 +00:00
parent e5cad2d741
commit e88ffebbeb
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki
View File

@@ -237,7 +237,7 @@ The backbone of the Eiffel Method is design by contract. Preconditions, postcond
The role of the precondition is somewhat different in SCOOP than in sequential Eiffel. In non-concurrent Eiffel we view the precondition of a routine as defining a set of obligations on potential callers of the routine. That is, the set of conditions that must be true before correct execution of the routine can be expected. So, we could look at the precondition clauses in sequential Eiffel as '''correctness conditions'''. A typical example might be a square root routine that returns the square root of a passed argument value. A precondition clause, i. e., a correctness condition, for this routine will be that the argument must be non-negative. It is the responsibility of the caller to ensure that this property of the argument holds at the time of the feature call.
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'''.
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'''. }}