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.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC 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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Nick Leaton Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/19 Message-ID: <33F9C6D5.D7C84F67@calfp.co.uk>#1/1 X-Deja-AN: 267954247 References: <5siqrr$3of@jupiter.milkyway.org> <5smgts$p68$1@miranda.gmrc.gecm.com> <33EFCCE4.4CE0@flash.net> <5sq3fh$frg@wdl1.wdl.lmco.com> Reply-To: nickle@pauillac X-NNTP-Posting-Host: calfp.demon.co.uk [158.152.70.168] Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-19T00:00:00+00:00 List-Id: Robert Dewar wrote: > > Mark says > > < you can always just use the assertion "true" :-). > You can't even make using the assertion "true" illegal as there are > cases where the assertion "true" is exactly the correct assertion to > use; for example, using "true" as a precondition for a method documents the > fact that it has NO enviromential requirements at all. (E.G. a random > number routine or the Unix exit() call). And, what is the postcondition > for printf()?>> Well if we take the Eiffel equivalents of printf, which are put_string, put_integer ... Basically put_. We can come up with sensible postconditions. Since we are writting to a file, and let us assume we have have a method called file_position, which returns the position in the file. For put_string we have ensure old file_position + string.count = file_position Since other routines are likely to use this to output the formatted values that means the other postconditions are to be found in the formatting routines, where they belong. > As for the last question, this is just the tip of the iceburg. Of course it > is not the case that all requirements can be caught by pre and post conditions. Agreed, but you should be breaking your requirements down into smaller parts. Some are expressable, but wise to do. Membership of collections is one, and specifying the postcondition of a sorted collection is also not a wise postcondition to add. If you were writing a library they may be a wise addition. Running them in production code wouldn't be. It is too inefficient. > The idea of using pre and post conditions and assertions is very old. It > is useful but by no means applicable in all cases. > > What should be the post condition after outputting an error message > from a compiler? > pragma Assert (programmer now understands what they did wrong); > > You need a *really* clever language to test that one (well I suppose the > assertion routine executed at runtime could ask the programmer whether > he understood :-) Please explain? -- Nick