This is one of the very few books we've seen that tries to make practical sense and takes formal mathematical methods through application. (This replaces Baber's earlier book, "The Spine of Software: Designing Provably Correct Software--Theory & Practice.")