From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 12 May 2015 11:39:11 -0700
Date: 2015-05-12T11:39:11-07:00 [thread overview]
Message-ID: <8738311vzk.fsf@jester.gateway.sonic.net> (raw)
In-Reply-To: alpine.DEB.2.11.1505120951500.17718@debian
Stefan.Lucks@uni-weimar.de writes:
> Either I write it as a second-class precondition in the form of a
> comment, or as a fist-class precondition using the "pre" attribute, or
> something similar ("unchecked_pre" or whatever). I'd prefer the
> second, because the compiler will tell me if my precondition is
> syntactically correct.
I'd say the first-class precondition (if executable) is also better
because even if a runtime check (say for an array being sorted) is too
expensive to use in a deployed application, you can still enable the
check during testing and pay the runtime cost, possibly finding some
bugs that way.
>> I disagree, actually. I think any useful postcondition has to be
>> reasonably executable. Else there is no difference from a comment,
Don't you want {pre,post}conditions to be able to quantify over infinite
ranges, and therefore not always be executable? For example, consider a
compiler optimization pass expressed as a function that takes a code
fragment and returns a new code fragment: the postcondition is that both
fragments have the same semantics, which means for all inputs, both
fragments compute the same result. That postcondition is not executable
but it is (example: CompCert) potentially provable. So wanting to state
and prove it is a legitimate desire.
> I don't care much about the syntax, some "unchecked_pre",
> "unchecked_post" attributes would be perfectly fine.
You could have a static precondition that accepts proof by assertion,
like in Coq where you can say "admitted".
>> Like everyone, I want it all, for free, right now. :-) Only Ada comes
>> close, and I just want to make it closer.
> Violent agreement, again!
Do you use other verification systems like Coq? Are the ones used with
Ada comparable at all?
next prev parent reply other threads:[~2015-05-12 18:39 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 [this message]
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
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