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: Mon, 11 May 2015 19:28:32 -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> <1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net> <8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net> <146ggcmq4yw40.17j749rax0sqi$.dlg@40tude.net> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431390512 21324 24.196.82.226 (12 May 2015 00:28:32 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 12 May 2015 00:28:32 +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:25821 Date: 2015-05-11T19:28:32-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:146ggcmq4yw40.17j749rax0sqi$.dlg@40tude.net... > On Fri, 8 May 2015 18:31:02 -0500, Randy Brukardt wrote: ... >> And there are few applications >> where there is any value to writing the program twice; for most, it is >> just >> wasted time. > > Nothing is written twice. Proof specifications are as much program as test > code is. Don't you write tests? Outside of the ACATS (which is a product unto itself), not often. Sometimes I rewrite other people's tests to generalize them or to simplfy them. Most of my programs are tested in-situ, either with live data (as in the web server/mail server) or by using constructed data. (The ACATS essentially falls into this category, from the prespective of a compiler.) I definitely don't write or use unit tests in the majority of cases. It's easier to use live data than to figure out some way of getting that data correctly initialized in order to do a unit test. (Consider operations on a compiler symboltable. In order to unit test those, you have to construct a symboltable for them to work on, and that symboltable has to be constructed exactly as the compiler will do it - otherwise you end up testing the unit test more than anything useful. Since the compiler already knows how to do that, we let the compiler do the setup and then debug in place.) Since testing proves almost nothing about a program's quality, I prefer to avoid them (and it) as much as possible. [Probably too much. :-)] I want my compiler to detect all of my mistakes before I run anything. That's the whole reason I started to use Ada and continue to use Ada. (Plus testing and debugging of tests is incredibly frustrating.) >> *Especially* if you're adding them after the fact -- what would >> the point be? The program is already debugged and fielded. > > Most interesting programs cannot be debugged. It is quite strange, you > don't believe correct program exist, but trust "debugged" programs do! > (:-)) Naw, Ada does my debugging. When there's a problem that actually requires debugging, it takes forever for it to get fixed. (Sorry, Tero. ;-) My point as just that a fielded program already has some amount of testing and fixing done to it (we hope), and once that happens, leave it alone until/unless there is a problem. Randy.