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=-1.7 required=3.0 tests=BAYES_00,NICE_REPLY_A,
	REPLYTO_WITHOUT_TO_CC,T_SCC_BODY_TEXT_LINE autolearn=no
	autolearn_force=no version=3.4.6
Path: eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Contracts in generic formal subprogram
Date: Wed, 12 Apr 2023 09:30:55 +0200
Organization: A noiseless patient Spider
Message-ID: <u15mng$2uq94$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>
 <4I=3lX6HccsqYa6JC@bongo-ra.co>
Reply-To: nonlegitur@notmyhomepage.de
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 12 Apr 2023 07:30:56 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="0741b94302a501f99b01e7df1e85ead4";
	logging-data="3107108"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+1f3+DrtAqQqesDMp1soIoii6SGDhycDE="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:102.0)
 Gecko/20100101 Thunderbird/102.9.1
Cancel-Lock: sha1:GtUu/tvmr0xMy2HeiaEeN+/zCQY=
In-Reply-To: <4I=3lX6HccsqYa6JC@bongo-ra.co>
Content-Language: en-US
Xref: feeder.eternal-september.org comp.lang.ada:65091
List-Id: <comp.lang.ada>

On 12.04.23 05: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.

Thanks for pointing out the issue: When P_n or Q_m don't
mention the thing to which they "belong",
then how does just mentioning names of predicates clarify
to what end of the substitution the comparatives "weaker"
or "stronger" will apply? It's variance of meaning.

"The LSP paper" uses "weak" more generally.

OK, condition P is generally considered stronger than Q
if P implies Q, right? I.e., Q not without P.
Is there a commonly accepted definition of the words "weak"
and "strong", in mathematics perhaps, that justifies the
usual contextual _omissions_ from speech?

LSP uses "pre" and "post" for an object's value in a state.
There are phrases such as "stronger requirements that constrain".

Consider a different choice of adjectives:

   Given a primitive operation f of a type T,
   then a precondition of any overridden f of
   a type D descended from T must be sexier.

Does "sexy" carry more or less meaning than "weak" WRT assertions?