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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: "Alejandro R. Mosteo" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 13 Dec 2016 12:56:22 +0100 Organization: A noiseless patient Spider Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 13 Dec 2016 11:55:00 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="05d53532b8e857d633012e02e9d3ce5e"; logging-data="6658"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+0XymD5RSLhXDRxDKQHlku" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 In-Reply-To: Cancel-Lock: sha1:HdxNPHTm5GOR+WSweL9xl8LOo1o= Xref: news.eternal-september.org comp.lang.ada:32778 Date: 2016-12-13T12:56:22+01:00 List-Id: On 05/12/16 09:58, Dmitry A. Kazakov wrote: > On 05/12/2016 09:41, Stefan.Lucks@uni-weimar.de wrote: >> On Sun, 4 Dec 2016, Robert Eachus wrote: > >>> I would consider it a major bug to have a pragma Assert that could >>> fail at run-time absent a hardware failure or some such. (Even though >>> it would be turned off in production code.) >> >> I don't quite think so. A failed Assert (or a failed pre- or >> postcondition, which are essentially a nice way to put Asserts in >> specifications) *may* be checked even in the productin system. What is >> important is to always shut down when upon Assert-failure -- preferably >> after writing diagnostic information to wherever digagnostics goe. > > A run-time "failed" Assert is an if-statement evaluating false. There is > nothing of failure there. > > Things called in Ada pre- and post-conditions if evaluated during > run-time are merely subprogram bodies booby-trapped with unanticipated > exceptions. Bad thing. Jumping in here for lack of a better place. I'm a bit flabbergasted (in a good way, I'm learning a lot) about some positions being argued. It seems I'm way out of league when it comes to theory of languages. At some points it seems to me that the discussion is almost merely about semantics of the terms being used (precondition, predicate, etc) but then at other it clearly seems not: - Pre are not preconditions (but what's the formal definition?) - Pre/Post (aspects in general?) should not be used, or be hidden (Apologies if I am misremembering.) Generally speaking, I see these additions to Ada 2012 as something that average programmers would welcome, so it surprises me that they should be characterized as that problematic. At the same time, I think that SPARK was one of the reasons to bring them on (to make SPARK comments part of the static/dynamic checks?), which again seems a movement in the direction of reliability that Ada strives for. Since it seems that usually is you, Dmitry, the one coming from a more theoretical (mathematical? purist?) POV into the arguments, perhaps you could recommend to me some reference(s) where I can better understand the principles involved in this discussion (the part about preconditions/predicates, not IR)? I confess to having only a superficial grasping of the situation, by way of using the Ada 2012 facilities. Thanks, Álex. > >> On one hand, there are systems that must not shut down (maybe an >> autopilot at flight time). If that is the case, Assert-checking in >> production executables is plain wrong. > > It is plain wrong regardless. If assertion is a correctness statement it > shall never be checked at run time. If assertion is an if-statement with > exception raised upon one of the outcomes it must *always* be evaluated > unless the condition proven static. It is either or, never both. >