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: a07f3367d7,39579ad87542da0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.224.215.194 with SMTP id hf2mr22405204qab.0.1368583806214; Tue, 14 May 2013 19:10:06 -0700 (PDT) Path: y6ni44342qax.0!nntp.google.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.etla.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Sat, 11 May 2013 14:25:28 +0200 Organization: cbb software GmbH Message-ID: <16dmf6mnhdcxa.4khisjas6rut.dlg@40tude.net> References: <1msoad3apbkf.1optea1ujjydv.dlg@40tude.net> <357683977389964588.963651rm-host.bauhaus-maps.arcor.de@news.arcor.de> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: 15waz9CoS+eMakbyhTPyFQ.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-05-11T14:25:28+02:00 List-Id: On 11 May 2013 11:49:12 GMT, Georg Bauhaus wrote: > "Dmitry A. Kazakov" wrote: > >> The condition is moved to the post-condition. E.g. >> >> # require X >= 0.0 >> function sqrt (X : Float) return Float; >> # ensure sqrt (X)**2 = X >> >> is replaced with >> >> # require true >> function sqrt (X : Float) return Float; >> # ensure sqrt (X)**2 = X or else Constraint_Error raised > > So sqrt tests X for being non-negative and raises C_E otherwise? > Can the test be turned off? It is not test, it is a behavior. However if sqrt were inlined, at least partially, one branch of "if" could be removed if its condition proved static. > # require true > procedure increase_pressure (P : in out Pot; X : Float); > # ensure pressure (P) = X * pressure (P'old) or else Kaboom raised > > So where goes the precondition of the second kind mentioned > earlier, for calls, the one that is needed for correctness of the program? Is it a physical system you are talking about? In that case it does not work this way. You have a hardware in the [control] loop (HIL). E.g. a valve, a boiler, whatever. You set the valve using an actuator, you control its position using position sensors, you control pressure using pressure sensors, you control things using indirect measures, e.g. of the temperature etc. There is a model of the system according to which you act and react. It is very different from digital deterministic systems where cause and effect are tied to the point of being equivalent. > I take it that the former kind of precondition prevents Kaboom in the > system? By not raising it. So long the model is adequate [as estimated though the sensors] you don't raise anything. When the model is no more adequate you drive the system into a definite state as specified by the requirements, e.g. by doing an emergency shutdown. This procedure may be implemented using exceptions. In some cases definite state is achieved by self destruction (see Ariane). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de