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 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Tue, 12 May 2015 10:04:27 +0200 Organization: cbb software GmbH Message-ID: <1olki2iqp6u46.w73ivw33kci5.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:25834 Date: 2015-05-12T10:04:27+02:00 List-Id: On Mon, 11 May 2015 19:28:32 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:146ggcmq4yw40.17j749rax0sqi$.dlg@40tude.net... >> On Fri, 8 May 2015 18:31:02 -0500, Randy Brukardt wrote: > ... >>> *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. That's the problem. > (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. Either you must have a very high level code quality or you don't care. Since it is not the latter case, why wouldn't you use C instead? It is the former. Then we return to the starting point of the discussion. No compiler and no language, no matter how tedious, can ensure that level upon compilation. And as you said it is too much burden to require this from programmers. furthermore, it is simply impossible to achieve in just single step of developing process. Yet you cannot delay the phase of executable code forever. Just for pragmatic reasons, most bugs are much simple and effective to find and eliminate running the code. That is why people buy in quick-and-dirty approach. Therefore proofs must be optional, their extent adjustable, the time and place in the developing process up to the programmer. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de