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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,99e73f65ea2533b9 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!194.25.134.126.MISMATCH!newsfeed01.sul.t-online.de!newsfeed00.sul.t-online.de!t-online.de!news-lei1.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: and then... (a curiosity) Date: Fri, 5 Sep 2008 08:57:29 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <18b41828-bda4-4484-8884-ad62ce1c831d@f36g2000hsa.googlegroups.com> <57qdnfULQ9tzKCHVnZ2dnUVZ_tHinZ2d@comcast.com> <48bd0003$1@news.post.ch> <12prmxev8newf.lvc4m055okkb$.dlg@40tude.net> <1vmbk6d18az86$.hfgj8yjrvho8$.dlg@40tude.net> Reply-To: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: tigger.scc.uni-weimar.de 1220593540 28736 141.54.178.228 (5 Sep 2008 05:45:40 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Fri, 5 Sep 2008 05:45:40 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1vmbk6d18az86$.hfgj8yjrvho8$.dlg@40tude.net> Xref: g2news2.google.com comp.lang.ada:7659 Date: 2008-09-05T08:57:29+02:00 List-Id: On Thu, 4 Sep 2008, Dmitry A. Kazakov wrote: > There is absolutely no reason to sacrifice purity for impurity. Fine! ;-) > > If A is false, the expression is false, whatever B does. > > If A raises an exception, of if A is true and B raises an exception, > > the exception is propagated. > > 1 /\ T = T (it works!) > > As you see the theory works fine, even if you don't like it. > > Anyway now I see what you want. That is (more or less formally): > > Boolean'Base is Belnap logical values. All Boolean expressions are > evaluated in Boolean'Base, as it is already done for numeric types. Nothing > drastically new. (Compare also how Float overflow is converted to IEEE > Infinity.) Like universal numbers, Boolean'Base may have no variables > declared. > > (*) Funny problem: *Which* exception should be propagated? > > This is not funny. This one kills the idea, unless you forcefully convert > all exceptions into Constraint_Error, when a non-Boolean value is converted > to Boolean. If I would actually propose something like that, I would probably propose to raise Program_Error if the exceptions aren't all the same. > But the main problem is that this is not what people want. They do lazy > evaluation in order to control side effects (and exception is considered > rather as a side effect). Well, exceptions are treated like side effects, but they actually are something different. E.g., pure functions are free from "real" side effects, but they can still raise an exception. Even if you employ the SPARK verifier, you can be sure that no Constraint_Error occurs, but you still don't know about Storage_Error. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------