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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.241.162 with SMTP id wj2mr8945481pbc.2.1340729309700; Tue, 26 Jun 2012 09:48:29 -0700 (PDT) Path: l9ni22614pbj.0!nntp.google.com!news2.google.com!goblin3!goblin.stu.neva.ru!news.tu-darmstadt.de!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Tue, 26 Jun 2012 18:48:05 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:13.0) Gecko/20120614 Thunderbird/13.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net> <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net> <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net>

<4fe9bde5$0$6566$9b4e6d93@newsspool4.arcor-online.net> In-Reply-To: Message-ID: <4fe9e7c5$0$6567$9b4e6d93@newsspool4.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 26 Jun 2012 18:48:05 CEST NNTP-Posting-Host: 4be7f59d.newsspool4.arcor-online.net X-Trace: DXC=QV\DHL_KLkD@Y=h<_c3PkH4IUKJLh>_cHTX3jMd^WN96<_CmN X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2012-06-26T18:48:05+02:00 List-Id: On 26.06.12 16:45, Dmitry A. Kazakov wrote: > On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote: > >> On 26.06.12 15:07, Dmitry A. Kazakov wrote: >> >>> They are contracts when checked statically and implementations when checked >>> dynamically. >> >> What do pre/post implement, if so, in your view? > > if Pre(...) then > > if Post(...) then > null; > else > raise Constraint_Error; > end if; > else > raise Constraint_Error; > end if; There is a different understanding of "implement". Pre/Post do not implement anything essential. is supposed to implement something that essentially agrees with Pre/Post. Some confusion here, I think. >>> Contract violation => terminate. Exceptional state => recover. >> >> How does a client do make the program recover if an exception >> stands for "unforeseen"? > > How does a client recover if X contains 3 rather than 1? > > Answer: it recovers by continuing its program further. In a truly exceptional situation, as opposed to when there is a catch-all "special value", there is no contract that could have been violated, because the contract does not in any way cover the situation There is no known good value contained in X, for example, because there is no (practically) meaningful state. For this truly exceptional situation, which is necessarily unforeseen (otherwise it could have been covered by the contract), I'd include Exception(foreseeable) => recover. Exception(unforeseen) => STOP. Unforeseen is a modest word for "the exception handling mechanism might be broken in this situation". However, Exception(foreseeable) would include violations of Ada-Pre/Ada-Post, unless checking these results in Exception(unforeseeable).