Re: Contracts in generic formal subprogram

["G.B." <bauhaus@notmyhomepage.invalid>]

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?