Re: Contracts for protected objects: internal call cannot appear in precondition of protected operation

["Randy Brukardt" <randy@rrsoftware.com>]

That's not allowed, as it would require extra mutual exclusion. Since that 
exclusion would have to be separate from the protected action (necessary 
since the entry may not be open when the call is made), you'd also have a 
race condition (the precondition could be evaluated with one value, the 
value then changed, and then later the entry accepted). Best practices is 
always that preconditions should only depend on the parameters to a call 
(regardless of the kind of call involved).

                        Randy.


"reinert" <reinkor@gmail.com> wrote in message 
news:4ed8fa1e-0b4d-4d6b-bc36-0236f6965db0@googlegroups.com...
> Hello,
>
> I tried to use pre-conditions for an entry in a protected object.
> Say (in the specification):
>
>   entry E1 with Pre => test1;
>
> This seems OK when test1 is external (defined outside the protected 
> object).
>
> However, when test1 is defined inside the protected object, I get:
>
> internal call cannot appear in precondition of protected operation
>
> (I assume this is related to avoid deadlock - but testing from outside
> here should not give deadlock?)
>
> I also would like to include (for security) a test on a variable
> defined in the private part of the protected object). Anyhow possible?
> I do not mange to include pre/post conditions in the body of my
> protected object. I missed something?
>
> reinert