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=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,2746dae4f161c04e X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-11-22 19:51:48 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: dewar@gnat.com (Robert Dewar) Newsgroups: comp.lang.ada Subject: Re: Understanding Booleans Date: 22 Nov 2001 19:51:47 -0800 Organization: http://groups.google.com/ Message-ID: <5ee5b646.0111221951.c9892ae@posting.google.com> References: <20011121.053507.496987743.3460@web.de> <3BFBDF14.4B83708B@boeing.com> <5ee5b646.0111212023.17ab963d@posting.google.com> NNTP-Posting-Host: 205.232.38.14 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1006487507 30249 127.0.0.1 (23 Nov 2001 03:51:47 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 23 Nov 2001 03:51:47 GMT Xref: archiver1.google.com comp.lang.ada:16889 Date: 2001-11-23T03:51:47+00:00 List-Id: rod@praxis-cs.co.uk (Rod Chapman) wrote in message news:... > > A := (b = c) or (e = f); > > > > some people prefer to write > > > > if (b = c) or (e = f) then > > A := True; > > else > > A := False; > > end if; > > The latter form suffers slightly from introducing two > paths, > whereas the former only has one (ignoring the possibility > for the moment of the compiler transforming the "or" into > an "or else".) This could have a negative > effect on coverage analysis and the volume (but > not the difficulty) of code proof. > - Rod If this is harder to prove, then it is just an indication of weaknesses in the techniques used, since the two forms are obviously semantically identical. Yes, just as we sometimes distort code to deal with incomplete optimization, we may have to distort code to deal with incomplete proof tools :-)