From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-65-14.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-3.2 required=3.0 tests=BAYES_00,NICE_REPLY_A,
	T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6
Path: eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Contracts in generic formal subprogram
Date: Tue, 11 Apr 2023 14:03:27 +0200
Organization: A noiseless patient Spider
Message-ID: <u13iae$2kj2n$1@dont-email.me>
References: <0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com>
 <u0r72o$16jtj$1@dont-email.me> <u12squ$2j3h0$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 11 Apr 2023 12:03:26 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="dcee31fe3801779a0057231ac5470c96";
	logging-data="2772055"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19vaBi0OaZfkOlevsJUMNeWtDW5hHXE5T8="
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.9.1
Cancel-Lock: sha1:SRShcFSwfE+j2VXsbmBevQpYk2Y=
In-Reply-To: <u12squ$2j3h0$1@dont-email.me>
Content-Language: en-US
Xref: feeder.eternal-september.org comp.lang.ada:65087
List-Id: <comp.lang.ada>

On 2023-04-11 07:56, G.B. wrote:
> On 08.04.23 10:02, Dmitry A. Kazakov wrote:
>> On 2023-04-08 09:00, mockturtle wrote:
>>
>>> Should the actual subprogram specify the same contract? I am not sure 
>>> (and I guess this could be a stumbling block for the adoption of this 
>>> idea).
>>
>> The general principle of substitutability is that the preconditions 
>> can be weakened, the postoconditions can be strengthened.
> 
> Side track: "weak" and "strong" alone sounding like a valuation to the
> uninitiated, but neither technical nor precise; and the "objects" of
> comparison of sets of conditions being implicit; and the ARM not
> defining a technical term for these adjectives unless weak ordering
> helps.

The formal meaning of weaker/stronger relation on predicates P and Q:

weaker   P => Q
stronger Q => P

The formal rationale is that if you have a proof

   P1 => P2 => P3

Then weakening P1 to P1' => P1 and strengthening P3 => P3' keeps it:

   P1' => P2 => P3'

--------------------------------------------------------
As for ARM.

Regarding dynamic checks all the above is irrelevant because dynamic 
checks are no contracts. Furthermore since the proper contracts include 
Constraint_Error or Storage_Error raised, do you really care how are you 
going to bomb your program while keeping proper contracts? (:-)) Sincere 
advise: forget about this mess.

For static checks a proof of implication is rather straightforward since 
we assume that all static predicates must be decidable anyway.

Of course, with generics you might run into troubles as you would have 
both proper contracts, i.e. the instantiated ones, and the generic ones 
expressed in generic terms. Instantiated contracts are easy to check, 
but what one would actually wish is checking generic contracts, which 
might turn impossible. The glimpse of the problem is what any Ada 
programmer knows: generic instantiations may fail to compile even if the 
actual parameters match...

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