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 top-level code position.

• 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.

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 (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.