comp.lang.ada
 help / color / mirror / Atom feed
From: Marin David Condic <condicma@bogon.pwfl.com>
Subject: Re: Ada and Java. different behaviour. casting long to int problem.
Date: 1999/06/23
Date: 1999-06-23T00:00:00+00:00	[thread overview]
Message-ID: <3770F79C.42132886@pwfl.com> (raw)
In-Reply-To: 7kp3f2$m9i$1@nnrp1.deja.com

Robert Dewar wrote:
> This is unrealistic. The idea that safety critical software
> depends on programmers doing the right thing on the basis of
> "casual belief" is way off the mark.
> 
Never said that. What I was aiming at was the issue of default semantics
for arithmetic operations. Most of the time when a programmer writes "X
:= X + 1" he's off thinking that he is going to get the successor to X.
It would be the unusual condition which would create an overflow (or
wraparound or saturation)

BTW: We do the intense verification specifically because fallible human
beings often casually assume that X := X + 1 is going to generate the
successor and someone had better test to find out what happens if it
doesn't.

> In fact an unanticipated overflow causing an exception may be
> as dangerous, if not MORE dangerous than an ignored overflow
> (Ariane 5 was a nice demonstration of this).
> 
Yup. That's why I have said elsewhere that I think there should be
different types with different semantics so that the appropriate
behavior can be selected for the application in question. Example:
Standard Integer semantics are fine for a bank balance program because
halting the program with an exception is less harmful than wrapping
around or saturating. Whereas, in most control applications, saturation
is infinitely superior to either an exception or a wraparound.

> In practice in safety critical software, formal verification
> and certification techniques are used to ensure that NEITHER
> event happens.
> 
> Don't worry, when you fly on a plane, regardless of the language
> used, you are not at the mercy of programmers doing *anything*
> casually. Safety critical software just does not work this way!
> 
I don't worry. I build this stuff for a living! :-) Because I do, I'm
very cognizant of the fact that human beings make mistakes on a regular
basis and that's why we go through multiple layers of very expensive
verification before a control is ever allowed to fly a jet engine that
is carrying people. Yet still, we design into it the "What if there is
an error somewhere that we didn't catch?" strategy which guarantees safe
and sane behavior "just in case".

MDC
-- 
Marin David Condic
Real Time & Embedded Systems, Propulsion Systems Analysis
United Technologies, Pratt & Whitney, Large Military Engines
M/S 731-95, P.O.B. 109600, West Palm Beach, FL, 33410-9600
***To reply, remove "bogon" from the domain name.***

Visit my web page at: http://www.mcondic.com/




  reply	other threads:[~1999-06-23  0:00 UTC|newest]

