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
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:
References: <0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com>
<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:
On 2023-04-12 6:37, Spiros Bousbouras wrote:
> On Wed, 12 Apr 2023 02:18:45 -0000 (UTC)
> Spiros Bousbouras wrote:
>> On Tue, 11 Apr 2023 14:03:27 +0200
>> "Dmitry A. Kazakov" 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".