[CN] Streamline spec syntax

[dc-mak]

Current syntax for spec requires user to retype function name and argument types. It's flexible, but tedious. Here's a proposal for not doing that.

Restriction on C syntax: should error (require specs to name arguments).

int inc(int);
/*@ spec; .. @*/

Restriction on C syntax: should error (zero or more than one declaration previously):

int b, int inc(int i);
/*@ spec; requires i < MAXi32(); ensures return == i + 1i32; @*/

Should error (not a function):

int inc;
/*@ spec; requires i < MAXi32(); ensures return == i + 1i32; @*/

Should work without repeating function name:

int inc(int i);
/*@ spec; requires i < MAXi32(); ensures return == i + 1i32; @*/

[septract]

I think this would be unambiguously a good change!

I wonder about requiring that spec is the first keyword (which is currently enforced by the parser). This is a bit irregular in CN - mostly it doesn't matter what order we put keywords. And the syntax doesn't suggest that there's anything special about the positioning of spec.

Note related grumbling here: #467

[cp526]

One things that's nice about this is that if the spec doesn't repeat function name and argument list there is no consistency to be checked between that and the function prototype.

Though, why not then drop the spec keyword here and just have the user give a requires/ensures/... list?

[thatplguy]

I love this idea. Following up on what @cp526 said, can we simply make function specifications on definitions and declarations the same?

If we decide to batch up breaking changes, moving specs to precede the function name would help unify these two cases, e.g.

/** Normal doc comments. */
/*@
  accesses glob;
  requires true;
  ensures true;
@*/
void my_function_decl();

/** Normal doc comments. */
/*@
  accesses glob;
  requires true;
  ensures true;
@*/
void my_function_def() {
    return;
}

FWIW this is how Frama-C places annotations.

[cp526]

We used to have function specifications precede their definition but moved away from it because it leads to less readable specifications: when specifications precede the definition, the syntax doesn’t reflect the binding structure, since the function arguments are in scope of the specification but are introduced only below it.

[thatplguy]

I see what you mean, but in some sense, CN annotations are simply structured comments. There's a long history of doc generation based on structured comments that have forward references to the function they're documenting (doxygen, javadoc, etc.).

Putting the spec after function decls is also a little weird w.r.t. scoping:

void my_decl();
// This is not in scope of this declaration.

void my_decl()
// This is... kind of?
;

// This is also not in scope, but it's common for comments to precede the thing they're commenting on.
void my_decl();

[septract]

FWIW Frama-C orders specs before definitions: https://www.frama-c.com/html/acsl.htmlOn Aug 30, 2024, at 10:31 AM, Cole Schlesinger ***@***.***> wrote: I see what you mean, but in some sense, CN annotations are simply structured comments. There's a long history of doc generation based on structured comments that have forward references to the function they're documenting (doxygen, javadoc, etc.). Putting the spec after function decls is also a little weird w.r.t. scoping: void my_decl(); // This is not in scope of this declaration. void my_decl() // This is... kind of? ; // This is also not in scope, but it's common for comments to precede the thing they're commenting on. void my_decl(); —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you commented.Message ID: ***@***.***>

[cp526]

As far as I can see, unifying the syntax for CN specifications for function definitions and function prototypes is independent of where the specification is placed, no?

[thatplguy]

As far as I can see, unifying the syntax for CN specifications for function definitions and function prototypes is independent of where the specification is placed, no?

Yes, we can unify the syntax without unifying the placement, so no need to make a decision on placement to move forward with the other bit.