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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Wed, 6 May 2015 16:07:17 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1430946437 3011 24.196.82.226 (6 May 2015 21:07:17 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 6 May 2015 21:07:17 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:25740 Date: 2015-05-06T16:07:17-05:00 List-Id: wrote in message news:ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com... ... >But what Ada and SPARK 2014 are doing is "design by contract", as > Bertrand Meyer called it. This makes a confusion between a precondition > and a runtime test. ... >Therefore, I don't think that it is the right choice for a langage that is >mainly >used in safety critical systems. If that's all Ada is going to be used for, it's completely irrelevant what features it has. I would never have used Ada personally if that was the case. Ada (IMHO) is a language to write (more) correct programs, no matter what kind of programs you write. The basic idea behind the preconditions in Ada 2012 is to give a way for people (and implementations and tools as well) to ease into using additional checking and proof. Almost no one is willing to submit to the horrors of complete description of entities as required by SPARK. But (almost?) everyone using Ada would be interested in improving the correctness of their programs, one assertion at a time. After all, consider how you likely learned the value of ranges and strong types and subtypes. Most everyone started out using mostly type Integer for everything. But one quickly notices that those cases where separate types were used get more errors detected at compile time and at runtime -- eliminating what usually are long and painful debugging sessions. This positive feedback loop quickly turns most Ada programmers into advocates and heavy users of the simple tools available in Ada. By extending those mechanisms (via predicates and preconditions) to arbitrary expressions, we allow much more such error detection to occur. There's also a performance benefit. In my experience, 10-20% of Ada code is checking code correctness (such is that a container routine is not passeed a null cursor). By making these sort of rules preconditions or (better) predicates, we increase the chances that errors are detected immediately so no debugging is needed. I don't believe that checks in Ada (of any kind) should ever be turned off. It's much better to let the compiler eliminate those that aren't needed (which is most of them, if your program is written correctly). The same will happen for predicates and preconditions and so on. I also don't believe in separate proof tools. That's something that should be a basic part of the compiler (it has to be to do optimization, check elimination, and the like anyway). The difficult question is how to feed information about those things (particular checks known to fail) back to the programmer (as optimization phases tend to run without messages, and the messages that they do give are rather non-specific). In order for proof to be part of the compiler, the proof language has to be part of the language. Lastly, fancy proof languages tend to be beyond the skill level of ordinary (and some not so ordinary) programmers. Despite, 6 years of University education, a masters degree, and 30 years of real-world experience, I had to have both the meaning of the implication operator and a "universally quantified predicate" explained to me. As it turns out, I had run into both in the past, but not under those names. Moreover, the programming language semantics is already complete -- why invent a new syntax just to confuse people? (I know from the early days when the compiler was written in Pascal how hard it is to switch between two similar languages used in similar contexts. That would be a permanent rather than transient problem.) As I noted before, Ada (prior to 2012) uses exceptions to describe both requirements on callers and error conditions in a routine. It's much better to separate these, because the former can be eliminated by proof techniques and the latter cannot (no proof technique can tell you that a file will exist when it is initially opened). Ada 2012 preconditions allow one to do this without having to change the defined semantics of a routine (meaning that they can be profitably used on existing code). The idea that proof has any value by itself is the real problem here. At best it is a tool to reduce the needed checking in a program, and a way to detect problems at compile-time (in this later use, it's only really of value as part of the compiler -- most programmers will not screw around with extra tools that have to be configured and managed and slow down the development process even more). Once you over-rely on proof, all you've done is forced your code into a new kind of specification, one that will have at least as many errors as the original. There's little value in that (especially in larger programs). Anyway, more than enough ranting on this topic. IMHO, Ada 2012 gets it right, and building SPARK on top of it makes it more accessible to more programmers. That seems like a good idea, even if SPARK itself remains misguided. Randy.