From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: {Pre,Post}conditions and side effects
Date: Wed, 13 May 2015 20:21:39 -0500
Date: 2015-05-13T20:21:39-05:00 [thread overview]
Message-ID: <mj0tb3$pq1$1@loke.gir.dk> (raw)
In-Reply-To: miusk8$ife$1@dont-email.me
"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message
news:miusk8$ife$1@dont-email.me...
> On 13.05.15 00:37, Randy Brukardt wrote:
>> "Bob Duff" <bobduff@theworld.com> wrote in message
>> news:87egml511m.fsf@theworld.com...
>>> "Randy Brukardt" <randy@rrsoftware.com> writes:
>>>
>>>> I can see that are some cases where the properties are too expensive to
>>>> verify at runtime. It would be nice if there was a way to turn off
>>>> those
>>>> (AND ONLY THOSE) properties. But Ada doesn't have that sort of
>>>> granularity,
>>>
>>> Sure it does. If Is_Sorted is too slow for production use, you can say:
>>>
>>> ... with Predicate => (if Slow_Mode then Is_Sorted(...))
>>>
>>> and set the Slow_Mode flag to True for testing. Also set it to True
>>> when running proof tools.
>>
>> Of course. That's essentially what I've ("we've", really, Isaac created a
>> lot of the tracing stuff in Janus/Ada) been doing for years. I just
>> hadn't
>> thought of trying to use it directly in the assertions. We'd use a
>> function
>> call, though, rather than a constant:
>>
>> ... with Dynamic_Predicate => (if JTrace.Trace(Current_Unit) then
>> Is_Sorted(...))
>
> Given this fine-grained run-time configuration (another IF and then
> a little something like a debugging thing from an implementation),
> is the condition in the same category of expressions as Is_Sorted?
>
> The second, Is_Sorted, is strictly about the parameters, contractual,
> so to speak. The first looks rather different and distracting to me.
I think I made that point in my original message; this looks rather heavy
and hurts the readability of the predicates. But that certainly could be
reduced by naming and defaults.
-- At the start of the package:
Check : renames JTrace.Trace(Current_Unit);
... with Dynamic_Predicate => (if Check then Is_Sorted(...))
That certainly depends upon your needs; I typical use 3 or 4 levels of
tracing crosscut with subsystem or package level control. That might be
overkill for many, and perhaps Bob's direct solution would be enough for
you.
Randy.
next prev parent reply other threads:[~2015-05-14 1:21 UTC|newest]
Thread overview: 107+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-12-22 16:22 {Pre,Post}conditions and side effects Jean François Martinez
2014-12-22 17:18 ` Brad Moore
2014-12-23 8:22 ` Jean François Martinez
2014-12-23 17:05 ` Robert A Duff
2014-12-23 21:09 ` Jean François Martinez
2014-12-23 21:35 ` Robert A Duff
2014-12-23 23:02 ` Peter Chapin
2014-12-24 1:03 ` Robert A Duff
2015-04-24 8:59 ` Jacob Sparre Andersen
2015-04-24 9:18 ` J-P. Rosen
2015-04-24 23:39 ` Randy Brukardt
2015-04-24 12:10 ` G.B.
2015-04-24 14:40 ` Jacob Sparre Andersen
2015-04-24 16:29 ` G.B.
2015-04-24 23:46 ` Randy Brukardt
2015-04-24 22:26 ` Peter Chapin
2015-04-25 0:13 ` Randy Brukardt
2015-04-25 1:01 ` Peter Chapin
2015-04-25 5:51 ` Dmitry A. Kazakov
2015-04-25 0:31 ` Bob Duff
2015-04-25 12:08 ` vincent.diemunsch
2015-04-25 16:37 ` Georg Bauhaus
2015-05-06 21:07 ` Randy Brukardt
2015-05-06 22:10 ` Paul Rubin
2015-05-07 9:01 ` Georg Bauhaus
2015-05-07 9:12 ` Dmitry A. Kazakov
2015-05-07 9:29 ` Georg Bauhaus
2015-05-07 9:31 ` Georg Bauhaus
2015-05-07 18:32 ` Randy Brukardt
2015-05-08 7:50 ` Dmitry A. Kazakov
2015-05-08 23:31 ` Randy Brukardt
2015-05-09 6:16 ` Dmitry A. Kazakov
2015-05-12 0:28 ` Randy Brukardt
2015-05-12 8:04 ` Dmitry A. Kazakov
2015-05-07 10:06 ` Stefan.Lucks
2015-05-07 12:16 ` Dmitry A. Kazakov
2015-05-07 18:00 ` Stefan.Lucks
2015-05-07 19:01 ` Randy Brukardt
2015-05-07 19:29 ` Niklas Holsti
2015-05-08 23:16 ` Randy Brukardt
2015-05-09 5:18 ` Niklas Holsti
2015-05-12 0:15 ` Randy Brukardt
2015-05-07 19:55 ` Dmitry A. Kazakov
2015-05-08 23:24 ` Randy Brukardt
2015-05-09 5:47 ` Dmitry A. Kazakov
2015-05-07 18:52 ` Randy Brukardt
2015-05-07 19:40 ` Stefan.Lucks
2015-05-08 7:28 ` Dmitry A. Kazakov
2015-05-08 22:58 ` Randy Brukardt
2015-05-08 22:52 ` Randy Brukardt
2015-05-09 0:14 ` Paul Rubin
2015-05-12 0:30 ` Randy Brukardt
2015-05-12 18:10 ` Paul Rubin
2015-05-12 22:01 ` Randy Brukardt
2015-05-13 9:35 ` Dmitry A. Kazakov
2015-05-13 11:53 ` G.B.
2015-05-13 12:47 ` Dmitry A. Kazakov
2015-05-13 14:06 ` G.B.
2015-05-13 14:21 ` Dmitry A. Kazakov
2015-05-13 16:33 ` G.B.
2015-05-13 19:15 ` Dmitry A. Kazakov
2015-05-14 1:36 ` Randy Brukardt
2015-05-14 7:10 ` Dmitry A. Kazakov
2015-05-14 1:32 ` Randy Brukardt
2015-05-14 7:19 ` Dmitry A. Kazakov
2015-05-12 0:36 ` Randy Brukardt
2015-05-11 10:35 ` Stefan.Lucks
2015-05-11 21:49 ` vincent.diemunsch
2015-05-11 22:49 ` Peter Chapin
2015-05-12 4:49 ` vincent.diemunsch
2015-05-12 23:25 ` Peter Chapin
2015-05-13 9:00 ` vincent.diemunsch
2015-05-12 4:42 ` vincent.diemunsch
2015-05-12 14:53 ` johnscpg
2015-05-13 9:14 ` vincent.diemunsch
2015-05-12 1:03 ` Randy Brukardt
2015-05-12 7:21 ` Georg Bauhaus
2015-05-12 22:08 ` Randy Brukardt
2015-05-12 8:02 ` Georg Bauhaus
2015-05-12 22:14 ` Randy Brukardt
2015-05-12 8:37 ` Stefan.Lucks
2015-05-12 11:25 ` Stefan.Lucks
2015-05-12 18:44 ` Paul Rubin
2015-05-12 20:52 ` Stefan.Lucks
2015-05-18 9:49 ` Jacob Sparre Andersen
2015-05-18 12:10 ` Stefan.Lucks
2015-05-19 7:46 ` Jacob Sparre Andersen
2015-06-09 7:55 ` Stefan.Lucks
2015-06-09 12:02 ` G.B.
2015-06-09 17:16 ` Stefan.Lucks
2015-05-12 18:39 ` Paul Rubin
2015-05-12 20:51 ` Stefan.Lucks
2015-05-12 14:21 ` Bob Duff
2015-05-12 22:37 ` Randy Brukardt
2015-05-13 6:58 ` Georg Bauhaus
2015-05-14 1:21 ` Randy Brukardt [this message]
2015-05-07 21:29 ` Georg Bauhaus
2015-05-08 23:11 ` Randy Brukardt
2015-05-08 23:19 ` tmoran
2014-12-23 21:53 ` Florian Weimer
2014-12-24 11:41 ` Brad Moore
2014-12-22 19:38 ` sbelmont700
2014-12-22 19:59 ` Brad Moore
2014-12-22 23:46 ` Randy Brukardt
2014-12-23 10:41 ` Georg Bauhaus
2014-12-22 23:32 ` Randy Brukardt
2015-04-24 17:59 ` Shark8
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox