15.5  Control Restrictions

A number of restrictions on the syntax of control statements are motivated by a desire to minimize the difficulty of translating from an imperative to a functional programming paradigm. Thus, the only control statements supported are those listed in Sectionmascover. In particular, while and do...while are not included. Moreover, a number of restrictions are imposed on the remaining constructs.

The ACL2 translator converts a for loop into an auxiliary recursive function. In order for this function to be admitted into the ACL2 logic, the prover must be able to establish that execution of this function terminates. In order to guarantee that this proof succeeds, we require a for loop to have the form

  for ( init; test; update) { ... }
under the following restrictions:

Neither break nor continue may occur in a for loop. In some cases, the loop test may be used to achieve the functionality of break. For example, instead of

  for (uint i=0; i<N; i++) {
    if ( expr) break;
we may write

  for (uint i=0; i<N && ! expr; i++) {

The ACL2 translator converts a switch statement to the LISP case macro. We require that each case of a switch has one of two forms:

case label: $ \mathit{stmt}_1$ ... $ \mathit{stmt}_k$

default: $ \mathit{stmt}_1$ ... $ \mathit{stmt}_k$

(1) if $ k>1$, then break does not occur in any $ \mathit{stmt}_i$ for $ i < k$, and

(2) if $ k>0$, then except for the final case of the statement, $ \mathit{stmt}_k$ is break.

Further restrictions are imposed on the placement of return statements. We require every function body to satisfy the following definition: A statement block is well-formed with respect to return statements if (1) it consists of a non-empty sequence of statements, (2) none of these statements except the final one contains a return statement, and (3) the final statement of the block is either a return statement or an if...else statement of which both branches are well-formed with respect to return statements.

David Russinoff 2017-08-01