Re: Tests in a software release

["G.B." <bauhaus@notmyhomepage.invalid>]

On 31.10.17 09:32, Dmitry A. Kazakov wrote:

> Implementation of bounds check = implementation of contract on bounds check.

To declare that the different names of different
things shall mean the same is one way of cutting
the Gordian knot.


> Checks can be removed only when statically proven not to fail.

Programmers may remove checks whenever they think
they should. No fancy proof is required(*).

> This is called optimization.

Optimization means that a compiler translates
source text using different algorithms.

Contracts between clients and suppliers do not
need a compiler. They do not require source text.
They need a lawyer. No, I am not joking.

>  The point is that any run-time check is behavior of the callee and cannot be argued something belonging to the caller or to whatever else.

Checks have actually belonged to something else,
on useful hardware, as has been explained in the past.

But your description of typical translations of
Ada programs that carry checks is about today's checks
in GNAT output. It's not even about contracts, which
are a purely legal thing between parties.

__
(*) It has been proven is that programs proven correct
will of necessity be rare or impractical.