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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.226.10 with SMTP id ro10mr1742539pbc.6.1328177080680;
        Thu, 02 Feb 2012 02:04:40 -0800 (PST)
X-FeedAbuse: http://nntpfeed.proxad.net/abuse.pl feeded by 88.191.131.2
Path: 
 lh20ni251721pbb.0!nntp.google.com!news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!nntpfeed.proxad.net!88.191.131.2.MISMATCH!news.chainon-marquant.org!usenet.pasdenom.info!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?=
 =?UTF-8?B?Pw==?=
Date: Thu, 2 Feb 2012 11:04:00 +0100
Organization: cbb software GmbH
Message-ID: <1j53ptti2a3li.e4igtda1zawb$.dlg@40tude.net>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net>
 <4f27b5e8$0$6628$9b4e6d93@newsspool2.arcor-online.net>
 <19jyp0vyqkcop$.6oatj9p6pcp1$.dlg@40tude.net>
 <4f27dfa5$0$6570$9b4e6d93@newsspool4.arcor-online.net>
 <12pod8zxdo56v.16pnewlc853au$.dlg@40tude.net>
 <4f280a00$0$6583$9b4e6d93@newsspool3.arcor-online.net>
 <r176484qtwsf.ia6ftfe1d5kh$.dlg@40tude.net>
 <4f284488$0$6634$9b4e6d93@newsspool2.arcor-online.net>
 <1wn5azarpihb1.13g4tvu7fddve.dlg@40tude.net>
 <Pine.LNX.4.64.1202011054270.26654@medsec1.medien.uni-weimar.de>
 <k4q0w3hid5t6$.12146xli5l156$.dlg@40tude.net>
 <Pine.LNX.4.64.1202011604270.29918@medsec1.medien.uni-weimar.de>
 <oxvm5rgonh77$.135nqc7uxq9wr$.dlg@40tude.net>
 <Pine.LNX.4.64.1202021002060.7297@medsec1.medien.uni-weimar.de>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-02-02T11:04:00+01:00
List-Id: <comp.lang.ada>

On Thu, 2 Feb 2012 10:18:03 +0100, stefan-lucks@see-the.signature wrote:

> On Thu, 2 Feb 2012, Dmitry A. Kazakov wrote:
> 
>>>   procedure Ask_Database(U: User; Q: Query; R: out Response)
>>>     with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
>>>               then R=Empty_Response);
>> 
>> BTW, contracts to be stated in terms of equivalence rather than
>> implications. I.e.
>> 
>>    R=Empty_Response <=> not Authorized(U)) or ...
> 
> Why?
> 
> These implications are what you would typically find in a security 
> requirements specification. (In human-readable way, such as "if an 
> unauthorized user asks for any confidential data, no answer is provided by 
> the XY system.")

And conversely, if no answer is provided, then the user was not authorized
to get it. And furthermore, the data the user gets is the data he asked for
and so on.

> What is the point of rewriting this in terms of equivalence? You run the 
> trouble of proving that your rewritten contract is logically equivalent to 
> the requirements specification. (Or you risk proving your program correct 
> with respect to an incorrect spec.)

You must translate the above into some specifications of some modules
anyway.

If a module has an output, the meaning of that output is the set of
propositions provable with the output value:

   Get_Line = 'a' |= the user typed 'a'

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de