Date: Thu, 23 Oct 2025 19:31:59 +0300
On Thu, 23 Oct 2025 at 19:21, Tom Honermann via SG21
<sg21_at_[hidden]> wrote:
>
> On 10/22/25 10:26 AM, John Spicer via SG21 wrote:
>
> That still fails to do what i want, which is to have the library provide know that the semantic they choose will be the one used when the program is linked.
>
> The following question is, again, intended as a serious one.
>
> Why do you want to use contracts to provide that guarantee?
>
> From my perspective, an unconditional-always-enforce contract semantic changes a function that has a narrow contract into a function that has a wide contract (or at least a wider contract subject to contracts that are actually expressible in the language). Contracts aren't needed to do that; we can express wider contracts in code today. Is the desire based on wanting integration with a contract violation handler? Or a desire to express hardened preconditions in the function interface so that they are available for static analysis or caller-side optimization?
>
> Assuming those capture your motivation, how far would support for a syntax like the following go towards satisfying your desire?
>
> int* find(int *begin, int *end, int item)
> pre hardened (begin != nullptr) // Hardened preconditions;
> pre hardened (end != nullptr) // always evaluated with a
> pre hardened (begin <= end) // terminating contract semantic.
> pre (is_sorted(begin, end) // Not a hardened precondition.
> ;
That syntax does the essential job. An example and its rumination
follows. I'll edit it to use your suggested syntax instead of its
original presentation choice
of 'pre_always', hopefully I'll search & replace correctly. :)
Consider:
A)
class X {
public:
/* expects: x >= 0 */
void f(int x);
};
void X::f(int x) {
if (x < 0)
terminate();
/* the rest, whatever */
}
B)
class X {
public:
void f(int x) pre hardened(x >= 0);
};
void X::f(int x) {
/* whatever */
}
Are those the same?
Yes, in their final form, they are.
But in how to get there, they are not, not at all.
I write the class definition. A less-seasoned programmer writes the
definition of
the member function.
My comment on the member function declaration in the class definition
in (A) is just a wish. And I need to go look, later, and verify
that the wish was fulfilled, when the less-seasoned programmer is done with the
task of producing the member function definition.
In case of (B), I don't need to go look later. My job is done after I
write the class definition. And I *know* the job is done,
and that's not subject to any build flags anywhere. And it works the
same everywhere,
including regardless of whether the functions are inline or not.
The contract.. ..isn't wide. I can see your point about it being wider
than a narrow contract, in that it doesn't have UB outside
the contract. Its behavior in those cases is certainly
splendidly-well-defined.. ..but the.. ..philosophical width of it
isn't wide,
in the sense that it's still just incorrect to call that function
outside the contract, even though that doesn't run into actual UB,
and indeed has perfectly well-defined behavior.
<sg21_at_[hidden]> wrote:
>
> On 10/22/25 10:26 AM, John Spicer via SG21 wrote:
>
> That still fails to do what i want, which is to have the library provide know that the semantic they choose will be the one used when the program is linked.
>
> The following question is, again, intended as a serious one.
>
> Why do you want to use contracts to provide that guarantee?
>
> From my perspective, an unconditional-always-enforce contract semantic changes a function that has a narrow contract into a function that has a wide contract (or at least a wider contract subject to contracts that are actually expressible in the language). Contracts aren't needed to do that; we can express wider contracts in code today. Is the desire based on wanting integration with a contract violation handler? Or a desire to express hardened preconditions in the function interface so that they are available for static analysis or caller-side optimization?
>
> Assuming those capture your motivation, how far would support for a syntax like the following go towards satisfying your desire?
>
> int* find(int *begin, int *end, int item)
> pre hardened (begin != nullptr) // Hardened preconditions;
> pre hardened (end != nullptr) // always evaluated with a
> pre hardened (begin <= end) // terminating contract semantic.
> pre (is_sorted(begin, end) // Not a hardened precondition.
> ;
That syntax does the essential job. An example and its rumination
follows. I'll edit it to use your suggested syntax instead of its
original presentation choice
of 'pre_always', hopefully I'll search & replace correctly. :)
Consider:
A)
class X {
public:
/* expects: x >= 0 */
void f(int x);
};
void X::f(int x) {
if (x < 0)
terminate();
/* the rest, whatever */
}
B)
class X {
public:
void f(int x) pre hardened(x >= 0);
};
void X::f(int x) {
/* whatever */
}
Are those the same?
Yes, in their final form, they are.
But in how to get there, they are not, not at all.
I write the class definition. A less-seasoned programmer writes the
definition of
the member function.
My comment on the member function declaration in the class definition
in (A) is just a wish. And I need to go look, later, and verify
that the wish was fulfilled, when the less-seasoned programmer is done with the
task of producing the member function definition.
In case of (B), I don't need to go look later. My job is done after I
write the class definition. And I *know* the job is done,
and that's not subject to any build flags anywhere. And it works the
same everywhere,
including regardless of whether the functions are inline or not.
The contract.. ..isn't wide. I can see your point about it being wider
than a narrow contract, in that it doesn't have UB outside
the contract. Its behavior in those cases is certainly
splendidly-well-defined.. ..but the.. ..philosophical width of it
isn't wide,
in the sense that it's still just incorrect to call that function
outside the contract, even though that doesn't run into actual UB,
and indeed has perfectly well-defined behavior.
Received on 2025-10-23 16:32:13
