From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Wed, 27 Jun 2012 17:08:57 +0200
Date: 2012-06-27T17:08:58+02:00 [thread overview]
Message-ID: <4feb220a$0$6580$9b4e6d93@newsspool3.arcor-online.net> (raw)
In-Reply-To: <2klq69d4qqsp$.veefi8i6jnwa.dlg@40tude.net>
On 27.06.12 14:19, Dmitry A. Kazakov wrote:
>> A and B can be shown to both be implementations of the behavior
>> that some contract stipulates.
>
> This is wrong on multiple accounts:
>
> 1. It cannot be shown: if Pre (HALT (p)) then ... else ... end if;
For run time parameters P1 and P2, and for static or dynamic K:
if P1 + P2 < K then ... else ... end if;
The client programmer sees Pre (P1 + P2 < K) in a spec. She or he will
make sure that all values passed as parameters will satisfy P1 + P2 < K,
QED.
If one programmer can write Pre (HALT (p)) then no programmer should
be able to read or write Pre (P1 + P2 < K)? This seems overly
restrictive because it prevents *working* towards a man made proof.
> 2. For any program there exist an infinite set of contracts satisfied by;
For any Ada 2012 program there exists just one relevant contract,
which is the contract explicitly stated using Ada with Pre/Post/Inv.
Any program satisfying this contract is fine.
> 3. It is irrelevant to whether both pieces are equivalent.
Equivalence of programs in terms of a given contract can be the goal.
I have given an example of a stack that shows essentially the
same behavior with checks on or off. That is,
if Pre (...) then Stmnts; else raise ...
vs
Stmnts;
The difference was in the quality of the error reports.
The "essential sameness" was that the same stack operations
would result in the same stacks.
From a business point of view, the programs fulfill the
necessary conditions of equivalence.
> I don't know what "essentially same effect" is, but whatever formal
> definition of essential you took you would have to prove that two programs
> are equivalent according to the definition. That will require proving that
> the exception is not propagated or else handled to an "essentially" same
> result. Good luck with that.
Wow, finally. ;-) With the addition of having the exception
stop the program according to Assertion_Policy, this is DbC,
a human activity that includes a proof obligation.
next prev parent reply other threads:[~2012-06-27 15:08 UTC|newest]
Thread overview: 125+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi
2012-06-20 14:02 ` Georg Bauhaus
2012-06-20 14:13 ` Dmitry A. Kazakov
2012-06-20 14:24 ` Nasser M. Abbasi
2012-06-20 14:37 ` Dmitry A. Kazakov
2012-06-20 17:02 ` Georg Bauhaus
2012-06-20 18:28 ` Dmitry A. Kazakov
2012-06-21 20:32 ` Randy Brukardt
2012-06-22 7:23 ` Dmitry A. Kazakov
2012-06-22 11:54 ` Georg Bauhaus
2012-06-22 12:39 ` Georg Bauhaus
2012-06-22 12:43 ` Dmitry A. Kazakov
2012-06-22 14:30 ` Georg Bauhaus
2012-06-22 14:36 ` Georg Bauhaus
2012-06-22 15:05 ` Dmitry A. Kazakov
2012-06-22 15:52 ` Georg Bauhaus
2012-06-22 16:35 ` Dmitry A. Kazakov
2012-06-22 16:53 ` Georg Bauhaus
2012-06-22 16:45 ` Georg Bauhaus
2012-06-22 17:24 ` Dmitry A. Kazakov
2012-06-22 19:41 ` Randy Brukardt
2012-06-22 23:08 ` Dmitry A. Kazakov
2012-06-23 10:46 ` Georg Bauhaus
2012-06-23 11:01 ` Dmitry A. Kazakov
2012-06-23 17:46 ` AdaMagica
2012-06-23 19:23 ` Dmitry A. Kazakov
2012-06-24 14:59 ` Georg Bauhaus
2012-06-24 16:06 ` Dmitry A. Kazakov
2012-06-24 19:51 ` Georg Bauhaus
2012-06-25 7:48 ` Dmitry A. Kazakov
2012-06-25 10:10 ` Georg Bauhaus
2012-06-25 8:08 ` Dmitry A. Kazakov
2012-06-25 10:17 ` Georg Bauhaus
2012-06-25 11:54 ` Dmitry A. Kazakov
2012-06-25 12:39 ` Georg Bauhaus
2012-06-25 12:51 ` Georg Bauhaus
2012-06-25 13:19 ` Dmitry A. Kazakov
2012-06-25 16:43 ` Georg Bauhaus
2012-06-25 14:08 ` stefan-lucks
2012-06-25 14:36 ` Dmitry A. Kazakov
2012-06-25 14:37 ` Dmitry A. Kazakov
2012-06-25 16:26 ` stefan-lucks
2012-06-25 19:42 ` Dmitry A. Kazakov
2012-06-26 11:50 ` stefan-lucks
2012-06-26 13:07 ` Dmitry A. Kazakov
2012-06-26 13:49 ` Georg Bauhaus
2012-06-26 14:45 ` Dmitry A. Kazakov
2012-06-26 16:48 ` Georg Bauhaus
2012-06-26 19:43 ` Dmitry A. Kazakov
2012-06-27 8:23 ` Georg Bauhaus
2012-06-27 8:52 ` Dmitry A. Kazakov
2012-06-27 10:30 ` Georg Bauhaus
2012-06-27 12:19 ` Dmitry A. Kazakov
2012-06-27 13:41 ` Nasser M. Abbasi
2012-06-28 7:00 ` Georg Bauhaus
2012-06-27 15:08 ` Georg Bauhaus [this message]
2012-06-29 21:03 ` Shark8
2012-06-30 8:26 ` Dmitry A. Kazakov
2012-06-30 12:54 ` Niklas Holsti
2012-07-05 2:58 ` Shark8
2012-07-05 7:24 ` Dmitry A. Kazakov
2012-07-06 6:23 ` Shark8
2012-07-06 7:57 ` Dmitry A. Kazakov
2012-07-07 1:09 ` Randy Brukardt
2012-07-07 8:44 ` Dmitry A. Kazakov
2012-06-26 14:54 ` stefan-lucks
2012-06-26 15:14 ` Dmitry A. Kazakov
2012-07-03 5:28 ` Randy Brukardt
2012-07-03 12:53 ` Dmitry A. Kazakov
2012-07-03 13:48 ` Georg Bauhaus
2012-07-03 14:06 ` Dmitry A. Kazakov
2012-07-03 16:12 ` Georg Bauhaus
2012-07-03 16:45 ` Georg Bauhaus
2012-07-05 1:45 ` Randy Brukardt
2012-07-05 7:48 ` Dmitry A. Kazakov
2012-07-05 19:11 ` Adam Beneschan
2012-07-05 19:55 ` Dmitry A. Kazakov
2012-07-06 7:41 ` Georg Bauhaus
2012-07-06 7:47 ` Georg Bauhaus
2012-07-06 8:05 ` Dmitry A. Kazakov
2012-07-06 8:30 ` Georg Bauhaus
2012-07-06 9:01 ` Dmitry A. Kazakov
2012-07-06 11:33 ` Simon Wright
2012-07-06 13:25 ` Dmitry A. Kazakov
2012-07-06 12:07 ` Georg Bauhaus
2012-07-06 13:37 ` Dmitry A. Kazakov
2012-07-06 16:17 ` Georg Bauhaus
2012-07-06 16:34 ` Georg Bauhaus
2012-07-06 19:18 ` Dmitry A. Kazakov
2012-07-07 1:24 ` Randy Brukardt
2012-07-07 9:09 ` Dmitry A. Kazakov
2012-07-07 1:18 ` Randy Brukardt
2012-07-07 9:14 ` Dmitry A. Kazakov
2012-07-07 12:06 ` Georg Bauhaus
2012-07-07 12:54 ` Dmitry A. Kazakov
2012-07-07 13:31 ` Georg Bauhaus
2012-07-03 5:10 ` Randy Brukardt
2012-07-03 4:51 ` Randy Brukardt
2012-07-03 12:46 ` Dmitry A. Kazakov
2012-07-05 2:18 ` Randy Brukardt
2012-07-05 8:48 ` Dmitry A. Kazakov
2012-07-05 12:07 ` Georg Bauhaus
2012-07-05 12:13 ` Georg Bauhaus
2012-07-05 12:31 ` Dmitry A. Kazakov
2012-07-05 18:16 ` Georg Bauhaus
2012-07-05 19:57 ` Dmitry A. Kazakov
2012-07-06 6:53 ` Georg Bauhaus
2012-07-07 0:43 ` Randy Brukardt
2012-07-07 8:06 ` Dmitry A. Kazakov
2012-07-07 11:17 ` Georg Bauhaus
2012-07-07 11:31 ` Dmitry A. Kazakov
2012-07-07 12:21 ` Georg Bauhaus
2012-07-07 13:03 ` Dmitry A. Kazakov
2012-06-20 19:18 ` Anh Vo
2012-06-20 20:16 ` Jeffrey R. Carter
2012-06-20 20:21 ` Jeffrey R. Carter
2012-06-20 20:51 ` Maciej Sobczak
2012-06-20 21:04 ` Dmitry A. Kazakov
2012-06-20 22:19 ` Robert A Duff
2012-06-21 6:32 ` Georg Bauhaus
2012-06-21 20:37 ` Randy Brukardt
2012-06-21 20:55 ` Jeffrey Carter
2012-06-22 19:15 ` Randy Brukardt
2012-06-21 20:23 ` Randy Brukardt
2012-06-22 7:34 ` Martin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox