Final Homework Excercises

As promised in class, here is a list of problems you should choose from for your last 2 homework assignments. I will grade the same way I have been, just limited to these assignments. If you want to do others, I will happily grade them and give you extra homework points.

Unfortunately exercises are not numbered, so I will simply list the theorems to prove by name.

Equiv.v

1. skip_right
2. if_false
3. swap_if_branches
4. while_true
5. seq_assoc
6. assign_aequiv
7. CIf_congruence

We did not go over assignment in any detail, but I think the last couple of proofs are quite doable.

Hoare.v

1. hoare_post_true
2. hoare_pre_false
3. hoare_asgn_examples1
4. hoare_asgn_examples2
5. hoare_asgn_wrong
6. hoare_asgn_forward
7. hoare_asgn_fwd_exists
8. assertion_sub_ex1'
9. assertion_sub_ex2'
10. if_minus_plus

All homeworks are due on the last day of finals, regardless of what Canvas says. I will try to remember to update the dates.