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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.220.230 with SMTP id pz6mr2829469pbc.3.1341319564585; Tue, 03 Jul 2012 05:46:04 -0700 (PDT) Path: l9ni10736pbj.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Tue, 3 Jul 2012 14:46:10 +0200 Organization: cbb software GmbH Message-ID: <13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net> References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> 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-07-03T14:46:10+02:00 List-Id: On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net... >> You seem to imply that value in the range is a precondition of the >> operation constrained to that range. This is wrong. > > It can't be "wrong", because the programmer of an abstraction decides what > the preconditions and postconditions are. No. He cannot decide them to implement the contract. That he actually can, per allowing dynamic checks, is a language design bug. >> If S is a subtype of T then the precondition is >> >> X in T >> >> The postcondition is >> >> (X in S and ) or (X not in S and Constraint_Error propagated) >> >>> And Ada *always* has had dynamic preconditions: >>> >>> procedure New_Line (Spacing : in Positive_Count := 1); >> >> The precondition here is Spacing in Positive_Count'Base because the >> behavior of New_Line is *defined* when Spacing is not in >> Positive_Count'Range. >> >> New_Line(0) >> >> is a *legal* Ada program. > > Legality has nothing to do with preconditions or postconditions. => It is OK to violate a "contract" defined by these. Here you are. > The only kind of correctness checks that *can* exist in general are dynamic. > Ada's entire reason to exist is to include checks like range checks and > overflow checks to programs. Without them you get the buffer overflows and > other errors that plague C code. Yes, but irrelevant. These checks are not contract checks, because, otherwise you are in contradiction. No words can change that. But also there are important consequences for software engineering. Since these checks have nothing to do with contracts, they must be considered as a part of the program semantics and all possible outcomes must be *handled*. The problem of buffer overflow is exactly in pretending that it cannot overflow. So the program is broken when it does. > I suppose you have a totally different definition of "correctness checks" > than I do; as usual, we can't have a useful discussion because you have your > own set of terminology. Terminology is secondary to the semantics. The problem is with the meaning. > SPARK is next to useless for real programs - at best it can be used only to > prove small parts of a program, and it takes a lot of effort to get there. You don't need to prove every possible aspect of the program. The language should allow the programmer to choose. Ada 83 had provable contracts stated in terms of types. Nothing prevents us from having more detailed contracts as well as other program correctness stuff. I simply don't understand where is a problem with that. > Instead of getting the benefits of building in Ada now, > and getting more and more static checks as compilers improve. I don't see tracking down exceptions as a benefit. Neither would it be a for the maintainer to discover that the program suddenly became illegal because static checks has been "improved." I prefer to rely on things known to work now. These I use and hope that they will continue to work in the future. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de