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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.28.135 with SMTP id b7mr7721307pbh.8.1322131771741; Thu, 24 Nov 2011 02:49:31 -0800 (PST) Path: lh20ni12432pbb.0!nntp.google.com!news1.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newspeer1.nac.net!newsfeed.xs4all.nl!newsfeed6.news.xs4all.nl!xs4all!feeds.phibee-telecom.net!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!usenet-fr.net!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 24 Nov 2011 11:49:30 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <1ecuhb030iugz.4q1hfjx371xa.dlg@40tude.net> <4ecc393d$0$7625$9b4e6d93@newsspool1.arcor-online.net> <124aq618dmove.884jj64mzm6w$.dlg@40tude.net> <1jxx617mf2cqf$.1j076axdq83mr$.dlg@40tude.net> <1cjufyo57vlpg$.11kf45cs5vnb7.dlg@40tude.net> In-Reply-To: Message-ID: <4ece213a$0$6629$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 24 Nov 2011 11:49:30 CET NNTP-Posting-Host: 82edcb75.newsspool2.arcor-online.net X-Trace: DXC=\f?;1F5>0SP@>[RYkFXOIPA9EHlD;3YcR4Fo<]lROoRQ8kFejVXlBkIO^noWbS?3I;eHSC4=\ X-Complaints-To: usenet-abuse@arcor.de Xref: news1.google.com comp.lang.ada:19109 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2011-11-24T11:49:30+01:00 List-Id: On 24.11.11 10:27, Dmitry A. Kazakov wrote: > On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote: > >> To take Georg's example of the stack, I don't see how you're going to >> express the fact that its capacity is bounded other than by comments >> about constraint errors or by preconditions. > > The point is that when this behavior can be expressed I hate to go on when we have a summary by Stefan Lucks but two more issues: Maybe there isn't that much of a disagreement, if we can fake the choice by replacing it with a choice of style; notably, a project may require that pre => True post => May_Raise be the only conditionals allowed. Then, programmers of clients should be ready to handle failures. This choice still doesn't restrict Ada contracts to get all the flexibility of statically checked expressions, but is closer to exceptions only, I'd think. The notions are not ones of behavior, just like debugging statements, but rather more simple, and specifically intended to be only guiding the creation of behavioral aspects of the program proper: Like in the example given in [1], programmers are supposed to write bodies so that the conditionals given in pre/post/inv are meaningful. This is their contractual obligation. A precondition of the form T'Valid (Some_Input) is inappropriate if the body doesn't actually implement its meaning, since assertions do *not* count as program behavior. Note that I am saying "they do not count", and not saying "they do not result in behavior": it does not matter that in some circumstances they are supposed to result in behavior, for example, during testing. The capacity of a stack can be a trivial Type_Invariant if the size is a type constraint. There will be less silly scenarios than these, but nevertheless: procedure Stacking (N: Positive) is type T is (One, Two, Three); package Local_Stacks is type Stack (Capacity : Natural) is tagged private with Type_Invariant => (Stack.Capacity = N and True); -- etc. private ... end Local_Stacks; package body Local_Stacks is separate; S1 : Local_Stacks.Stack (N); -- o.K. S2 : Local_Stacks.Stack (42); -- raises when 42 /= N and pramga Assertion_Policy (Check); begin null; end Stacking; > A dynamic precondition does not express anything, Well, frankly, any expression demonstrably expresses something, because an Ada compiler can and will assign meaning to all constituent parts of the expression. The expression does not necessarily have a Boolean value at compile time, but it certainly isn't void of meaning. As per intent. Programmers also assign meaning to expressions in assertions of the contract. > SPARK does it right, Eiffel and now Ada do it wrong. > > If correctness cannot be proved > statically, then the requirement expressed by the precondition must be > considered as not satisfied. We may state our assumptions and have them checked, or we may state our assumptions and perform the checks ourselves, before runtime, statically. Like when showing that for a stack object, the sequence (not Is_Full, Push, Pop) is a safe sequence, ceteris paribus. That is, safe in terms of the contract, ignoring hardware failures, ignoring a breach of contract in the stack's bodies. Since, normally, any of these can be true, one may prepare for failure. But! There is no need for the sequence of calls to be changed in order to handle failures! Is is a correct sequence. This style just seems more expressive than "raise Constraint_Error" without indication of possible causes, when some are in fact known, and expressed as assertions, before compile time! I am not so sure that programmers are fooling themselves into thinking that adding descriptive assertions somehow makes a program automatically correct. It only helps with this effort. __ [1] http://www2.adacore.com/wp-content/uploads/2006/03/Ada2012_Rational_Introducion.pdf Page 2, on the right.