comp.lang.ada
 help / color / mirror / Atom feed
From: "David K Allen" <dkallen@visi.com>
Subject: Re: Interresting thread in comp.lang.eiffel
Date: 2000/07/13
Date: 2000-07-13T00:00:00+00:00	[thread overview]
Message-ID: <i_kb5.878$6E.108485@ptah.visi.com> (raw)
In-Reply-To: 396DA53D.19DDBACE@baesystems.com

> 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








  reply	other threads:[~2000-07-13  0:00 UTC|newest]

Thread overview: 102+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <8ipvnj$inc$1@wanadoo.fr>
     [not found] ` <8j67p8$afd$1@nnrp1.deja.com>
     [not found]   ` <39573CAB.BB90DF92@gecm.com>
     [not found]     ` <8j8ek0$24la$3@ID-9852.news.cis.dfn.de>
     [not found]       ` <3957ED3E.E64E7390@lmco.com>
     [not found]         ` <8k8orn$1tlh9$1@ID-9852.news.cis.dfn.de>
     [not found]           ` <94S95.9936$7%3.667320@news.flash.net>
2000-07-13  0:00             ` Interresting thread in comp.lang.eiffel Joachim Durchholz
2000-07-14  0:00               ` Ken Garlington
2000-07-16  0:00                 ` Joachim Durchholz
2000-07-16  0:00                   ` Ken Garlington
     [not found]   ` <slrn8leffq.ebq.gisle@spurv.ii.uib.no>
     [not found]     ` <395886DA.CCE008D2@deepthought.com.au>
     [not found]       ` <3958B07B.18A5BB8C@acm.com>
     [not found]         ` <y1d65.620$7%3.33446@news.flash.net>
     [not found]           ` <395A0ECA.940560D1@acm.com>
     [not found]             ` <8jd4bb$na7$1@toralf.uib.no>
     [not found]               ` <8jfabb$1d8$1@nnrp1.deja.com>
     [not found]                 ` <SVH65.1596$7%3.129344@news.flash.net>
     [not found]                   ` <8jt4i0$18ec7$1@ID-9852.news.cis.dfn.de>
     [not found]                     ` <nSt85.5388$7%3.424540@news.flash.net>
     [not found]                       ` <8k5a31$1p61t$1@ID-9852.news.cis.dfn.de>
     [not found]                         ` <qlt95.7824$7%3.596314@news.flash.net>
     [not found]                           ` <3966D7B0.5D6475E4@earthlink.net>
     [not found]                             ` <A5J95.9237$7%3.638838@news.flash.net>
2000-07-12  0:00                               ` Robert I. Eachus
2000-07-13  0:00                                 ` Ken Garlington
2000-07-23  0:00                                   ` Robert I. Eachus
2000-07-23  0:00                                     ` Ken Garlington
2000-07-24  0:00                                       ` David Gillon
2000-07-24  0:00                                         ` Ken Garlington
2000-07-24  0:00                                       ` swhalen
2000-07-24  0:00                                     ` David Gillon
     [not found]                             ` <39688CA2.31B2A7EF@acm.com>
2000-07-13  0:00                               ` Joachim Durchholz
2000-07-13  0:00                                 ` Marin D. Condic
     [not found]                           ` <8k8p8m$1upjk$1@ID-9852.news.cis.dfn.de>
     [not found]                             ` <0cS95.9944$7%3.667682@news.flash.net>
2000-07-13  0:00                               ` Joachim Durchholz
2000-07-14  0:00                                 ` Ken Garlington
     [not found]                 ` <8jhq0m$30u5$1@toralf.uib.no>
     [not found]                   ` <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de>
     [not found]                     ` <3963CDDE.3E8FB644@earthlink.net>
     [not found]                       ` <8k5alv$1oogm$1@ID-9852.news.cis.dfn.de>
     [not found]                         ` <Rmt95.7825$7%3.595826@news.flash.net>
