# Hoare2Hoare Logic, Part II

On a piece of paper, write down a specification (as
a Hoare triple) for the following program:

X ::= 2;;

Y ::= X + X

X ::= 2;;

Y ::= X + X

Write down a (useful) specification for the following program:

X ::= X + 1;; Y ::= X + 1

X ::= X + 1;; Y ::= X + 1

Write down a (useful) specification for the following program:

TEST X ≤ Y

THEN SKIP

ELSE

Z ::= X;;

X ::= Y;;

Y ::= Z

FI

TEST X ≤ Y

THEN SKIP

ELSE

Z ::= X;;

X ::= Y;;

Y ::= Z

FI

Write down a (useful) specification for the following program:

X ::= m;;

Z ::= 0;;

WHILE ~(X = 0) DO

X ::= X - 2;;

Z ::= Z + 1

END

X ::= m;;

Z ::= 0;;

WHILE ~(X = 0) DO

X ::= X - 2;;

Z ::= Z + 1

END

# Decorated Programs

*compositional*: the structure of proofs exactly follows the structure of programs.

*decorated program*carries within it an argument for its own correctness.

### For example, consider the program:

WHILE ~(X = 0) DO

Z ::= Z - 1;;

X ::= X - 1

END

### Here is one possible specification for this program:

{{ X = m ∧ Z = p }}

WHILE ~(X = 0) DO

Z ::= Z - 1;;

X ::= X - 1

END

{{ Z = p - m }}

*parameters*m and p, which stand for fixed-but-arbitrary numbers. Formally, they are simply Coq variables of type nat.

### Here is a decorated version of the program, embodying a proof of this specification:

{{ X = m ∧ Z = p }} ->>

{{ Z - X = p - m }}

WHILE ~(X = 0) DO

{{ Z - X = p - m ∧ X ≠ 0 }} ->>

{{ (Z - 1) - (X - 1) = p - m }}

Z ::= Z - 1;;

{{ Z - (X - 1) = p - m }}

X ::= X - 1

{{ Z - X = p - m }}

END

{{ Z - X = p - m ∧ ¬(X ≠ 0) }} ->>

{{ Z = p - m }}

### To check that a decorated program represents a valid proof, we check that each individual command is

*locally consistent*with its nearby assertions in the following sense:

- SKIP is locally consistent if its precondition and
postcondition are the same:

{{ P }} SKIP {{ P }}

- The sequential composition of c
_{1}and c_{2}is locally consistent (with respect to assertions P and R) if c_{1}is locally consistent (with respect to P and Q) and c_{2}is locally consistent (with respect to Q and R):

{{ P }} c_{1};; {{ Q }} c_{2}{{ R }}

- An assignment is locally consistent if its precondition is the
appropriate substitution of its postcondition:

{{ P [X ⊢> a] }}

X ::= a

{{ P }}

- A conditional is locally consistent (with respect to assertions
P and Q) if the assertions at the top of its "then" and
"else" branches are exactly P ∧ b and P ∧ ¬b and if its
"then" branch is locally consistent (with respect to P ∧ b
and Q) and its "else" branch is locally consistent (with
respect to P ∧ ¬b and Q):

{{ P }}

TEST b THEN

{{ P ∧ b }}

c_{1}

{{ Q }}

ELSE

{{ P ∧ ¬b }}

c_{2}

{{ Q }}

FI

{{ Q }}

- A while loop with precondition P is locally consistent if its
postcondition is P ∧ ¬b, if the pre- and postconditions of
its body are exactly P ∧ b and P, and if its body is
locally consistent:

{{ P }}

WHILE b DO

{{ P ∧ b }}

c_{1}

{{ P }}

END

{{ P ∧ ¬b }}

- A pair of assertions separated by ->> is locally consistent if
the first implies the second:

{{ P }} ->>

