Re: Tests in a software release

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2017-10-31 08:17, G.B. wrote:
> 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?

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

It is called tautology.

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

That is what I said. Checks can be removed only when statically proven 
not to fail. This is called optimization.

If in the IF-statement the condition is proven statically true, the 
ELSE-part can be removed. Just same.

Ada could have a pragma to remove all ELSE parts of all IF-statements. 
Would anybody argue for that? (:-))

> Disabling Ada checks means to rely on this contract.

It relays on proven properties of the program.

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

Sure. Contract only limits behavior it does not specify it. 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. Body may be not 
all behavior, e.g. if the check happens on the caller's side of the call.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de