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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Samuel Tardieu Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: #1/1 X-Deja-AN: 257441747 Sender: tardieu@esmeralda.enst.fr References: <33CD1722.2D24@calfp.co.uk> <33CE082E.65FF@calfp.co.uk> <33CE0BB7.10CE@XYZZYcalfp.com> Mail-Copies-To: sam@ada.eu.org Organization: TELECOM Paris Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: >>>>> "Richie" == Richie Bielak writes: Richie> I always thought it would be nice to have postconditions of Richie> the form: Richie> ensure Richie> execution_time < 10 -- 10 milliseconds, let's say Richie> So an exception would be raised if the routine took too long Richie> to execute. Well, I find the corresponding Ada code readable enough: select delay 0.010; -- The 10ms you were talking about raise Timeout_Failure; -- Raise an exception, or do anything else -- you need (use a fast version of -- your computation for example). then abort [...your code here...] -- This piece of code will be -- aborted if it is not terminated within -- the 10ms you required above. end select; And I don't think this should be a pre or post-condition, since it is not something which will be checked at the beginning or at the end of the job, but something which will indirectly interact with it (the job will be potentially aborted). Sam -- Samuel Tardieu -- sam@ada.eu.org