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 ro10mr1630605pbc.6.1328174181307;
        Thu, 02 Feb 2012 01:16:21 -0800 (PST)
Path: 
 lh20ni251610pbb.0!nntp.google.com!news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail
From: stefan-lucks@see-the.signature
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?=
 =?UTF-8?B?Pw==?=
Date: Thu, 2 Feb 2012 10:18:03 +0100
Organization: Bauhaus-Universitaet Weimar
Message-ID: <Pine.LNX.4.64.1202021002060.7297@medsec1.medien.uni-weimar.de>
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>
Reply-To: stefan-lucks@see-the.signature
NNTP-Posting-Host: medsec1.medien.uni-weimar.de
Mime-Version: 1.0
X-Trace: tigger.scc.uni-weimar.de 1328174181 17676 141.54.178.228 (2 Feb 2012
 09:16:21 GMT)
X-Complaints-To: news@tigger.scc.uni-weimar.de
NNTP-Posting-Date: Thu, 2 Feb 2012 09:16:21 +0000 (UTC)
X-X-Sender: lucks@medsec1.medien.uni-weimar.de
In-Reply-To: <oxvm5rgonh77$.135nqc7uxq9wr$.dlg@40tude.net>
Content-Type: TEXT/PLAIN; charset=US-ASCII
Date: 2012-02-02T10:18:03+01:00
List-Id: <comp.lang.ada>

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.")

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.)

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------