help / color / mirror / Atom feed
From: "Dmitry A. Kazakov" <>
Subject: Re: Contracts in generic formal subprogram
Date: Tue, 11 Apr 2023 14:03:27 +0200	[thread overview]
Message-ID: <u13iae$2kj2n$> (raw)
In-Reply-To: <u12squ$2j3h0$>

On 2023-04-11 07:56, G.B. wrote:
> On 08.04.23 10:02, Dmitry A. Kazakov wrote:
>> On 2023-04-08 09:00, mockturtle wrote:
>>> Should the actual subprogram specify the same contract? I am not sure 
>>> (and I guess this could be a stumbling block for the adoption of this 
>>> idea).
>> The general principle of substitutability is that the preconditions 
>> can be weakened, the postoconditions can be strengthened.
> Side track: "weak" and "strong" alone sounding like a valuation to the
> uninitiated, but neither technical nor precise; and the "objects" of
> comparison of sets of conditions being implicit; and the ARM not
> defining a technical term for these adjectives unless weak ordering
> helps.

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'

As for ARM.

Regarding dynamic checks all the above is irrelevant because dynamic 
checks are no contracts. Furthermore since the proper contracts include 
Constraint_Error or Storage_Error raised, do you really care how are you 
going to bomb your program while keeping proper contracts? (:-)) Sincere 
advise: forget about this mess.

For static checks a proof of implication is rather straightforward since 
we assume that all static predicates must be decidable anyway.

Of course, with generics you might run into troubles as you would have 
both proper contracts, i.e. the instantiated ones, and the generic ones 
expressed in generic terms. Instantiated contracts are easy to check, 
but what one would actually wish is checking generic contracts, which 
might turn impossible. The glimpse of the problem is what any Ada 
programmer knows: generic instantiations may fail to compile even if the 
actual parameters match...

Dmitry A. Kazakov

  reply	other threads:[~2023-04-11 12:03 UTC|newest]

Thread overview: 13+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-04-08  7:00 Contracts in generic formal subprogram mockturtle
2023-04-08  8:02 ` Dmitry A. Kazakov
2023-04-11  5:56   ` G.B.
2023-04-11 12:03     ` Dmitry A. Kazakov [this message]
2023-04-12  2:18       ` Spiros Bousbouras
2023-04-12  3:37         ` Spiros Bousbouras
2023-04-12  6:49           ` Niklas Holsti
2023-04-12  7:30           ` G.B.
2023-04-12 12:29           ` Ben Bacarisse
2023-04-13  6:27         ` Dmitry A. Kazakov
2023-04-08  9:09 ` Randy Brukardt
2023-04-08 16:48 ` Simon Wright
2023-04-08 17:27   ` mockturtle
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox