Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.arch.embedded > #30539
| From | Niklas Holsti <niklas.holsti@tidorum.invalid> |
|---|---|
| Newsgroups | comp.arch.embedded |
| Subject | Re: C++, Ada, ... |
| Date | 2021-04-20 10:47 +0300 |
| Organization | Tidorum Ltd |
| Message-ID | <ie7f7qFhbedU1@mid.individual.net> (permalink) |
| References | (5 earlier) <s5hogv$77o$1@dont-email.me> <ie55l3F3ou7U1@mid.individual.net> <87blaagjyc.fsf@nightsong.com> <ie6aruFat9fU1@mid.individual.net> <877dkxyj3o.fsf@nightsong.com> |
On 2021-04-20 2:01, Paul Rubin wrote:
> Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
>> You can impose that constraint if you want to: if I had defined
>> type Zero_Handler is not null access procedure;
>> then the above declaration of the At_Zero component would be illegal,
>> and the compiler would insist on a non-null initial value.
>
> Oh, this is nice.
>
>> But IMO sometimes you need pointers that can be null, just as you
>> sometimes need null values in a database.
>
> Preferable these days is to use a separate type for a value that is
> nullable or optional, so failing to check for null gives a compile-time
> type error. This is 't Option in ML, Maybe a in Haskell, and iirc
> std::Optional<T> these days in C++.
I'm not aware of proposals for such a thing in Ada.
>> The state of the art in Ada implementations of critical systems is
>> slowly becoming to use static analysis and proof tools to verify that
>> no run-time check failures, such as accessing a null pointer, can
>> happen. That is already fairly easy to do with the AdaCore tools
>> (CodePeer, SPARK and others). Proving functional correctness still
>> remains hard.
>
> I know about SPARK. Is CodePeer something along the same lines? Is it
> available through GNU, or is it Adacore proprietary or what?
CodePeer is a for-money AdaCore tool, a static analyzer that basically
(AIUI) applies bottom-up weakest-precondition construction and
pre-post-condition analysis to detect many kinds of logical programming
problems, in particular possible failures of run-time checks.
See https://www.adacore.com/codepeer.
To use it in practice on larger programs, one usually has to guide and
help its analysis by writing a certain amount of explicit precondition
and postcondition aspects into the Ada source (which CodePeer then
verifies as part of its analysis), but that has other benefits too, of
course.
> I still have Burns & Wellings' book on SPARK on the recommendation of
> someone here. It looks good but has been in my want-to-read pile since
> forever. One of these days.
Note that most if not all of the SPARK-specific comments that were used
earlier have now been superseded by the precondition, postcondition,
invariant etc. aspects in standard Ada, and the SPARK tools have been
updated accordingly. I'm not sure if this replacement is complete; I
haven't used SPARK.
By the way, did you know that NVIDIA has started using SPARK? There's a
presentation at
https://www.adacore.com/webinars/securing-future-of-embedded-software.
niklas holsti tidorum fi
. @ .
Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
C++, Ada, ... pozz <pozzugno@gmail.com> - 2021-04-17 17:48 +0200
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-17 18:45 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-17 19:55 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 12:53 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-18 18:48 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 18:59 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-19 13:51 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 14:22 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-19 19:16 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 22:19 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-20 01:03 +0300
Re: C++, Ada, ... Richard Damon <Richard@Damon-Family.org> - 2021-04-19 18:09 -0400
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-20 06:58 +0200
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 23:18 -0700
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-20 09:36 +0200
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 12:20 -0700
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-20 00:26 +0300
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 16:01 -0700
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-20 10:47 +0300
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-19 23:30 +0100
Re: C++, Ada, ... Clifford Heath <no.spam@please.net> - 2021-04-18 08:29 +1000
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-18 10:39 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 14:59 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-18 19:23 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 19:26 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-18 19:29 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 22:23 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-18 23:09 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 08:56 +0200
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-19 14:04 +0300
Re: C++, Ada, ... Dimiter_Popoff <dp@tgi-sci.com> - 2021-04-19 15:16 +0300
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 12:47 -0700
Re: C++, Ada, ... Niklas Holsti <niklas.holsti@tidorum.invalid> - 2021-04-20 00:37 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-20 07:50 +0200
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 14:26 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-18 19:30 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-18 22:17 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-18 23:17 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 08:52 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-19 10:08 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 12:15 +0200
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-19 12:00 +0100
Re: C++, Ada, ... Tauno Voipio <tauno.voipio@notused.fi.invalid> - 2021-04-19 16:15 +0300
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 15:43 +0200
Re: C++, Ada, ... pozz <pozzugno@gmail.com> - 2021-04-19 18:38 +0200
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 10:48 -0700
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-19 19:33 +0100
Re: C++, Ada, ... Tauno Voipio <tauno.voipio@notused.fi.invalid> - 2021-04-20 15:09 +0300
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-20 15:29 +0100
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-19 22:48 +0200
Re: C++, Ada, ... pozz <pozzugno@gmail.com> - 2021-04-19 23:17 +0200
Re: C++, Ada, ... Paul Rubin <no.email@nospam.invalid> - 2021-04-19 15:55 -0700
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-20 08:21 +0200
Re: C++, Ada, ... David Brown <david.brown@hesbynett.no> - 2021-04-20 08:20 +0200
Re: C++, Ada, ... Dave Nadler <drn@nadler.com> - 2021-04-17 21:07 -0400
Re: C++, Ada, ... Don Y <blockedofcourse@foo.invalid> - 2021-04-17 18:53 -0700
Re: C++, Ada, ... Tom Gardner <spamjunk@blueyonder.co.uk> - 2021-04-18 09:42 +0100
Re: C++, Ada, ... dalai lamah <antonio12358@hotmail.com> - 2021-04-18 14:39 +0200
csiph-web