2000-07-13  0:00                           ` Joachim Durchholz
2000-07-13  0:00                             ` Marin D. Condic
2000-07-14  0:00                             ` Ken Garlington
2000-07-16  0:00                               ` Joachim Durchholz
2000-07-16  0:00                                 ` Ken Garlington
2000-07-19  0:00                                   ` Joachim Durchholz
2000-07-19  0:00                                     ` Ken Garlington
2000-07-14  0:00                             ` Ken Garlington
2000-07-14  0:00                               ` Marin D. Condic
2000-07-14  0:00                                 ` Ken Garlington
     [not found]                       ` <3963DEBF.79C40BF1@eiffel.com>
     [not found]                         ` <2LS85.6100$7%3.493920@news.flash.net>
     [not found]                           ` <8k5aru$1odtq$1@ID-9852.news.cis.dfn.de>
     [not found]                             ` <Rnt95.7826$7%3.596208@news.flash.net>
     [not found]                               ` <8k8pk2$20cab$1@ID-9852.news.cis.dfn.de>
     [not found]                                 ` <_dS95.9945$7%3.666180@news.flash.net>
2000-07-12  0:00                                   ` David K Allen
2000-07-12  0:00                                     ` David Gillon
2000-07-13  0:00                                       ` Joachim Durchholz
2000-07-13  0:00                                       ` David Gillon
2000-07-13  0:00                                         ` David K Allen [this message]
2000-07-13  0:00                                           ` Bob Allen
2000-07-13  0:00                                             ` Joachim Durchholz
2000-07-18  0:00                                               ` Veli-Pekka Nousiainen
2000-07-19  0:00                                                 ` Joachim Durchholz
2000-07-14  0:00                                         ` Ken Garlington
2000-07-18  0:00                                       ` Veli-Pekka Nousiainen
2000-07-19  0:00                                         ` David Gillon
2000-07-12  0:00                                     ` Bob Allen
2000-07-12  0:00                                       ` Ken Garlington
2000-07-13  0:00                                         ` Bob Allen
2000-07-14  0:00                                           ` Ken Garlington
2000-07-14  0:00                                             ` Marin D. Condic
2000-07-14  0:00                                             ` carr_tom
2000-07-18  0:00                                               ` Veli-Pekka Nousiainen
2000-07-12  0:00                                     ` Ken Garlington
2000-07-12  0:00                                       ` David K Allen
2000-07-13  0:00                                         ` Howard W. LUDWIG
2000-07-13  0:00                                           ` Joachim Durchholz
2000-07-14  0:00                                           ` Ken Garlington
2000-07-14  0:00                                         ` Ken Garlington
2000-07-18  0:00                                           ` Veli-Pekka Nousiainen
2000-07-19  0:00                                             ` Ken Garlington
2000-07-19  0:00                                               ` Bob Allen
2000-07-12  0:00                                       ` David K Allen
     [not found]                             ` <Rnt95.78 <L6vb5.16117$7%3.988701@news.flash.net>
2000-07-14  0:00                               ` Nick Williams
     [not found]                         ` <396502D2.BD8A42E7@earthlink.net>
     [not found]                           ` <RSsa5.11075$7%3.784507@news.flash.net>
     [not found]                             ` <6aHa5.113$6E.23141@ptah.visi.com>
     [not found]                               ` <396B4A68.458FA3BC@maths.unine.ch>
     [not found]                                 ` <u6hp4i16$GA.283@cpmsnbbsa07>
2000-07-11  0:00                                   ` Ken Garlington
2000-07-12  0:00                                     ` Peter Amey
2000-07-12  0:00                                       ` Peter Amey
2000-07-13  0:00                                       ` Joachim Durchholz
2000-07-12  0:00                                     ` Bob Allen
2000-07-12  0:00                                       ` Ken Garlington
2000-07-12  0:00                                       ` David Starner
2000-07-11  0:00                                   ` cropt
     [not found]                           ` <39654639.B3760EF2@eiffel.com>
     [not found]                             ` <i4k95.7512$7%3.571616@news.flash.net>
     [not found]                               ` <oqog45g1j0.fsf@premise.demon.co.uk>
     [not found]                                 ` <85Fa5.11419$7%3.818927@news.flash.net>
