On contracts and implementations

On contracts and implementations

[G.B.]

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.

Re: On contracts and implementations

[Peter C. Chapin]

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

Re: On contracts and implementations

[Dmitry A. Kazakov]

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

Re: On contracts and implementations

[G.B.]

On 11.07.13 16:15, Dmitry A. Kazakov wrote:
> Since contract checks may have no
> effect on program semantics, they cannot be executable.

If the only effect that contract checks may have on program
semantics is to STOP them, they can be executable in read-only
mode as described.

Re: On contracts and implementations

[Randy Brukardt]

"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.