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).
GCC 12.2.0 accepts this code with -gnat2022.
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.
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'
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 .
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.
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.
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.
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 .
Sysop: | Keyop |
---|---|
Location: | Huddersfield, West Yorkshire, UK |
Users: | 251 |
Nodes: | 16 (2 / 14) |
Uptime: | 29:27:21 |
Calls: | 5,553 |
Files: | 11,677 |
Messages: | 5,115,091 |