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

Removed postcondition semantics description. This description had been true in other SCOOP implementations and descriptions, but does not apply to the current Eiffel Software implementation. A correct description needs to be provided.

Browse Source 
Author:halw
Date:2012-03-31T18:19:32.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@1056 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2012-03-31 18:19:32 +00:00
parent 62dabe50d0
commit dacc83d220
1 changed files with 0 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -255,10 +255,6 @@ As with preconditions the effect of concurrent execution can make a difference i
If a routine has executed correctly, then the postcondition of the routine will hold at the time that it terminates ... this is true whether or not concurrency is involved. However, when a postcondition involves separate calls or entities are involved, clients must be cautious about how they depend upon the state guaranteed by postconditions. If a routine has executed correctly, then the postcondition of the routine will hold at the time that it terminates ... this is true whether or not concurrency is involved. However, when a postcondition involves separate calls or entities are involved, clients must be cautious about how they depend upon the state guaranteed by postconditions.
Postcondition semantics are characterized as follows:
:If a called routine has a postcondition clause that is controlled, then a client can assume that clause holds, because no other client can affect it. However, a client cannot make the same assumption for uncontrolled postcondition clauses. Uncontrolled queries in postcondition clauses are evaluated by the processors of their targets. And this is done asynchronously. Wait by necessity does not apply. So, the case of uncontrolled queries in postcondition clauses is an exception to case S2.1 in the section about [[#What makes a call synchronous or asynchronous?|synchronous and asynchronous calls]], above.
===Class invariants=== ===Class invariants===