Reference manual / Z-related commands / Refinement commands / iteration

This command is part of the experimental refinement editor.

The iteration command refines a specification statement to a loop whose body is a non-deterministic alternation. It applies the following inference rule of the refinement calculus.

\vdash? I \land \lnot (G1 \lor ... \lor Gn) \implies Q
\vdash? I \land \lnot v \in \nat \implies \lnot (G1 \lor ... \lor Gn)
\vdash? \forall V : \nat @ \specstmt F[G1 \land V = v, I, v < V]
\vdash? \forall V : \nat @ \specstmt F[Gn \land V = v, I, v < V]

\vdash? \specstmt F[P,I,Q]

where V is a reference to a variable whose value is that of the variant expression and G1 ... Gn are guard predicates.

The code that is implicitly generated by this refinement rule is the following non-deterministic iteration of guarded specification statements.

do G1 \fun \specstmt F[G1 \land P, I, Q]
[] ...
[] Gn \fun \specstmt F[Gn \land P, I, Q]

The iteration command is applicable when any specification statement \specstmt F[P,I,Q] in a goal is inspected.

The variant V is entered into a dialogue box using the syntax of a Z expression, and it must be of type \arithmos. The default response is the previous response. Alternatively, if a suitable expression is displayed in the same window, it can have been selected first (crossed). Then, each guard in the sequence G1 ... Gn is entered into one of a sequence of dialogue boxes using the syntax of a Z predicate. The sequence is ended by giving an empty response. The default response is nothing. Alternatively, if some suitable predicates are displayed in the same window, they can have been selected first (crossed). Additional guards can then be entered in dialogue boxes. The variant and guards are typechecked in the environment of the inspected specification statement. An error in any dialogue box aborts the entire iteration command.

There must be at least one guard.

Tactic example

"iteration" "G1" ... "Gn" "v" p

This example applies the iteration command to specification statement p using variant expression v and the guards G1 ... Gn.

A tactic that applies the iteration command must be executed by play tactic; it is not applicable under apply tactic as the resulting code would not be accessible to the code command.

IT 20-Nov-2000