On Sat, 7 Oct 2023 at 13:46, Martin Uecker via Liaison
<liaison_at_[hidden]> wrote:
>
> Am Samstag, dem 07.10.2023 um 12:24 +0300 schrieb Timur Doumler:
> You could make these additional arguments of the "macro":
>
> pre (x != 0, audit_level(3))
>
> or maybe:
>
> pre (<audit_level(3)>, x != 0)

Indeed..

pre(audit_level(3), x != 0)

and something like

> > void increment_size()
> > post [old_size = size()] (size() == old_size + 1);
>
> You could do
>
> post ( [old_size = size()] (size() == old_size + 1) );

post(capture(old_size = size()), size() == old_size + 1)

The capture one is interesting, and will be relevant for C, because it allows
writing a postcondition that uses the original value of a parameter even if your
function modifies the parameter. Such as if you get a pointer to a beginning and
return a pointer to something you were finding, you can just increment
the pointer
to the beginning, but you may want to check the original value in a
postcondition.

So.. at any rate, these suggestions are valuable, thanks for providing
them. I think
there is a way to fit them into the C++ syntax that we are designing,
because we do similar
things in other places. What the examples I wrote above illustrate are
just instances
of adding a prefix argument of a particular type to a pre/post "call"
. It's essentially
a tag argument. (And yes, we could equally well use postfix tags
instead of prefix tags.)

And the gist of what you're saying is that we should look into using
such tags or any other
techniques so that a a pre/post is always just "pre(whatever)" or
"post(whatever)", and
if we want to add bells and whistles, they should somehow go into the
"whatever", not
outside it, so no "[magic] pre(something)", no "pre<magic>(something)". Put that
"magic" inside "something" and the syntax as a whole remains macroable
and more C-friendly.