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!.POSTED!not-for-mail From: Georg Bauhaus Newsgroups: comp.lang.ada Subject: Re: SPARK: missing case value Date: Sat, 10 Oct 2015 16:19:31 +0200 Organization: A noiseless patient Spider Message-ID: References: <87twq09ke2.fsf@theworld.com> <8ea6wfytssdg.1ake0jrn1irc8.dlg@40tude.net> <8auc1f2imdsr.1clgpdkai0ezl.dlg@40tude.net> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=big5 Content-Transfer-Encoding: 8bit Injection-Date: Sat, 10 Oct 2015 14:17:33 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="10ca66458083610b89918ee8fea6489c"; logging-data="8853"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19J79KeSD0A8rlf+k9O5SG97biyIh1BvLw=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0) Gecko/20100101 Thunderbird/38.3.0 In-Reply-To: <8auc1f2imdsr.1clgpdkai0ezl.dlg@40tude.net> Cancel-Lock: sha1:B95gYfC8JPXm13vnpV41/rY8ozY= Xref: news.eternal-september.org comp.lang.ada:27964 Date: 2015-10-10T16:19:31+02:00 List-Id: On 10.10.15 12:00, Dmitry A. Kazakov wrote: > >> 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... Killed as agreed in the contract, so to speak. > aircraft shattered into pieces and burned down, check! The system has failed to respond to assertion failure. That's what robustness is about. https://en.wikipedia.org/wiki/Robustness_(computer_science) > Post-conditions are *proved* to be implied by the pre-conditions. Uhm, no, post-conditions (after "Post => ") are stated, nothing more. If someone proves implication (hopefully), that's only related. (The work would be from the obligation part of DbC.) > Proof /= check. Absolutely. And contract based design encourages proofs, but proofs need not be part of the contract. However, it is the right of either party to misbehave if the contract was violated. Checks will help detect violations. >>>> [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. Is "condition" to mean "state", then? I think "X > 0" is a perfectly normal condition in the sense of boolean_expression; also, in another sense, it expresses the possible "conditions" in which variable X would be, making the quoted text evaluate to True or False. So, just write a predicate that takes a long time to compute, say, so long that the compiler gives up (in some way), but is otherwise easily stated and only assumed to be true, like a conjecture. >> Should the compiler reject known truths? > > Known to who? The experts. See previous discussions. Programmers will then be able to draw conclusions from the stated truth. > 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. Sorry, correction: "should [the compiler] just arrange for performing the test at run-time?" That's instead of rejecting a predicate, just because the compiler does not have the powers for "testing" all values at once by formal demonstration. I note that one can also demonstrate correctness by testing each possible set of values, so a proof is not the only means. Just so much more useful, early, possibly preventing exceptions, and likely fast enough, unlike testing. >> (*) "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. The outcome does make the programs "not ... miss their stated goals". It does make the result correct even though the program did not correctly implement some specification. So, the latter correctness ("*") does not exhaust possible causes for programs apparently being correct, that's all. (Seems better to me to have correct results, rather than stop producing results at all because they could be got the wrong way.) And that's what. Also this: the paragraph was meant to emphasize that correct programs seem to be a pipe dream in the sense that there will always only be particular programs achieving some amount of correctness. But in general, we need to write and debug programs without being hindered by some expressions not being static or possibly failing. That seems more practical than just giving up, dreaming the dream. > A program is correct (as defined) > or not independently on the skills of any given programmer. How do we know that some given program is correct or not? By narrowing program design so that what is allowed in programming needs to be statically decidable? Should we prove larger systems correct or else not run them at all? Contracts as in "contract based design" are, I think, not about after-the-fact properties of a program. They exist prior to implementation. Hopefully, skillful programmers will feel obliged to show that the contract is good and that their programs follow the contract.