Project 2 - Hoare Logic

Following are a set of exercises to help you practice reasoning with Rocq and Hoare logic. We will be working through some of these in class and others will be up to you. You must submit solutions for all of them by the due date.

For working the exercises I would suggest starting with Hoare.v and add your solutions to the end of the file. That way you will know that everything we’ve discussed in class is in scope for your proofs.

Please watch carefully for updates to this assignment and blog posts. Exercises for Hoare Triples are tricky to get right. I will post answers to questions on the blog.

Exercise 1. Write a precondition P and verify correctness for each assignment:

{{ P }} X := 5 {{ X = 5 }}
{{ P }} X := X + 1 {{ X ≤ 10 }}

Exercise 2. Determine which of these are valid Hoare triples. For the invalid ones, give a concrete counterexample state:

{{True}} X := 5; Y := 0 {{X = 5}}
{{X = 2 /\ X = 3}} X := 5 {{X = 0}}
{{ True }} X := X + 1 {{ X > 0 }}
{{ X ≠ 0 }} X := X - 1 {{ X ≥ 0 }}
{{ X > 5 }} X := X - 1 {{ X > 4 }}
{{False}} skip {{True}}
{{True}} skip {{False}}

Exercise 3. Prove the following triple valid using the consequence and assignment rules:

{{ X = n }}
  Y := X;
  X := Y + 1
{{ X = n + 1 }}

Exercise 4. Prove both of these directly from valid_hoare_triple:

Theorem hoare_post_true : forall (P Q : Assertion) c,
  (forall st, Q st) -> {{P}} c {{Q}}.

Theorem hoare_pre_false : forall (P Q : Assertion) c,
  (forall st, ~ (P st)) -> {{P}} c {{Q}}.

Exercise 5. Fill in the precondition P and prove each triple using only hoare_asgn:

Example hoare_asgn_examples1 :
  exists P, {{ P }} X := 2 * X {{ X <= 10 }}.

Example hoare_asgn_examples2 :
  exists P, {{ P }} X := 3 {{ 0 <= X /\ X <= 5 }}.

Exercise 6. Fill in the post-condition Q and verify:

{{ True }}
  if X ≤ 0 then Y := 0 else Y := X end
{{ Q }}

Exercise 7. Fill in the precondition P and verify using eapply hoare_consequence_pre:

{{ P }} X := X * 2 + 1 {{ X > 5 }}

Exercise 8. Prove:

{{ X > 0 }} X := X + 1 {{ X ≥ 2 }}

Exercise 9. The “obvious” forward assignment rule is incorrect:

{{ True }} X := a {{ X = a }}

Find a specific a for which this fails and complete:

Theorem hoare_asgn_wrong : exists a : aexp,
  ~ {{ True }} X := a {{ X = a }}.

Hint: Think about what happens when a itself mentions X.

Exercise 10. Prove these using eapply hoare_consequence_pre, apply hoare_asgn, and the assertion_auto tactic defined in the text:

Example assertion_sub_ex1' :
  {{ X <= 5 }} X := 2 * X {{ X <= 10 }}.

Example assertion_sub_ex2' :
  {{ 0 <= 3 /\ 3 <= 5 }} X := 3 {{ 0 <= X /\ X <= 5 }}.

Exercise 11. Translate this program into a Rocq proof, supplying the intermediate assertion explicitly to hoare_seq:

{{ True }} ->>
{{ 1 = 1 }}
  X := 1
{{ X = 1 }} ->>
{{ X = 1 /\ 2 = 2 }};
  Y := 2
{{ X = 1 /\ Y = 2 }}

Exercise 12. Consider an Imp program that swaps X and Y using arithmetic only:

Definition swap_program : com :=
   X := X + Y; Y := X - Y; X := X - Y.

verify it in Rocq for the specification:

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

Hint: Use X := X + Y; Y := X - Y; X := X - Y. Work backwards from the post-condition. Use eapply hoare_seq and eapply hoare_consequence_pre.

Exercise 13. Show that this triple is not valid for all a and n:

Theorem invalid_triple : ~ forall (a : aexp) (n : nat),
    {{ a = n }} X := 3; Y := a {{ Y = n }}.

Hint: Use specialize H with (a := X) (n := 0). The key insight: after X := 3, the expression a = X no longer refers to the original value of X. Derive two contradictory values for st' Y from the same final state.

Exercise 14. Hoare.v extends Imp with a one-sided conditional if1 b then c end that does nothing when b is false.

Add two evaluation rules to ceval for if1 (true and false cases).

State and prove a Hoare rule hoare_if1 modeled on hoare_if but handle the case where the guard is false like skip.

Use your new rule to prove:

Lemma hoare_if1_good :
  {{ X + Y = Z }}
    if1 Y <> 0 then X := X + Y end
  {{ X = Z }}.