Tactic: swap

The swap tactic applies to program-logic goals by rewriting the program into a semantically equivalent form where two consecutive, independent program fragments are exchanged.

In a nutshell, swap permutes commands when doing so does not change the program’s behavior (typically because the swapped fragments do not interfere, e.g., they write to disjoint variables and neither reads what the other writes).

Applying swap replaces the current goal by the same goal, but with the selected commands swapped in the program. This is useful to expose a more convenient program structure, for example to align programs in relational proofs or to bring related statements closer together.

Syntax

The swap tactic comes in several forms:

Syntax

• swap {side}? {codepos1}

• swap {side}? {codepos1} {codeoffset1}

• swap {side}? [{codepos1}..{codepos1}] {codeoffset1}`

Here:

• {side} is optional and is either 1 or 2. It selects the left or right program in relational goals. If omitted, the tactic applies to the single program under consideration.

• {codepos1} denotes a code position in the program.

• Any {codepos1} or block [{codepos1}..{codepos1}] may be prefixed with a code path, selecting a nested block in which the swap takes place. Each step of the path is a code position followed by a branch selector: . for the then-branch of a conditional or the body of a loop, ? for the else-branch of a conditional, and #C. for the arm of a match labelled by the constructor C. A single position directly follows the path, while a block is separated from it by :. For instance, 2#Some.1 designates the first command of the Some arm of the match at position 2, and 1.:[1..2] the block formed by the first two commands of the then-branch (or loop body) of the command at position 1.

• A {codeoffset1} is either:

  • a signed integer (n or -n), denoting a relative position, or

  • an absolute code position written @ {codepos1}.

The meaning of these forms is as follows:

• swap {side}? {codepos1}

  swaps the two adjacent commands starting at the top-level position {codepos1}.

• swap {side}? {codepos1} {codeoffset1}

  swaps the command at top-level position {codepos1} with the command at the position designated by {codeoffset1}.

• swap {side}? [{codepos1}..{codepos1}] {codeoffset1}

  swaps a whole sequence of commands delimited by [{codepos1}..{codepos1}] with the commands starting at the position designated by {codeoffset1}.

In all cases, the swap is only valid when the exchanged fragments are independent, so that the transformation preserves the program semantics.

When a code path is given, positions and offsets are interpreted relative to the selected block, the destination must lie inside that block, and the enclosing command (conditional, loop or match) and its other branches are left unchanged.

Example (single statement)

The following example swaps two adjacent assignments that do not interfere. The returned result is unchanged, but the rewritten program may be more convenient for subsequent proof steps.

Example (swapping a block)

The following example illustrates the block form swap [{codepos1}..{codepos1}] {codeoffset1}. We swap a block of two commands with a later, independent command.

Example (swapping inside a branch)

The following example uses a code path to swap two commands located in the then-branch of a conditional. The conditional itself and its else-branch are preserved.

Example (invalid swap)

The following example shows a swap attempt that fails because the two commands are not independent: the second command reads the value written by the first one.