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,699cc914522aa7c4 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Structured exception information Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <1168885771.30643.20.camel@localhost> <1168891576.30643.39.camel@localhost> <5NKdnTv2UZfVZTbYnZ2dnUVZ_vipnZ2d@megapath.net> <38z8yk9z1uxn$.1r6qpevwu2i7c.dlg@40tude.net> <1lpy2h06scx34.1i2k4dlbg0nfy.dlg@40tude.net> Date: Thu, 18 Jan 2007 10:55:20 +0100 Message-ID: NNTP-Posting-Date: 18 Jan 2007 10:55:20 CET NNTP-Posting-Host: 7a093af7.newsspool3.arcor-online.net X-Trace: DXC=UE1THbb?gi:QbA1[CgMQ00McF=Q^Z^V384Fo<]lROoR1gUcjd<3m<;2MUZ;RCm1@E:[6LHn;2LCV>7enW;^6ZC`4F0oL On Wed, 17 Jan 2007 18:38:21 GMT, Jeffrey Carter wrote: > Dmitry A. Kazakov wrote: >> >> I doubt that others could or should be called preconditions. > >> The point is that violated preconditions are non-states and cannot be >> handled at all. Provided, that one understands precondition as a method of >> proving program correctness. Otherwise, it is something else. > > It's clear that you're locked into the concept of a precondition as part > of correctness proofs. In that context, yes, you statically prove that > preconditions are met, and do not need to dynamically test them. This is > the case with SPARK, for example. I think that stress on compile-time checks is to some extent misleading. In my view, the issue is not "when", but "who" performs the checks. Correctness checks cannot be performed by the same program. In the case of static checks, it is just so that the compiler program P2 checks my program P1. If I wished to check my program at run-time, I should have a run-time checker P3. For that matter, it could well be a part of Ada run-time library, provided it were good insulated from my P1. But in all cases, when P2 or P3 detects that P1 is incorrect (not Ada), then P1 cannot be continued. The checker is free to start some third (Ada) program, though. For this reason exception propagation in P1 were fundamentally flawed. We cannot pretend that P1 has any scope which wasn't spoiled by the bug. > In general, though, preconditions are a useful tool for documenting SW, > especially SW that will be used by people other than the developer. It's > a useful way of communicating to the client what he needs to ensure in > order for the SW to function normally (this condition must be true), and > the consequences of failing to do so (this exception is raised). To me this is a contract: x/y yields a mathematically correct result or else it propagates an exception when, for example, y=0. I.e. it is legal to write 1/0 and the precondition is True. If the precondition were y/=0, then 1/0 would be illegal and nothing could be done about it. > Ideally, you'd use the same syntax for both uses of preconditions. I think is a difficult question. The languages of P1 (my program) and of P2 (a checker of) could be sufficiently different, by necessity. On the other hand, Ada compilers are written in Ada... In any case there should be a clear visual distinction between the contracts and the things checking the contracts. The latter are optional (=have the semantics outside P1) the former are not (=have the semantics of P1). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de