Some solutions to the exercises from the excellent book "Program Proofs" by K. Rustan M. Leino in SPARK 2014.
