* On contracts and implementations
@ 2013-07-11 9:35 G.B.
2013-07-11 11:56 ` Peter C. Chapin
0 siblings, 1 reply; 5+ messages in thread
From: G.B. @ 2013-07-11 9:35 UTC (permalink / raw)
There is a claim that contracts of Ada 2012 are part of the
implementation. They are not.
Assuming that they are part of the implementation is a misconception
about designing with contracts.
The contract idea is, rather, to make engineers not program
defensively, but to agree on a contract that states what is
true. The word "Contract" as we know it: to call the post-hoc
conditions of a program's state a "contract" would be a misnomer.
Technically, contracts can be evaluated on separate hardware #2,
controlling hardware #1. The following program is an example.
"Subtract a non-negative number from a non-negative number"
P0: LOAD Input, R1
LOAD Input, R2
$TRNSFR #2
BLT R1, 0, [T1]
BLT R2, 0, [T1]
BGE R1, 0, [P1]
T1: $STOP #1
$STOP #2
P1: $TRNSFR #1
SUB R2, R1, R0
Hardware #2 gets a copy of the register words of #1, and a read-only
copy of the program and its memory.
Then, the program that harware #1 runs, is, essentially,
P0: LOAD Input, R1
LOAD Input, R2
SUB R2, R1, R0
This is efficient, since defensive checking is gone: once the program
has been shown to be correct, $TRNSFR may mean to just skip the tests.
As always, if engineers decide to plant side effects into predicates,
they are on their own.
Sorry for the steam, but it is perhaps a good idea to state that it is
the engineers who take responsibility for writing proper contracts,
and then using them.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: On contracts and implementations
2013-07-11 9:35 On contracts and implementations G.B.
@ 2013-07-11 11:56 ` Peter C. Chapin
2013-07-11 14:15 ` Dmitry A. Kazakov
2013-07-12 21:30 ` Randy Brukardt
0 siblings, 2 replies; 5+ messages in thread
From: Peter C. Chapin @ 2013-07-11 11:56 UTC (permalink / raw)
On 07/11/2013 05:35 AM, G.B. wrote:
> There is a claim that contracts of Ada 2012 are part of the
> implementation. They are not.
I think the litmus test for contract code vs "ordinary" code is that the
contracts should be removable without changing the functional behavior
of the program. This means that any checks of errors arising from the
execution environment, such as missing files or bad user input, can't be
in contracts.
It is important to be able to remove contracts for performance reasons.
I'm not talking about the constant time overhead of extra range checks.
I'm talking about major performance costs.
For example a binary search function might reasonably have a pre-
condition that states the input array is sorted. Checking that contract
requires O(n) time and is thus asymptotically slower than the function
itself. One might be able to tolerate that during testing on small data
sets. Furthermore it would be useful to be able to prove that nowhere is
the function called with an unsorted array. However, it is unlikely that
the deployed program could tolerate the slow down in asymptotic running
time. On a full sized data set we might be talking about a 1,000,000x
reduction in speed!
Peter
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: On contracts and implementations
2013-07-11 11:56 ` Peter C. Chapin
@ 2013-07-11 14:15 ` Dmitry A. Kazakov
2013-07-11 16:14 ` G.B.
2013-07-12 21:30 ` Randy Brukardt
1 sibling, 1 reply; 5+ messages in thread
From: Dmitry A. Kazakov @ 2013-07-11 14:15 UTC (permalink / raw)
On Thu, 11 Jul 2013 07:56:02 -0400, Peter C. Chapin wrote:
> On 07/11/2013 05:35 AM, G.B. wrote:
>
>> There is a claim that contracts of Ada 2012 are part of the
>> implementation. They are not.
>
> I think the litmus test for contract code vs "ordinary" code is that the
> contracts should be removable without changing the functional behavior
> of the program. This means that any checks of errors arising from the
> execution environment, such as missing files or bad user input, can't be
> in contracts.
Right
> It is important to be able to remove contracts for performance reasons.
> I'm not talking about the constant time overhead of extra range checks.
> I'm talking about major performance costs.
It is in contradiction with the above. Since contract checks may have no
effect on program semantics, they cannot be executable. Of course they can
be removed, because they never were inserted in first place.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: On contracts and implementations
2013-07-11 11:56 ` Peter C. Chapin
2013-07-11 14:15 ` Dmitry A. Kazakov
@ 2013-07-12 21:30 ` Randy Brukardt
1 sibling, 0 replies; 5+ messages in thread
From: Randy Brukardt @ 2013-07-12 21:30 UTC (permalink / raw)
"Peter C. Chapin" <PChapin@vtc.vsc.edu> wrote in message
news:ieWdnXSAKPXPAEPMRVn_vwA@giganews.com...
...
> I think the litmus test for contract code vs "ordinary" code is that the
> contracts should be removable without changing the functional behavior of
> the program. This means that any checks of errors arising from the
> execution environment, such as missing files or bad user input, can't be
> in contracts.
>
> It is important to be able to remove contracts for performance reasons.
> I'm not talking about the constant time overhead of extra range checks.
> I'm talking about major performance costs.
>
> For example a binary search function might reasonably have a pre-
> condition that states the input array is sorted. Checking that contract
> requires O(n) time and is thus asymptotically slower than the function
> itself. One might be able to tolerate that during testing on small data
> sets. Furthermore it would be useful to be able to prove that nowhere is
> the function called with an unsorted array. However, it is unlikely that
> the deployed program could tolerate the slow down in asymptotic running
> time. On a full sized data set we might be talking about a 1,000,000x
> reduction in speed!
I understand your point, but I think it's short-sighted to think about
removing the contracts. If you do so, then the contracts can't be used to
"hoist" what otherwise have to be checks in the code (as in Text_IO, the
containers, and many other packages). Turning off these checks in
language-defined code is a complete non-starter, the result would not meet
the language specifications (and would introduce erroneousness where none
currently exists).
Secondly, as compiler's proof abilities increase, most of these contract
assertions will disappear. The compiler will be able to prove that they
always will succeed, and thus no check will be made.
After all, this is the case with existing constraints and exclusions.
Compilers work overtime to eliminate unnecessary checks, and tend to remove
60-80% of the checks. It's rare that I see an explicit range check when I
examine generated code these days. The same should happen to assertion
checks (but only if they are well-written, using globals annotations and/or
expression functions).
To look further at your example, I agree that evaluating Is_Sorted could be
prohibitively expensive. But how did that object *get* sorted? One presumes
that it was explicitly sorted somewhere, in which case that routine has an
Is_Sorted postcondition. If the compiler can tie those together, there
certainly is no need to reevaluate the Is_Sorted on a following
precondition. Similarly, the compiler may have been able to prove that the
Is_Sorted postcondition is always true. In that case, that won't be executed
either. So you still will have the safety of checks on, and *still* have no
actual overhead.
Now, obviously, these things won't always be next to each other; the array
might have been a parameter. But in that case you can use a predicate to
ensure that that parameter Is_Sorted, pushing the optimization to another
level.
To summarize, I expect these to become much like range checks. You'll
sometimes have to suppress them, but it will be pretty rare, and often you
can add some subtypes in appropriate places to remove the checks rather than
actually suppressing them (the latter being more dangerous).
Randy.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2013-07-12 21:30 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-07-11 9:35 On contracts and implementations G.B.
2013-07-11 11:56 ` Peter C. Chapin
2013-07-11 14:15 ` Dmitry A. Kazakov
2013-07-11 16:14 ` G.B.
2013-07-12 21:30 ` Randy Brukardt
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox