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=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!212.27.60.9.MISMATCH!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 13 May 2010 04:03:38 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.1.9) Gecko/20100317 Thunderbird/3.0.4 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions References: <87mxw9x7no.fsf@ludovic-brenta.org> <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net> <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net> <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> <4beaf93a$0$6875$9b4e6d93@newsspool2.arcor-online.net> <1u6ficvfjfreg$.16cmwyau8jkd9.dlg@40tude.net> In-Reply-To: <1u6ficvfjfreg$.16cmwyau8jkd9.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4beb5dfa$0$6883$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 13 May 2010 04:03:39 CEST NNTP-Posting-Host: 1ebd18ec.newsspool2.arcor-online.net X-Trace: DXC=M^R`c=mOH_`UoRk[hk2WalA9EHlD;3Ycb4Fo<]lROoRa8kFejVh0SG?TmjlX_eoE7< On 5/12/10 11:57 PM, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > >> On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> >>>> Being better is precisely the point (of DbC). >>>> DbC talks about proof obligations, not about provability. >>> >>> Who is obliged to whom in what? >> >> By being a programmer subscribing to the principles of DbC, >> you are obliged to show that the components of your system >> obey the components' contracts. The compiler and run-time >> try to help you achieving this goal. > > A C programmer would tell you same story about merits of pointers, casts > and preprocessor. All of these features of C have merits besides what else they may have. But they sure don't warrant dismissing DbC? A C programmer is "right" when he tells an *analogous* story that competent C programmers will avoid typical mistakes by correct use of C features. ... whenever a competent C programmer is defined to be one who avoids these mistakes... A C programmer's tool set is difficult to use for correct, portable programs. For example, ADTs are mostly emulated via style and conventions, by programmers working correctly; there is little direct language support for ADTs in C. Ada seems better here. But before the arrival of preconditions etc. Ada didn't have that much to offer to programmers wanting to state sets of permissible values, for example for subprogram parameters. Or wanting to state relations required to hold between parameters. Ada subtypes, e.g. scalars, are poorly equipped for this style of value set specification, AFAICS. They do establish two implicit preconditions (>= S'First and <= S'Last). And these little things seem to do miracles already, judging by the model train study of McCormick. A Qi style type system could do more via types but is not to be in Ada any time soon, is it? Let alone a statically verifiable one. Hence my insistence on a worked out example of a subtype Even with a static specification of the intended value set, one that can be written by a single programmer. Alternatively, as is, package P is type Number is range 1 .. 10; function Compute (A, B: Number) return Number with Precondition => A >= B; type Number_Too is range 0 .. 10_000_000; function Compute_Too (A, B: Number_Too) return Number_Too with Precondition (A + B = 5_000_000); -- etc., with Precondition's predicate in O(P(N)); end; (Such specifications, if they were to be being static, would exclude a test of A in relation to B at run time, for example to reverse their order in a recursive call as needed. It would also exclude a simple test at run time that A + B = 5_000_000.) A distinguishing property of DbC visible here is that a programmer will *see* the contract (or part thereof). Whatever implementation of Compute will later be provided, he does not need to infer arguments in proper calls of Compute from looking at the code of the body (or its object code). Surely code review can provide results insofar as there will be no doubt about what (current!) preconditions can be inferred from the code. The code of the current implementation! Code review, meant as an alternative to giving preconditions, just seems impractical in the general case. Unlike DbC. >> Which set of "specifications" has only static things in it? >> Why exclude conditionals whose results cannot reasonably >> be computed by the compiler but >> >> (a) can be computed for every single case occuring in the >> executing program > > If they can for *every* case, they are statically checkable, per > definition. "Every case" cannot "reasonably be computed by the compiler". Continuing the examples above. (This argument is also somewhere in OOSC2.) >> (b) can guide the author of a client of a DbC component? > > I don't know what does it mean technically. Contractually, it means "do as the preconditions say." And the preconditions say more than an Ada type can ever say! A subprogram is perfect if there is little else to say than "of this subtype", but that isn't always possible. A responsible programmer will then write calls ensuring that an argument is even. Or that the first argument is greater than the second. The client programmer can arrange for these conditions only because he has clear, formal instructions written as preconditions. The contract guides him, it tells what to do. Why not have a computer language help us express these preconditions? Some can even be checked when we develop our software. A paradoxical consequence of this style of invitation (to please write your client code properly) is this: "Under no circumstances shall the body of a routine ever test for the routine's precondition." -- OOCS2, p.343 IOW, no redundant checks. Note that this is true with assertion checking on or off. And yes, the author does say something about defensive programming at the microscopic (routine) level: it should be avoided in DbC systems in favor of correct software. Have DbC help you write correct software instead. (There is more to say here, e.g. about the "magic" that is needed to program a correct defence...) >> For example, assume that Is_Prime(N) is a precondition of sub P. >> Furthermore, TIME(Is_Prime(N))>> PERMISSIBLE_TIME. >> Then, still, PRE: Is_Prime (N) expresses an obligation, >> part of a contract: Don't call P unless N is prime, >> no matter whether or not assertion checking is in effect. > > char X [80]; // Don't use X[80], X[81], no matter etc. Yes, and don't use X[-200]. But you can. OTOH: function Access_Element (S: String_80; X: Index_80); function Careful (S: String_80; X: Index_80) with Precondition => X rem 2 = 1; How would you write a statically checked version? >> (A DbC principle is that assertions are *not* a replacement >> for checking input (at the client side).) > > Exactly. Assertion is not a check. You said this. What check means, exactly, is important. DbC assertion checking or monitoring can turn assertions into run-time checks; these checks turned can be on or off, like pragma Assert in Ada. Input checking is something completely different. Input to a routine comes from a programmer's call. It is the programmer's obligation to make sure input is valid. It is not the called routine's obligation. Another input is I/O, which by the rules is checked for validity, too. >>>> What is "breach of contract" in your world? >>> >>> A case for the court. >> >> What's the court (speaking of programs)? > > A code revision. How do you become aware of a broken contract? Statically? Dynamically? Typically, I think, you notice a malfunctioning program or an exception occurrence; same with DbC. But DbC is also about specifying what you want before you have an issue and before you have a result of code review. In this sense, DbC extends an Ada spec. I guess you can even use DbC assertions in code review comparing results with your contracts. >> I'm a programmer. If I "design" anything, it is a program whose >> parts need to interact in a way that meets some almost entirely >> non-mathematical specification. > > Mathematics has nothing to do with this. It is about a clear distinction > between a contract and a condition, how undesirable it could be but > nevertheless it is a condition, which you, as a programmer are obliged to > consider as *possible*. Eiffel gives you an illusion of safety. No. Eiffel marketing claims that a fully proven DbC program is 100% bug free. I can't imagine that compiler makers will claim that such a program is guaranteed to automatically produce correct results for each input and presume that every input can be successfully tested for validity. They know about SPARK and TTBOMK they won't claim DbC to effect more than SPARK does. > Simply consider > the following rule: my program shall handle each exception I introduce. > Objections? No objection. > Then consider exceptions from assertions. That is what Eiffel's rescue mechanism is about. Failed assertions are one exception case (defined in $12.1 of OOSC2). BTW, there is a rule in DbC about the correctness of exception handlers of primitive operations. The rule starts from a call of a primitive operation that fails (to terminate its execution in a state satisfying the primitive operation's contract {post(x) and INV}. The primitive operation's exception handler is correct if it establishes its type's INV before propagating the exception to its caller. I am mentioning this to draw attention to the fact that DbC is not just a thin, fluffy wrapper for "raise when" or pragma Assert. If it were the latter, then it would be a bit like C style roll-your-own. >>>> How would you specify >>>> >>>> subtype Even is ...; ? >>> >>> Ada's syntax is: >>> >>> subtype is ; >> >> What will static and static be for subtype Even? > > No, in Ada is not required to be static. Example: > > procedure F (A : String) is > subtype Span is Integer range A'Range; > Is the constraint, not to be static, then part of the contractual specification of subtype Even?