Check consistency of function parameter names in API

[RustanLeino]

I first provide a quick reminder of the syntax of function signatures, then speak about the Boogie API and a problem, and finally suggest an enhancement.

Function syntax

Syntactically, Boogie allows two forms of function-declaration signatures. In one form, only the types of the parameters are given:

function F0(A, A, B): int;

In the other form, each parameter is decorated by a name. The name is meaningless to Boogie (unless the function has a body), but may help the Boogie user remember which parameter is which. For example:

function F1(x: A, y: A, z: B): int;

In this second form, Boogie also allows adjacent parameters of the same type to be separated by commas:

function F2(x, y: A, z: B): int;

In the examples above, the type signatures of F0, F1, and F2 are the same.

Boogie does not allow you to mix these two forms, because then ambiguities may arise. For example:

function F3(x, y: A, z): int; // ill-formed
function F4(x, y: A, B): int; // ill-formed

Here, it's not clear if z and B are supposed to be types, or if these are the names of the last parameter and the user forgot to give the type of that parameter. Indeed, a user could also make a mistake with an earlier parameter, forgetting to give it a name or a type:

function F5(C, y: A, z: B): int;

Just like Boogie accepts F2, Boogie accepts F5, interpreting C as the name of the first parameter (of type A), whereas it flags the z in F3 and the B in F4 as errors.

API

In the Boogie API, a Function accepts its parameters via a List<Variable>, where each Variable has a TypedIdent, which gives the name: Type of each function parameter. In the API, the lack of a name is indicated by passing in the name as TypedIdent.NoName.

The API does not validate its parameters, so it is happy to accept a list of parameters, some with names and some without. This is fine for Boogie, since the parameter names of a function don't matter (except if the function has a body, but I'll continue to ignore that case here).

So, what's the problem, since the parameter names are ignored, anyway? The problem is that if Boogie is asked to print out the program, it may end up outputting something that is malformed Boogie--that is, something that the Boogie parser will not accept. I can't blame the print routine. The problem lies in misuse of the Boogie API--the construction of a Function should follow the same "no parameter has a name or every parameter has a name" rule as is enforced by the parser.

Suggested enhancement

The Boogie-client Dafny sometimes accidentally uses the Boogie API to construct malformed function signatures. These have not been detected until, some day, when someone happens to print out the Boogie program to run it through Boogie directly. It would be nice to detect this problem earlier. I think the best place to do so is inside Boogie.

As a Boogie enhancement, I propose that the Function constructor in the Boogie API check the "no parameter has a name or every parameter has a name" condition and does something drastic (like a Contract.Assume(false)) if the condition is not met. This would help Boogie clients find their misuse of the Boogie API sooner. (Of course, such clients would crash until their misuse has been corrected. For example, I expect that Dafny will fail in that way. However, we would then quickly fix those problems in Dafny and then we'd be living a happier life where printed Boogie programs parse back in without errors.)