Initial proposal for functions with (in-)out parameters in SPARK

[yannickmoy]

Full proposal here

[clairedross]

AFAIU, IN parameters of functions will remain constant even if they are of an access-to-variable type right?

[yannickmoy]

@clairedross yes, that's the current proposal.

[clairedross]

Ok, best keep it simple. We should also disallow IN OUT and OUT parameters in traversal functions probably.

[yannickmoy]

agree with you @clairedross in forbidding procedural traversal functions. I amended the RFC.

[sttaft]

It is a bit misleading to say that you restrict calls on procedural functions to the RHS of an assignment statement, because you also seem to allow it as the initial expression of an object declaration, which is not called an "assignment statement" in Ada. A better description of the restriction might be that such calls can only appear as the RHS of an assignment operation as part of a declaration or an assignment statement.

[yannickmoy]

@sttaft No, the intent is not to allow it as the initial expression of an object declaration. That would require more changes in flow/proof to allow effects in parts where we don't expect them currently.