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!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Fri, 2 Dec 2016 20:50:00 +0100
Organization: A noiseless patient Spider
Message-ID: <o1sj6s$9vp$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <o1jdgk$tja$1@dont-email.me>
 <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com>
 <o1kpbo$rni$1@gioia.aioe.org>
 <b777d7e3-4779-4566-b741-8617a9501fd0@googlegroups.com>
 <o1kqk9$tmk$1@gioia.aioe.org>
 <e5adb2c3-f526-4152-9ec9-6e4182e18825@googlegroups.com>
 <o1m2oi$g8l$1@gioia.aioe.org>
 <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com>
 <o1ndod$14ke$1@gioia.aioe.org>
 <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com>
 <o1oohd$13nu$1@gioia.aioe.org> <o1q81b$9kc$1@franka.jacob-sparre.dk>
 <o1s71b$oi7$1@gioia.aioe.org>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 2 Dec 2016 19:48:44 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="a00fa29e63b71b4ac27562256d9ea06e";
	logging-data="10233"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19obFsvVrX8NFtrTYjqtah1Qpn1d0YHyG8="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.0
In-Reply-To: <o1s71b$oi7$1@gioia.aioe.org>
Cancel-Lock: sha1:PpN+GFpeJ6oadVBN+N5tFoSI6KE=
Xref: news.eternal-september.org comp.lang.ada:32561
Date: 2016-12-02T20:50:00+01:00
List-Id: <comp.lang.ada>

On 02.12.16 17:21, Dmitry A. Kazakov wrote:
> Predicates are just arbitrary expressions the programmer sets without understanding all effects of his actions.

So are programs.

While I think I understand the desire for a fully proven
type centered, consistent, awesome Ada program and supporting
language, meanwhile a simple

   pragma Assert (Is_Sorted (S));  -- S a library level constant

has in effect created a desirable change in behavior of an
older program here. Even though the behavior so far had not
caused any concern, a bug was sure lurking.

The predicate Is_Sorted is reflecting formally what had been
a comment only in that program. Making it an executable
predicate has made me spot an error in this:

    To_Mapping ("abcdefghijklmnopqrstuvxyz",
                "ABCDEFGHIJKLMNOPQRSTUVXYZ");

After fixing, one change will be that the program will behave
more correctly, irrespective of the Assert's ignorable
operational effects.

  "I did not realize that the success of tests is that
    they test the programmer, not the program." -- Tony Hoare

It's programmers who write programs, improving their understanding
of a lot of thing that affects their programs, using assertions.

Now, do assertion distract from learning how to write correct
programs using types that manage to express them? And in such
a way that an Ada compiler can determine truth at compile time?

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff