Invariants Text
My book, Invariants: a Generative Approach to Programming was published by College Publications in 2008. It discusses loop invariants and class invariants, arguing that these should be used as reasoning tools when writing programs. Invariants are introduced in the context of games and puzzles, searching, sorting, graphs, dynamic programming, context-free grammars, and refinement, written at the level of CS2.
I've released the book as open-source under the GNU Free Documentation License. The book is typeset in LaTeX; the figures are Graphviz graphs. I would be grateful for any additions/corrections to content, typesetting, etc., and equally pleased if you use/adapt the text for your class.
If you'd like a hardcopy, the book is available from Amazon.