2000-07-11  0:00                                   ` Aspects (Re: Interesting thread in comp.lang.eiffel) tom
2000-07-12  0:00                                     ` Veli-Pekka Nousiainen
2000-07-12  0:00                                       ` tom
2000-07-12  0:00                                     ` Steve Merrick
2000-07-12  0:00                                       ` Frank Mitchell
2000-07-14  0:00                                         ` Jubilation
2000-07-14  0:00                                           ` Frank Mitchell
2000-07-15  0:00                                             ` Jubilation
2000-07-12  0:00                                   ` Design by Contract (was " David Kristola
2000-07-12  0:00                                     ` Greg
2000-07-12  0:00                                       ` Matthew J Heaney
2000-07-13  0:00                                         ` Eirik Mangseth
2000-07-12  0:00                                     ` Howard W. LUDWIG
2000-07-12  0:00                                       ` Greg
2000-07-12  0:00                                         ` Eirik Mangseth
2000-07-13  0:00                                       ` Joachim Durchholz
2000-07-14  0:00                                         ` David Kristola
2000-07-14  0:00                                           ` Matthew J Heaney
2000-07-16  0:00                                           ` Joachim Durchholz
2000-07-17  0:00                                             ` David Kristola
2000-07-19  0:00                                               ` Joachim Durchholz
2000-07-25  0:00                                                 ` Richard Riehle
2000-07-18  0:00                               ` Interesting thread in comp.lang.eiffel Veli-Pekka Nousiainen
2000-07-19  0:00                                 ` Ken Garlington
     [not found]                             ` <i4k95.7512$7%3.571616@n <397D8CC3.BB0C9001@ix.netcom.com>
2000-07-29  0:00                               ` Writing better software was: Design by Contract (was Re: Interesting thread in comp.lang.eiffel) Kent Paul Dolan
2000-07-29  0:00                                 ` Ken Garlington
2000-07-31  0:00                                   ` Stefan Skoglund
2000-08-01  0:00                                     ` Ken Garlington
2000-08-01  0:00                                   ` Kent Paul Dolan
2000-08-01  0:00                                     ` Ken Garlington
2000-07-31  0:00                                 ` Simon Brady
2000-07-30  0:00                                   ` John Magness
2000-08-01  0:00                                     ` Simon Brady
2000-08-01  0:00                                       ` Simon Brady
2000-08-04  0:00                                         ` Robert I. Eachus
2000-08-04  0:00                                           ` Simon Brady
2000-08-01  0:00                                       ` Ken Garlington
     [not found]   ` <8j7i54$j7d5@news.kvaerner.com>
     [not found]     ` <395887EB.8D612FC7@deepthought.com.au>
     [not found]       ` <395A190E.FD4D8978@easystreet.com>
     [not found]         ` <6Yt65.3417$MS3.72586@news1.online.no>
     [not found]           ` <395A7E7E.FE57E036@easystreet.com>
     [not found]             ` <8jermi$5cb2@news.kvaerner.com>
     [not found]               ` <395BCE66.2BE8EE0A@eiffel.com>
     [not found]                 ` <wccaeg3gj61.fsf@world.std.com>
     [not found]                   ` <395D113D.1F654A68@eiffel.com>
     [not found]                     ` <dus75.5086$MS3.105182@news1.online.no>
     [not found]                       ` <395E5D16.C4D109F1@eiffel.com>
2000-07-18  0:00                         ` Interesting thread in comp.lang.eiffel Veli-Pekka Nousiainen
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox