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: Sat, 9 May 2015 08:16:21 +0200 Organization: cbb software GmbH Message-ID: <146ggcmq4yw40.17j749rax0sqi$.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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: evoS9sCOdnHjo0GRLLMU1Q.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:25787 Date: 2015-05-09T08:16:21+02:00 List-Id: On Fri, 8 May 2015 18:31:02 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net... >> On Thu, 7 May 2015 13:32:28 -0500, Randy Brukardt wrote: > ... >>> You end up writing the program twice in two different languages. >> >> That is the idea. But it is not *the* program. The program is written only >> once in Ada. The proofs are written *for* this program, they do not change >> the program itself. Though proofs may hint the programmer to redesign >> certain parts of the program. > > That's madness. If the description is sufficiently complete to describe the > program (and it has to be for the proofs to mean much), then one could have > generated the program from that description and forget the Ada altogether > (and most people would do exactly that). Except that no description ever complete. A more important thing is that you could not convert such descriptions into code. As an example consider a definition of sine from a text book. It sufficiently completely defines sine, but gives you no idea what sin(0.76) is. The difference is in the computational framework. The behavior descriptions are intended for the correctness prover. They program the prover, nothing else. The behavior definitions (the program proper) are intended for the machine. They program the machine. (The definitions from the text book are for the framework which is not even computable) > 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? > *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! (:-)) > The only benefit > to any of these things is in shortening the debugging time, but once that's > already done, further work is pointless. (We had a rule at RRS about not > futzing with working code, because we'd been burned by that many times. It > was necessary to prevent people like me wasting lots of time on "cleanups" > that ultimately didn't clean up anything. As Tucker likes to say, you can > move the bump under the rug, but its rare that you can get rid of it.) Adding proofs meant to happen much earlier than that. But, surely, I would gladly add proofs to already deployed code. It is always worth to look after potential problems. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de