Thread overview: 120+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1999-06-12  0:00 Ada and Java. different behaviour. casting long to int problem nabbasi
1999-06-12  0:00 ` nabbasi
1999-06-12  0:00   ` jerry
1999-06-12  0:00     ` Robert Dewar
1999-06-14  0:00       ` Marin David Condic
1999-06-12  0:00 ` Tucker Taft
1999-06-12  0:00   ` PPAATT
1999-06-12  0:00   ` Keith Thompson
1999-06-12  0:00     ` kirck
1999-06-13  0:00       ` Robert Dewar
1999-06-12  0:00         ` Fred
1999-06-14  0:00           ` Mark Hood
1999-06-15  0:00             ` mike
1999-06-15  0:00               ` Samuel Mize
1999-06-15  0:00                 ` jerry
1999-06-16  0:00                   ` Richard D Riehle
1999-06-16  0:00                     ` jerry
1999-06-15  0:00               ` Marin David Condic
1999-06-15  0:00                 ` Mike Silva
1999-06-15  0:00                   ` rich
1999-06-15  0:00                     ` Samuel Mize
1999-06-15  0:00                     ` Marin David Condic
1999-06-15  0:00                       ` D'Arcy Smith
1999-06-15  0:00                         ` Keith Thompson
1999-06-16  0:00                           ` D'Arcy Smith
1999-06-16  0:00                           ` bill
1999-06-16  0:00                             ` George W. Bayles
1999-06-16  0:00                               ` Fraser Wilson
1999-06-17  0:00                               ` Aidan Skinner
1999-06-17  0:00                                 ` David Botton
1999-06-18  0:00                                   ` Dale Stanbrough
1999-06-18  0:00                                     ` David Botton
1999-06-18  0:00                                       ` Pascal Obry
1999-06-18  0:00                                     ` Matthew Heaney
1999-06-17  0:00                               ` Chris Dollin
1999-07-20  0:00                             ` Geoff Bull
1999-06-16  0:00                         ` George W. Bayles
1999-06-16  0:00                           ` Tucker Taft
1999-06-17  0:00                             ` George W. Bayles
1999-06-17  0:00                               ` Tucker Taft
1999-06-17  0:00                                 ` bob
1999-06-16  0:00                           ` D'Arcy Smith
1999-06-16  0:00                           ` D'Arcy Smith
1999-06-17  0:00                           ` Larry Kilgallen
1999-06-16  0:00                         ` Marin David Condic
1999-06-16  0:00                         ` Mike Silva
1999-06-16  0:00                           ` D'Arcy Smith
1999-06-16  0:00                             ` kirk
1999-06-16  0:00                               ` Hyman Rosen
1999-06-17  0:00                                 ` Robert I. Eachus
1999-06-17  0:00                                   ` Hyman Rosen
1999-06-17  0:00                                     ` Marin David Condic
1999-06-17  0:00                                     ` bob
1999-06-18  0:00                                       ` Hyman Rosen
1999-06-18  0:00                                         ` mike
1999-06-18  0:00                                           ` Hyman Rosen
1999-06-19  0:00                                             ` Samuel Mize
1999-06-21  0:00                                               ` Marin David Condic
1999-06-19  0:00                                             ` Dale Stanbrough
1999-06-21  0:00                                               ` Marin David Condic
1999-06-21  0:00                                             ` Mike Silva
1999-06-17  0:00                                 ` Markus Kuhn
1999-06-17  0:00                                 ` Jean-Pierre Rosen
1999-06-17  0:00                                   ` Marin David Condic
1999-06-17  0:00                                     ` Samuel Mize
1999-06-17  0:00                                       ` Marin David Condic
1999-06-22  0:00                                         ` Hyman Rosen
1999-06-22  0:00                                           ` Keith Thompson
1999-06-23  0:00                                             ` Marin David Condic
1999-06-24  0:00                                               ` Robert A Duff
1999-06-24  0:00                                                 ` Marin David Condic
1999-06-23  0:00                                           ` Marin David Condic
1999-06-18  0:00                                       ` Aidan Skinner
1999-06-20  0:00                                 ` Sera Hirasuna
1999-06-19  0:00                                   ` Kio
1999-06-20  0:00                                   ` Vladimir Olensky
1999-06-21  0:00                                   ` Hyman Rosen
1999-06-21  0:00                                   ` Samuel T. Harris
1999-06-22  0:00                                     ` Richard D Riehle
1999-06-22  0:00                                     ` Robert I. Eachus
1999-06-23  0:00                                       ` Richard D Riehle
1999-06-23  0:00                                       ` Aidan Skinner
1999-06-16  0:00                               ` D'Arcy Smith
1999-06-17  0:00                                 ` Markus Kuhn
1999-06-17  0:00                                   ` D'Arcy Smith
1999-06-17  0:00                                   ` john
1999-06-17  0:00                                     ` Ed Falis
1999-06-18  0:00                                     ` Aidan Skinner
1999-06-17  0:00                           ` Jean-Pierre Rosen
1999-06-22  0:00                       ` Robert Dewar
1999-06-23  0:00                         ` Marin David Condic [this message]
1999-06-23  0:00                           ` Vladimir Olensky
1999-06-23  0:00                             ` Marin David Condic
1999-06-23  0:00                             ` Roedy Green
1999-06-23  0:00                               ` Marin David Condic
1999-06-23  0:00                                 ` Keith Thompson
1999-06-24  0:00                                   ` Mike Silva
1999-06-24  0:00                                   ` Marin David Condic
1999-06-15  0:00                     ` tmoran
1999-06-15  0:00                       ` David Botton
1999-06-16  0:00                       ` Samuel Mize
1999-06-16  0:00                       ` Richard D Riehle
1999-06-16  0:00                 ` Mark Hood
1999-06-17  0:00                   ` Jean-Pierre Rosen
1999-06-17  0:00                 ` Robert I. Eachus
1999-06-17  0:00                   ` Marin David Condic
1999-06-15  0:00               ` D'Arcy Smith
1999-06-16  0:00                 ` George W. Bayles
1999-06-16  0:00                   ` D'Arcy Smith
1999-06-17  0:00                   ` Aidan Skinner
1999-06-17  0:00                   ` Matthew Heaney
1999-06-17  0:00             ` Markus Kuhn
1999-06-17  0:00               ` David Botton
1999-06-13  0:00   ` Robert Dewar
1999-06-14  0:00     ` tmoran
1999-06-30  0:00       ` John Merryweather Cooper
1999-07-01  0:00         ` Chad R. Meiners
1999-07-02  0:00           ` Robert Dewar
1999-07-02  0:00             ` John Merryweather Cooper
1999-07-03  0:00               ` Robert Dewar
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox