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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,7fd5a5da28dace78 X-Google-Attributes: gid103376,public From: John McCabe Subject: Re: Renaming Fixed Point Mutiplicative operator in Ada 95 Date: 1998/05/22 Message-ID: <6k3dj2$15e@gcsin3.geccs.gecm.com>#1/1 X-Deja-AN: 355494381 Content-Transfer-Encoding: 7bit References: <3561F32B.2F0B@innotts.co.uk> <01bd84c3$47215d60$440029a1@m00rq900> <356536FD.87A2B0A@praxis-cs.co.uk> Content-Type: text/plain; charset=us-ascii Organization: GMS&T Mime-Version: 1.0 Newsgroups: comp.lang.ada Date: 1998-05-22T00:00:00+00:00 List-Id: Rod Chapman wrote: >Robert Dewar wrote: > >> Incidentally, in a critical system, I would jolly well hope that EITHER >> >> a) you prove that division by zero cannot happen >> > >We've done that (for all exceptions) for several non-trivial SPARK programs. >It's actually a useful exercise too! I performed a similar exercise once but, rather than divide by zero, I had to prove that our program would not be affected by data dependencies in the floating point unit of a GPS MA31750 MIL-STD-1750A processor that would result in the wrong answer. It was quite interesting and saved a lot of effort in the long run! -- Best Regards John McCabe ===================================================================== Any opinions expressed are mine and based on my own experience. They should in no way be taken as the opinion of anyone I am currently working with, or of the company I am currently working for. If you have a problem with anything I say, SPEAK TO ME! =====================================================================