Textbook Examples Verified Using Spec#