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: Fri, 9 Oct 2015 17:34:34 +0200 Organization: cbb software GmbH Message-ID: References: <87twq09ke2.fsf@theworld.com> <87lhbc9idb.fsf@theworld.com> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: j6IQVb9uobzjXrpQLDU2rQ.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:27951 Date: 2015-10-09T17:34:34+02:00 List-Id: On Fri, 09 Oct 2015 11:22:40 -0400, Bob Duff wrote: > "Dmitry A. Kazakov" writes: > >> Because the above is a proper contract, while precondition is a land >> mine. > > Why do you think preconditions are dangerous? Even when statically checked they may cause issues as presented. And it trivially follows from the basic SW design principle of weakening preconditions. The weakest possible precondition is True, i.e. none. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de