From c5c596bf432274222415e1758a552c07cbd5a45b Mon Sep 17 00:00:00 2001 From: halw Date: Fri, 15 Jul 2011 22:02:00 +0000 Subject: [PATCH] Added more detail on controlled/uncontrolled assertions. Author:halw Date:2011-07-15T22:02:00.000000Z git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@941 abb3cda0-5349-4a8f-a601-0c33ac3a8c38 --- .../concurrent-computing/concurrent-eiffel-scoop/index.wiki | 2 ++ 1 file changed, 2 insertions(+) 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 c764320b..711a66dc 100644 --- a/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki +++ b/documentation/current/solutions/concurrent-computing/concurrent-eiffel-scoop/index.wiki @@ -242,6 +242,8 @@ In concurrent Eiffel, the same correctness conditions are still valid, but there {{definition|Controlled/uncontrolled 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'''. }} +So, the determination of whether a particular precondition or postcondition clause is controlled or uncontrolled depends upon the context of the calling routine. That means that a particular clause on feature f might be considered controlled when f is called by one caller, but uncontrolled when called by a different caller. + Uncontrolled precondition clauses demand an adaptation of precondition semantics: {{Info|A violation of a '''controlled precondition clause''' will cause an exception in the caller as soon as the violation is detected. A violation of an '''uncontrolled precondition clause''' does not result in an exception in the caller. Rather, the feature application waits to execute until such time as the precondition clause holds. }}