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!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Newsgroups: comp.lang.ada
Subject: Re: How to get Ada to ?cross the chasm??
Date: Fri, 11 May 2018 23:32:17 +0300
Organization: Tidorum Ltd
Message-ID: <flmcuiFboocU1@mid.individual.net>
References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com>
 <pc8l7e$km5$1@franka.jacob-sparre.dk> <87in88m43h.fsf@nightsong.com>
 <cd866ee8-ad4d-489e-a38b-d8e5f5d4af00@googlegroups.com>
 <87efiuope8.fsf@nightsong.com> <pcdagp$7pn$1@franka.jacob-sparre.dk>
 <87lgd1heva.fsf@nightsong.com> <pcg54t$gul$1@franka.jacob-sparre.dk>
 <87zi1gz3kl.fsf@nightsong.com> <pciqcd$ou1$1@franka.jacob-sparre.dk>
 <878t8x7k1j.fsf@nightsong.com> <fl7t0uF410rU1@mid.individual.net>
 <87fu342q1o.fsf@nightsong.com> <fleiqiFjhprU1@mid.individual.net>
 <87mux9645j.fsf@nightsong.com> <fljn0oFnugqU1@mid.individual.net>
 <8736yz18e4.fsf@nightsong.com>
 <e47585a0-8bb0-46c2-82be-140b189643e8@googlegroups.com>
 <pd4gmg$koe$1@dont-email.me> <87mux62it0.fsf@nightsong.com>
 <flm7hdFainiU1@mid.individual.net> <87k1sat1ie.fsf@nightsong.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net L8hvtJMjs6zzOB2oCgKu2wsLmPgIxwDOPSiYwyeNbammksBrBA
Cancel-Lock: sha1:PjNaUcg+M6YQGBzNYQDX1h0SCa0=
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0)
 Gecko/20100101 Thunderbird/45.8.0
In-Reply-To: <87k1sat1ie.fsf@nightsong.com>
Xref: reader02.eternal-september.org comp.lang.ada:52288
Date: 2018-05-11T23:32:17+03:00
List-Id: <comp.lang.ada>

On 18-05-11 22:50 , Paul Rubin wrote:
> Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

>> Robert Dewar used to say that when some Ada source code is _really_
>> semantically equivalent to some C source code, GNAT is expected to
>> produce the same machine code for the Ada as GCC/C produces for the C,
>
> Yes, but constructions that express the same programmer intent are not
> semantically the same between the two languages.  Particularly a[i] is a
> checked reference in Ada and unchecked in C, and similarly a+b is (or
> should be) a checked integer addition in Ada, but it's UB in C in the
> case of overflow.

Yes, but for those examples, I think Robert Dewar would have assumed the 
Ada code to be compiled without the run-time checks, in order to have 
semantic equivalence. Alternatively, the C code would have to guard a[i] 
with checks on i. The case a+b would be harder to guard in the C form.

>> The CodePeer analysis tool from AdaCore is a compromise. It can be
>> used to prove that no run-time checks will fail
>
> Oh that sounds interesting.  I didn't know about it.

As I understand CodePeer, it is basically a weakest-precondition 
generator. You point it at a subprogram and it will give you the weakest 
precondition on parameters and globals that ensures that there will be 
no run-time error in the subprogram. It can also (of course) do 
inter-procedural analysis and make use of the various contracts 
specified in the program, as well as the usual type-specific constraints.

I haven't yet used CodePeer much myself, but a colleage did manage to 
prove run-time-error absence in a full on-board SW project for a quite 
complex instrument controller.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .