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: Sun, 11 Oct 2015 11:49:34 +0200 Organization: cbb software GmbH Message-ID: <1qsryd24l5y5t.13tfy1u51de0o.dlg@40tude.net> References: <87twq09ke2.fsf@theworld.com> <8ea6wfytssdg.1ake0jrn1irc8.dlg@40tude.net> <8auc1f2imdsr.1clgpdkai0ezl.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:27965 Date: 2015-10-11T11:49:34+02:00 List-Id: On Sat, 10 Oct 2015 16:19:31 +0200, Georg Bauhaus wrote: > On 10.10.15 12:00, Dmitry A. Kazakov wrote: >> >> aircraft shattered into pieces and burned down, check! > > The system has failed to respond to assertion failure. That's what robustness > is about. How much robust... The only problem is again confusion of terms. When the system responds [as required], it is no more failure, just per definition of response. >> Post-conditions are *proved* to be implied by the pre-conditions. > > Uhm, no, post-conditions (after "Post => ") are stated, nothing more. Then the thing after "Post => " is not a post-condition. See above. >> Proof /= check. > > Absolutely. And contract based design encourages proofs, but proofs > need not be part of the contract. Proofs are never a part of the contract. Proofs is the contract enforcer. No enforcement, no contract, just hot air. >>>>> [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? A set of states. > 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. Given a decision framework it is either decidable or not. If not decidable then it is not a condition. >>> 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. Good to them, but unrelated to the case at hand. There no such thing as truth outside a decision framework. If the framework is a compiler, then the only truth is what the compiler decides as truth. You can define a set of compilers having the same property of being able to prove truths you want to be true. That is what language design is about. >> 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?" No difference. There is no tests at run-time either. Run-time means program deployed and performing expected actions which is different from a program under test, as VW guys could wisely point out... > I note that one can also demonstrate correctness by testing each > possible set of values, so a proof is not the only means. Covering all program states IS a proof. >>> (*) "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". Right, what about 2 and 3? > 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. You confuse achieving correctness with defining correctness. Regardless whether correctness is achievable and any means of doing so, you must define what a correct program is. Even in the case when a correct program may not exist in the given computational framework (e.g. Turing-incomplete). [*] The goal of SW design is writing correct programs. >> 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? That depends on how we defined it being correct. > By narrowing program design so that what is allowed in programming > needs to be statically decidable? It is a good idea to define correctness decidable. But of course all sorts of informal requirements could easily do it undecidable or non-existent. > Should we prove larger systems correct or else not run them at all? We should prove as much as possible and economically/ethically/legally reasonable. > Contracts as in "contract based design" are, I think, not about after-the-fact > properties of a program. They exist prior to implementation. Which precludes any run-time semantics, obviously. Thank you for agreeing with my point. > Hopefully, skillful programmers will feel obliged to show that the contract > is good and that their programs follow the contract. Huh, contradicting yourself in just two consequent sentences? ---------------- * Correctness is defined is much more powerful frameworks that programming language, e.g. when requirements are written in natural language or given as mathematical expressions etc. Which is the core problem of programming and design, as a mapping of the problem space semantic (correctness #1) onto the language semantics (correctness #2). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de