From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Contracts for protected objects: internal call cannot appear in
 precondition of protected operation
Date: Thu, 28 May 2020 21:11:45 -0500
Organization: JSA Research & Innovation
Message-ID: <rapr13$673$1@franka.jacob-sparre.dk>
References: <4ed8fa1e-0b4d-4d6b-bc36-0236f6965db0@googlegroups.com>
Injection-Date: Fri, 29 May 2020 02:11:47 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="6371"; mail-complaints-to="news@jacob-sparre.dk"
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246
Xref: reader01.eternal-september.org comp.lang.ada:58813
Date: 2020-05-28T21:11:45-05:00
List-Id: <comp.lang.ada>

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