Re: Tests in a software release

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

On 30.10.17 21:56, Dmitry A. Kazakov wrote:
> On 2017-10-30 21:44, G. B. wrote:
>> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>>> On 2017-10-28 08:53, G.B. wrote:
>>>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>>>> The contract requires Constraint_Error propagation.
>>>>
>>>> Checks require Constraint_Error propagation.
>>>
>>> Checks ensure Constraint_Error as a part of implementation.
>>
>> Implementation of checks, not of contracts.
> 
> This is exactly same.

So, Ada programs will check theirs checks?

Expectations can be stated in comments,
or be part of accompanying documentation and still
be part of a contract.

> There is nothing that is not behavior.

Checking is behavior. However, let SPARK check conditions
of a contract, and let the result be Truth. Then they
have been checked before the program even runs, and
turning *off* Ada checks is, therefore, justified.

Disabling Ada checks means to rely on this contract.

> There is nothing that may not fall under the contract.

There are very many things, even in a program,
that do exist, exhibit behavior, but are not
part of any known, non-fictional contract, such as
the transitive closure of an unspeakable hypothesis.