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!news.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: Thu, 13 Apr 2023 08:27:30 +0200
Organization: A noiseless patient Spider
Message-ID: <u187ci$9mpm$1@dont-email.me>
References: <0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com>
 <u0r72o$16jtj$1@dont-email.me> <u12squ$2j3h0$1@dont-email.me>
 <u13iae$2kj2n$1@dont-email.me> <wTNwzuVC4pvpqJ=Iw@bongo-ra.co>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 13 Apr 2023 06:27:30 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="4960f866889f146161272c329b054297";
	logging-data="318262"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+m/UkfvTBqFG9QkCN/GC29IX8XP3BpH4E="
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.10.0
Cancel-Lock: sha1:wAfNzUMZtZaJHc3RZ+0qQGmPPn0=
Content-Language: en-US
In-Reply-To: <wTNwzuVC4pvpqJ=Iw@bongo-ra.co>
Xref: news.eternal-september.org comp.lang.ada:65093
List-Id: <comp.lang.ada>

On 2023-04-12 04:18, Spiros Bousbouras wrote:
> On Tue, 11 Apr 2023 14:03:27 +0200
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>> 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'
> 
> You have it backwards ; if  P1'  implies  P1  then  P1'  is stronger
> than  P1 .

Yes, you are right. Inclusion is an inverse of implication.

A weaker predicate is true on a set that contains the set where the 
stronger predicate is.

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