{{ P' }}*only*place in a decorated program where checking whether decorations are correct is not fully mechanical and syntactic, but rather may involve logical and/or arithmetic reasoning.

## Example: Swapping Using Addition and Subtraction

X ::= X + Y;;

Y ::= X - Y;;

X ::= X - Y

(* WORK IN CLASS *)

## Example: Simple Conditionals

{{ True }}

TEST X ≤ Y THEN

Z ::= Y - X

ELSE

Z ::= X - Y

FI

{{ Z + X = Y ∨ Z + Y = X }}

(* WORK IN CLASS *)

## Example: Reduce to Zero

{{ True }}

WHILE ~(X = 0) DO

X ::= X - 1

END

{{ X = 0 }}

(* WORK IN CLASS *)

### From an informal proof in the form of a decorated program, it is easy to read off a formal proof using the Coq versions of the Hoare rules. Note that we do

*not*unfold the definition of hoare_triple anywhere in this proof -- the idea is to use the Hoare rules as a self-contained logic for reasoning about programs.

Definition reduce_to_zero' : com :=

WHILE ~(X = 0) DO

X ::= X - 1

END.

Theorem reduce_to_zero_correct' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

(* First we need to transform the postcondition so

that hoare_while will apply. *)

eapply hoare_consequence_post.

- apply hoare_while.

+ (* Loop body preserves invariant *)

(* Need to massage precondition before hoare_asgn applies *)

eapply hoare_consequence_pre.

× apply hoare_asgn.

× (* Proving trivial implication (2) ->> (3) *)

unfold assn_sub, "->>". simpl. intros. exact I.

- (* Invariant and negated guard imply postcondition *)

intros st [Inv GuardFalse].

unfold bassn in GuardFalse. simpl in GuardFalse.

rewrite not_true_iff_false in GuardFalse.

rewrite negb_false_iff in GuardFalse.

apply eqb_eq in GuardFalse.

apply GuardFalse.

Qed.

### In Hoare we introduced a series of tactics named assn_auto to automate proofs involving just assertions. We can try using the most advanced of those tactics to streamline the previous proof:

Theorem reduce_to_zero_correct'' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

eapply hoare_consequence_post.

- apply hoare_while.

+ eapply hoare_consequence_pre.

× apply hoare_asgn.

× assn_auto''.

- assn_auto''. (* doesn't succeed *)

Abort.

Ltac verify_assn :=

repeat split;

simpl; unfold assert_implies;

unfold ap in *; unfold ap

_{2}in *;

unfold bassn in *; unfold beval in *; unfold aeval in *;

unfold assn_sub; intros;

repeat (simpl in *;

rewrite t_update_eq ||

(try rewrite t_update_neq; [| (intro X; inversion X; fail)]));

simpl in *;

repeat match goal with [H : _ ∧ _ ⊢ _] ⇒ destruct H end;

repeat rewrite not_true_iff_false in *;

repeat rewrite not_false_iff_true in *;

repeat rewrite negb_true_iff in *;

repeat rewrite negb_false_iff in *;

repeat rewrite eqb_eq in *;

repeat rewrite eqb_neq in *;

repeat rewrite leb_iff in *;

repeat rewrite leb_iff_conv in *;

try subst;

simpl in *;

repeat

match goal with

[st : state ⊢ _] ⇒

match goal with

| [H : st _ = _ ⊢ _] ⇒ rewrite → H in *; clear H

| [H : _ = st _ ⊢ _] ⇒ rewrite <- H in *; clear H

end

end;

try eauto; try omega.

Theorem reduce_to_zero_correct''' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

eapply hoare_consequence_post.

- apply hoare_while.

+ eapply hoare_consequence_pre.

× apply hoare_asgn.

× verify_assn.

- verify_assn.

Qed.

unfold reduce_to_zero'.

eapply hoare_consequence_post.

- apply hoare_while.

+ eapply hoare_consequence_pre.

× apply hoare_asgn.

× verify_assn.

- verify_assn.

Qed.

## Example: Division

X ::= m;;

Y ::= 0;;

WHILE n ≤ X DO

X ::= X - n;;

Y ::= Y + 1

END;

### Here's a possible specification:

{{ True }}

X ::= m;;

Y ::= 0;;

WHILE n ≤ X DO

X ::= X - n;;

Y ::= Y + 1

END

{{ n × Y + X = m ∧ X < n }}

(* WORK IN CLASS *)

# Finding Loop Invariants

## Example: Slow Subtraction

{{ X = m ∧ Y = n }}

WHILE ~(X = 0) DO

Y ::= Y - 1;;

X ::= X - 1

END

{{ Y = n - m }}

### To verify this program, we need to find an invariant Inv for the loop. As a first step we can leave Inv as an unknown and build a

*skeleton*for the proof by applying the rules for local consistency (working from the end of the program to the beginning, as usual, and without any thinking at all yet).

(1) {{ X = m ∧ Y = n }} ->> (a)

(2) {{ Inv }}

WHILE ~(X = 0) DO

(3) {{ Inv ∧ X ≠ 0 }} ->> (c)

(4) {{ Inv [X ⊢> X-1] [Y ⊢> Y-1] }}

Y ::= Y - 1;;

(5) {{ Inv [X ⊢> X-1] }}

X ::= X - 1

(6) {{ Inv }}

END

(7) {{ Inv ∧ ¬(X ≠ 0) }} ->> (b)

(8) {{ Y = n - m }}

- (a) it must be
*weak*enough to be implied by the loop's precondition, i.e., (1) must imply (2); - (b) it must be
*strong*enough to imply the program's postcondition, i.e., (7) must imply (8); - (c) it must be
*preserved*by each iteration of the loop (given that the loop guard evaluates to true), i.e., (3) must imply (4).

(* WORK IN CLASS *)

## Example: Parity

{{ X = m }}

WHILE 2 ≤ X DO

X ::= X - 2

END

{{ X = parity m }}

Fixpoint parity x :=

match x with

| 0 ⇒ 0

| 1 ⇒ 1

| S (S x') ⇒ parity x'

end.

(* WORK IN CLASS *)

## Example: Finding Square Roots

{{ X=m }}

Z ::= 0;;

WHILE (Z+1)*(Z+1) ≤ X DO

Z ::= Z+1

END

{{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

(* WORK IN CLASS *)

## Example: Squaring

{{ X = m }}

Y ::= 0;;

Z ::= 0;;

WHILE ~(Y = X) DO

Z ::= Z + X;;

Y ::= Y + 1

END

{{ Z = m×m }}

(* WORK IN CLASS *)

# Formal Decorated Programs (Advanced)

## Syntax

*Decorated commands*contain assertions mostly just as postconditions, omitting preconditions where possible and letting the context supply them.

{{P}} ({{P}} SKIP {{P}}) ;; ({{P}} SKIP {{P}}) {{P}},

- Command SKIP is decorated only with its postcondition, as
SKIP {{ Q }}.
- Sequence d
_{1};; d_{2}contains no additional decoration. Inside d_{2}there will be a postcondition; that serves as the postcondition of d_{1};; d_{2}. Inside d_{1}there will also be a postcondition; it additionally serves as the precondition for d_{2}. - Assignment X ::= a is decorated only with its postcondition,
as X ::= a {{ Q }}.
- If statement TEST b THEN d
_{1}ELSE d_{2}is decorated with a postcondition for the entire statement, as well as preconditions for each branch, as TEST b THEN {{ P_{1}}} d_{1}ELSE {{ P_{2}}} d_{2}FI {{ Q }}. - While loop WHILE b DO d END is decorated with its
postcondition and a precondition for the body, as
WHILE b DO {{ P }} d END {{ Q }}. The postcondition inside
d serves as the loop invariant.
- Implications ->> are added as decorations for a precondition as ->> {{ P }} d, or for a postcondition as d ->> {{ Q }}. The former is waiting for another precondition to eventually be supplied, e.g., {{ P'}} ->> {{ P }} d, and the latter relies on the postcondition already embedded in d.

Inductive dcom : Type :=

| DCSkip (Q : Assertion)

(* SKIP {{ Q }} *)

| DCSeq (d

_{1}d

_{2}: dcom)

(* d

_{1};; d

_{2}*)

| DCAsgn (X : string) (a : aexp) (Q : Assertion)

(* X := a {{ Q }} *)

| DCIf (b : bexp) (P

_{1}: Assertion) (d

_{1}: dcom)

(P

_{2}: Assertion) (d

_{2}: dcom) (Q : Assertion)

(* TEST b THEN {{ P

_{1}}} d

_{1}ELSE {{ P

_{2}}} d

_{2}FI {{ Q }} *)

| DCWhile (b : bexp) (P : Assertion) (d : dcom) (Q : Assertion)

(* WHILE b DO {{ P }} d END {{ Q }} *)

| DCPre (P : Assertion) (d : dcom)

(* ->> {{ P }} d *)

| DCPost (d : dcom) (Q : Assertion)

(* d ->> {{ Q }} *)

.

DCPre is used to provide the weakened precondition from
the rule of consequence. To provide the initial precondition
at the very top of the program, we use Decorated:

Inductive decorated : Type :=

| Decorated : Assertion → dcom → decorated.

Notation "'SKIP' {{ P }}"

:= (DCSkip P)

(at level 10) : dcom_scope.

Notation "l '::=' a {{ P }}"

:= (DCAsgn l a P)

(at level 60, a at next level) : dcom_scope.

Notation "'WHILE' b 'DO' {{ Pbody }} d 'END' {{ Ppost }}"

:= (DCWhile b Pbody d Ppost)

(at level 80, right associativity) : dcom_scope.

Notation "'TEST' b 'THEN' {{ P }} d 'ELSE' {{ P' }} d' 'FI' {{ Q }}"

:= (DCIf b P d P' d' Q)

(at level 80, right associativity) : dcom_scope.

Notation "'->>' {{ P }} d"

:= (DCPre P d)

(at level 90, right associativity) : dcom_scope.

Notation "d '->>' {{ P }}"

:= (DCPost d P)

(at level 80, right associativity) : dcom_scope.

Notation " d ;; d' "

:= (DCSeq d d')

(at level 80, right associativity) : dcom_scope.

Notation "{{ P }} d"

:= (Decorated P d)

(at level 90) : dcom_scope.

Delimit Scope dcom_scope with dcom.

Open Scope dcom_scope.

Example dec0 :=

SKIP {{ True }}.

Example dec1 :=

WHILE true DO {{ True }} SKIP {{ True }} END

{{ True }}.

:= (DCSkip P)

(at level 10) : dcom_scope.

Notation "l '::=' a {{ P }}"

:= (DCAsgn l a P)

(at level 60, a at next level) : dcom_scope.

Notation "'WHILE' b 'DO' {{ Pbody }} d 'END' {{ Ppost }}"

:= (DCWhile b Pbody d Ppost)

(at level 80, right associativity) : dcom_scope.

Notation "'TEST' b 'THEN' {{ P }} d 'ELSE' {{ P' }} d' 'FI' {{ Q }}"

:= (DCIf b P d P' d' Q)

(at level 80, right associativity) : dcom_scope.

Notation "'->>' {{ P }} d"

:= (DCPre P d)

(at level 90, right associativity) : dcom_scope.

Notation "d '->>' {{ P }}"

:= (DCPost d P)

(at level 80, right associativity) : dcom_scope.

Notation " d ;; d' "

:= (DCSeq d d')

(at level 80, right associativity) : dcom_scope.

Notation "{{ P }} d"

:= (Decorated P d)

(at level 90) : dcom_scope.

Delimit Scope dcom_scope with dcom.

Open Scope dcom_scope.

Example dec0 :=

SKIP {{ True }}.

Example dec1 :=

WHILE true DO {{ True }} SKIP {{ True }} END

{{ True }}.

An example decorated program that decrements X to 0:

Example dec_while : decorated :=

{{ True }}

WHILE ~(X = 0)

DO

{{ True ∧ (X ≠ 0) }}

X ::= X - 1

{{ True }}

END

{{ True ∧ X = 0}} ->>

{{ X = 0 }}.

Fixpoint extract (d : dcom) : com :=

match d with

| DCSkip _ ⇒ SKIP

| DCSeq d

_{1}d

_{2}⇒ (extract d

_{1};; extract d

_{2})

| DCAsgn X a _ ⇒ X ::= a

| DCIf b _ d

_{1}_ d

_{2}_ ⇒ TEST b THEN extract d

_{1}ELSE extract d

_{2}FI

| DCWhile b _ d _ ⇒ WHILE b DO extract d END

| DCPre _ d ⇒ extract d

| DCPost d _ ⇒ extract d

end.

Definition extract_dec (dec : decorated) : com :=

match dec with

| Decorated P d ⇒ extract d

end.

Example extract_while_ex :

extract_dec dec_while = (WHILE ¬X = 0 DO X ::= X - 1 END)%imp.

Proof.

unfold dec_while.

reflexivity.

Qed.

Fixpoint post (d : dcom) : Assertion :=

match d with

| DCSkip P ⇒ P

| DCSeq d

_{1}d

_{2}⇒ post d

_{2}

| DCAsgn X a Q ⇒ Q

| DCIf _ _ d

_{1}_ d

_{2}Q ⇒ Q

| DCWhile b Pbody c Ppost ⇒ Ppost

| DCPre _ d ⇒ post d

| DCPost c Q ⇒ Q

end.

Definition pre_dec (dec : decorated) : Assertion :=

match dec with

| Decorated P d ⇒ P

end.

Definition post_dec (dec : decorated) : Assertion :=

match dec with

| Decorated P d ⇒ post d

end.

Example pre_dec_while : pre_dec dec_while = True.

Proof. reflexivity. Qed.

Example post_dec_while : post_dec dec_while = (X = 0)%assertion.

Proof. reflexivity. Qed.

Definition dec_correct (dec : decorated) :=

{{pre_dec dec}} (extract_dec dec) {{post_dec dec}}.

Example dec_while_triple_correct :

dec_correct dec_while

= {{ True }}

(WHILE ~(X = 0) DO X ::= X - 1 END)%imp

{{ X = 0 }}.

Proof. reflexivity. Qed.

To check whether this Hoare triple is
The function verification_conditions takes a dcom d together
with a precondition P and returns a

*valid*, we need a way to extract the "proof obligations" from a decorated program. These obligations are often called*verification conditions*, because they are the facts that must be verified to see that the decorations are logically consistent and thus constitute a proof of correctness.## Extracting Verification Conditions

*proposition*that, if it can be proved, implies that the triple {{P}} (extract d) {{post d}} is valid. It does this by walking over d and generating a big conjunction that includes- all the local consistency checks
- many uses of ->> to bridge the gap between (i) assertions found inside decorated commands and (ii) assertions used by the local consistency checks. These uses correspond applications of the consequence rule.

Fixpoint verification_conditions (P : Assertion) (d : dcom) : Prop :=

match d with

| DCSkip Q ⇒

(P ->> Q)

| DCSeq d

_{1}d

_{2}⇒

verification_conditions P d

_{1}

∧ verification_conditions (post d

_{1}) d

_{2}

| DCAsgn X a Q ⇒

(P ->> Q [X ⊢> a])

| DCIf b P

_{1}d

_{1}P

_{2}d

_{2}Q ⇒

((P ∧ b) ->> P

_{1})%assertion

∧ ((P ∧ ¬b) ->> P

_{2})%assertion

∧ (post d

_{1}->> Q) ∧ (post d

_{2}->> Q)

∧ verification_conditions P

_{1}d

_{1}

∧ verification_conditions P

_{2}d

_{2}

| DCWhile b Pbody d Ppost ⇒

(* post d is the loop invariant and the initial

precondition *)

(P ->> post d)

∧ ((post d ∧ b) ->> Pbody)%assertion

∧ ((post d ∧ ¬b) ->> Ppost)%assertion

∧ verification_conditions Pbody d

| DCPre P' d ⇒

(P ->> P') ∧ verification_conditions P' d

| DCPost d Q ⇒

verification_conditions P d ∧ (post d ->> Q)

end.

Theorem verification_correct : ∀ d P,

verification_conditions P d → {{P}} (extract d) {{post d}}.

Proof.

induction d; intros; simpl in ×.

- (* Skip *)

eapply hoare_consequence_pre.

+ apply hoare_skip.

+ assumption.

- (* Seq *)

destruct H as [H

eapply hoare_seq.

+ apply IHd2. apply H

+ apply IHd1. apply H

- (* Asgn *)

eapply hoare_consequence_pre.

+ apply hoare_asgn.

+ assumption.

- (* If *)

destruct H as [HPre1 [HPre2 [Hd

apply IHd1 in HThen. clear IHd1.

apply IHd2 in HElse. clear IHd2.

apply hoare_if.

+ eapply hoare_consequence; eauto.

+ eapply hoare_consequence; eauto.

- (* While *)

destruct H as [Hpre [Hbody1 [Hpost1 Hd]]].

eapply hoare_consequence; eauto.

apply hoare_while.

eapply hoare_consequence_pre; eauto.

- (* Pre *)

destruct H as [HP Hd].

eapply hoare_consequence_pre; eauto.

- (* Post *)

destruct H as [Hd HQ].

eapply hoare_consequence_post; eauto.

Qed.

induction d; intros; simpl in ×.

- (* Skip *)

eapply hoare_consequence_pre.

+ apply hoare_skip.

+ assumption.

- (* Seq *)

destruct H as [H

_{1}H_{2}].eapply hoare_seq.

+ apply IHd2. apply H

_{2}.+ apply IHd1. apply H

_{1}.- (* Asgn *)

eapply hoare_consequence_pre.

+ apply hoare_asgn.

+ assumption.

- (* If *)

destruct H as [HPre1 [HPre2 [Hd

_{1}[Hd_{2}[HThen HElse]]]]].apply IHd1 in HThen. clear IHd1.

apply IHd2 in HElse. clear IHd2.

apply hoare_if.

+ eapply hoare_consequence; eauto.

+ eapply hoare_consequence; eauto.

- (* While *)

destruct H as [Hpre [Hbody1 [Hpost1 Hd]]].

eapply hoare_consequence; eauto.

apply hoare_while.

eapply hoare_consequence_pre; eauto.

- (* Pre *)

destruct H as [HP Hd].

eapply hoare_consequence_pre; eauto.

- (* Post *)

destruct H as [Hd HQ].

eapply hoare_consequence_post; eauto.

Qed.

Now that all the pieces are in place, we can verify an entire program.

Definition verification_conditions_dec (dec : decorated) : Prop :=

match dec with

| Decorated P d ⇒ verification_conditions P d

end.

Corollary verification_correct_dec : ∀ dec,

verification_conditions_dec dec → dec_correct dec.

Proof.

intros [P d]. apply verification_correct.

Qed.

### The propositions generated by verification_conditions are fairly big, and they contain many conjuncts that are essentially trivial. Our verify_assn can often take care of them.

Example vc_dec_while :

verification_conditions_dec dec_while =

((((fun _ : state ⇒ True) ->> (fun _ : state ⇒ True)) ∧

((fun st : state ⇒ True ∧ negb (st X =? 0) = true) ->>

(fun st : state ⇒ True ∧ st X ≠ 0)) ∧

((fun st : state ⇒ True ∧ negb (st X =? 0) ≠ true) ->>

(fun st : state ⇒ True ∧ st X = 0)) ∧

(fun st : state ⇒ True ∧ st X ≠ 0) ->> (fun _ : state ⇒ True) [X ⊢> X - 1]) ∧

(fun st : state ⇒ True ∧ st X = 0) ->> (fun st : state ⇒ st X = 0)).

Proof. verify_assn. Qed.

## Automation

Ltac verify :=

intros;

apply verification_correct;

verify_assn.

Theorem dec_while_correct :

dec_correct dec_while.

Proof. verify. Qed.

intros;

apply verification_correct;

verify_assn.

Theorem dec_while_correct :

dec_correct dec_while.

Proof. verify. Qed.

Let's use that automation to verify formal decorated programs
corresponding to informal ones we have seen.

### Slow Subtraction

Example subtract_slowly_dec (m : nat) (p : nat) : decorated :=

{{ X = m ∧ Z = p }} ->>

{{ Z - X = p - m }}

WHILE ~(X = 0)

DO {{ Z - X = p - m ∧ X ≠ 0 }} ->>

{{ (Z - 1) - (X - 1) = p - m }}

Z ::= Z - 1

{{ Z - (X - 1) = p - m }} ;;

X ::= X - 1

{{ Z - X = p - m }}

END

{{ Z - X = p - m ∧ X = 0 }} ->>

{{ Z = p - m }}.

Theorem subtract_slowly_dec_correct : ∀ m p,

dec_correct (subtract_slowly_dec m p).

Proof. verify. (* this grinds for a bit! *) Qed.

Definition swap : com :=

X ::= X + Y;;

Y ::= X - Y;;

X ::= X - Y.

Definition swap_dec (m n:nat) : decorated :=

{{ X = m ∧ Y = n}} ->>

{{ (X + Y) - ((X + Y) - Y) = n

∧ (X + Y) - Y = m }}

X ::= X + Y

{{ X - (X - Y) = n ∧ X - Y = m }};;

Y ::= X - Y

{{ X - Y = n ∧ Y = m }};;

X ::= X - Y

{{ X = n ∧ Y = m}}.

Theorem swap_correct : ∀ m n,

dec_correct (swap_dec m n).

Proof. verify. Qed.