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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: "David K Allen" Subject: Re: Interresting thread in comp.lang.eiffel Date: 2000/07/13 Message-ID: #1/1 X-Deja-AN: 645930759 References: <8ipvnj$inc$1@wanadoo.fr> <8j67p8$afd$1@nnrp1.deja.com> <395886DA.CCE008D2@deepthought.com.au> <3958B07B.18A5BB8C@acm.com> <395A0ECA.940560D1@acm.com> <8jd4bb$na7$1@toralf.uib.no> <8jfabb$1d8$1@nnrp1.deja.com> <8jhq0m$30u5$1@toralf.uib.no> <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de> <3963CDDE.3E8FB644@earthlink.net> <3963DEBF.79C40BF1@eiffel.com> <2LS85.6100$7%3.493920@news.flash.net> <8k5aru$1odtq$1@ID-9852.news.cis.dfn.de> <8k8pk2$20cab$1@ID-9852.news.cis.dfn.de> <_dS95.9945$7%3.666180@news.flash.net> <396C9C7F.D9B20E5F@baesystems.com> <396DA53D.19DDBACE@baesystems.com> X-Priority: 3 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 X-Complaints-To: abuse@visi.com X-Trace: ptah.visi.com 963501070 209.98.239.164 (Thu, 13 Jul 2000 10:11:10 CDT) X-MSMail-Priority: Normal NNTP-Posting-Date: Thu, 13 Jul 2000 10:11:10 CDT Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-13T00:00:00+00:00 List-Id: > David Gillon wrote: > > > One thing I'm still waiting to hear in this discussion is how [DBC] > > would handle a temporal constraint of the type 'Signal A will be updated > > with its new value within 2.5 ms of a change to any of its source > > inputs'. That is easy in theory, there is no magic here. You can do this in any language, and many probably have. But there is a cost to the calculation. In time-sensitive applications, the cost of calculating the answer may exceed the cost to do the calculation ;) I have no magic solution for that. Obviously this technique can only be practical when the cost of calculating the duration is immaterial compared to the cost of the process being measured. Although I will say that if these time-sensitive routines were in an embedded, real-time situation, then the 'timer'object shown below, could be a hardware timer that was dedicated to just such a task, so the measurement apparatus would have a negligible effect on the overall calculation in many cases. Also, someone else asked "What if my routine does not like the allowed duration chosen? Am I stuck with it failing, even though I might have wanted the answer even if it came later?" I will illustrate how to work around that. Assume a function 'signal' as follows: ------------------------------ signal (input: REAL): REAL is -- return 'signal' based upon 'input' require input_non_negative: input >= 0 do timer.start .... timer.stop ensure signal_valid: (input > 0) implies (Result > 0) and (input = 0) implies (Result = 0) duration_within_tolerance: timer.duration <= Max_Allowed_Duration end ------- This illustrates how DBC can be used in the 'ensure' clause to enforce the timing constraint Notice also that the reference point 'Max_Allowed_Duration' is a variable, to allow flexibility in application. This addresses the issue someone else raised (I could not find the post, but it was within the last few days). For a client to set this allowable duration to a value appropriate for the application, one merely writes a routine: ----------------------------------------- set_max_allowed_duration (d: REAL) is -- allow client routines to set the 'Max_Allowed_Duration' to suite their requirements require duration_valid: d > 0.01 do ... ensure Max_Allowed_Duration = d end -------------------------------------------- Or you could also have a feature pair 'disable_time_limit', and 'enable_time_limit' where do the obvious. What do you think of this approach? Can anyone think of better ways to model limits to duration in DBC? -- Best Wishes, David Kreth Allen Software Consultant Minneapolis, Minnesota - USA