Replace bindings by declare blocks

[treiher]

Context and Problem Statement

In #701 the introduction of declare blocks is proposed. Declare blocks provide a similar functionality as the already existing bindings. It could be beneficial to replace bindings by declare blocks.

Example

Without binding or declare block

      state X is
         [...]
         Hash : Opaque;
         Query : P::Query
      begin
         [...]
         Hash := Hash = Get_Hash (Transcript_Hash).Data;
         Query = P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash);
         Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query));

With binding

      state X is
         [...]
      begin
         [...]
         Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query)
                           where Query = P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash)
                              where Hash = Get_Hash (Transcript_Hash).Data);

With declare block

      state X is
         [...]
      begin
         [...]
         declare
            Hash : Opaque = Get_Hash (Transcript_Hash).Data;
            Query : P::Query := P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash);
         begin
            Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query));
         end;

Considered Options

O1 Replace bindings by declare blocks

+ Keep DSL smaller by preventing two ways to do essentially the same thing + Declare blocks are probably easier readable than bindings as type of variable is stated explicitly + Less implementation and maintenance effort (validation and code generation easier to implement for declare blocks than bindings as no type inference is needed)

O2 Keep bindings as well as declare blocks

+ Bindings are easier to write (as bindings are less verbose than declare blocks)

Decision Outcome

O1

[sttaft]

Bindings are perhaps easier to write, but they could be harder to read. In the example above, the definition of "Hash" via the "where" clause was not readily visible to me on a first reading. These are analogous to "let" statements, but the "where" clause comes at the end rather than at the beginning as in a "let" clause. Furthermore, Ada/SPARK generally requires definition before use, and having the "where" clause at the end violates that. More commonly, as in SQL, a "where" clause (or "when" clause in Ada/SPARK) acts as a filter rather than as a definition.