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: SPARK: missing case value Date: Sat, 10 Oct 2015 12:00:08 +0200 Organization: cbb software GmbH Message-ID: <8auc1f2imdsr.1clgpdkai0ezl.dlg@40tude.net> References: <87twq09ke2.fsf@theworld.com> <8ea6wfytssdg.1ake0jrn1irc8.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: j6IQVb9uobzjXrpQLDU2rQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="big5" Content-Transfer-Encoding: 8bit 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:27962 Date: 2015-10-10T12:00:08+02:00 List-Id: On Sat, 10 Oct 2015 11:10:48 +0200, Georg Bauhaus wrote: > On 09.10.15 23:01, Dmitry A. Kazakov wrote: >> On Fri, 9 Oct 2015 22:29:21 +0200, Georg Bauhaus wrote: >> >>> A precondition states conditionality of proper execution. >> >> You said that. > > That's what clauses of contracts do: they state conditions. > "Don't touch it or it'll ¡K!". You are free to touch. Killing you is a proper execution of laws of physics when you jump head down from the sky scrapper... >> Proper execution should be unconditional to the program >> state. Otherwise it is called 'bug'. > > Yes, of course! If a contract is violated, that's the work of > a bug.(*) > >> Ergo, precondition, especially a >> dynamic one, is a method of introducing bugs. > > A precondition is also used as a method of detecting bugs, Likewise, aircraft crash is a method of detecting engine failures... > preconditions usually being checked. Yes, the aircraft shattered into pieces and burned down, check! > Which bugs? Notably, failures to make some earlier post-conditions true. > Seemingly, post-conditions are not usually checked. Post-conditions are *proved* to be implied by the pre-conditions. Proof /= check. >>> [dynamic being more than static] >> No idea what this was supposed to mean. > > Dynamic predicates may express conditions that the compiler cannot > show to always be true, They may not. The only way to express a condition to show it true. > the compiler reflecting some state of the art. > A predicate may be known or assumed to be true and yet the compiler > cannot decide this. Should the compiler reject known truths? Known to who? The compiler knows the language, nothing else, nothing more. The rest is bad philosophy. > Or should it just perform the test at run-time if you tell it to do so? There is no compiler at run-time. Your reasoning is ridden with logical fallacies only possible because you confuse terms proof vs. check, compile vs. run-time, program vs. semantics of... > (*) "should ¡K" above seems to imply the ideal situation of universally > correct programs. This seems wishful thinking. At the risk of repeating > old stuff, some designs are built on top of conjectures. Also, > unforeseen program states are pretty normal in many programs, and not all > of them will necessarily make the programs miss their stated goals. So what? 2+2=4 even if you meant 2*2. That does not make it correct. Bad philosophy, again. Multiplication exists and is well-defined independently if somebody fell asleep in his classes. A program is correct (as defined) or not independently on the skills of any given programmer. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de