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!feeder.eternal-september.org!news.szaf.org!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Contracts in generic formal subprogram
Date: Wed, 12 Apr 2023 09:49:35 +0300
Organization: Tidorum Ltd
Message-ID: <k9n2jvFark6U1@mid.individual.net>
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>
 <4I=3lX6HccsqYa6JC@bongo-ra.co>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net wpzrt4emyV12Pp/74xsDsQpYi7jPUnOImoSnjUOJ/P890pdb/i
Cancel-Lock: sha1:NTHEiCYdbNZxJAQBIpqlcuBvf8k=
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:102.0)
 Gecko/20100101 Thunderbird/102.6.1
Content-Language: en-US
In-Reply-To: <4I=3lX6HccsqYa6JC@bongo-ra.co>
Xref: feeder.eternal-september.org comp.lang.ada:65090
List-Id: <comp.lang.ada>

On 2023-04-12 6:37, Spiros Bousbouras wrote:
> On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
> Spiros Bousbouras <spibou@gmail.com> 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 .
> 
> Apologies ; it was me who got it backwards.


Speaking of logic in general, rather than Ada contracts in particular, I 
would say that you got it right, and Dmitry did not.

Suppose we have a theorem about geometrical figures F, and at first we 
can prove the theorem only if we assume (precondition) that the figure F 
is a square. Later we manage to improve the proof so that it holds also 
for rectangles. I would say, and I think mathematicians would say, that 
we /weakened/ the assumptions from "F is a square" to "F is a 
rectangle", and indeed the former (stronger) implies the latter 
(weaker), which is not as Dmitry defined "stronger".