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: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: dewar@merv.cs.nyu.edu (Robert Dewar) Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp: process issue?) Date: 1997/09/12 Message-ID: #1/1 X-Deja-AN: 271984435 References: <33E9ADE9.4709@flash.net> <5upe9k$7he@newshub.atmnet.net> <5utag9$o6s@newshub.atmnet.net> <3416ad14.0@news.uni-ulm.de> <3416D889.4A6C@pseserv3.fw.hac.com> Organization: New York University Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-09-12T00:00:00+00:00 List-Id: Wes said >I claimed before (perhaps wrongly) that adding assertions to Ada >seemed fairly trivial, but even if correct, there is one aspect >that would NOT be trivial. Since an Eiffel-style assertion is >part of the contract, BUT it is executed when a routine is called, >how can it be put in an Ada spec in a form that is compilable AND >associated with a particular declaration? It seems pretty easy to devise a pragma that would have the desired effect, for example something like: procedure x (a : integer; b : integer); pragma Precondition (x, a = b + 17); which would say that this precondition on the parameters should be checked whenever the procedure is called. I don't see a problem in either defining or implementing such a pragma (this does not mean that it is zero work, or that we are about to rush away and add this feature to GNAT, but there is no conceptual or significant practical problem in implementing such a design.