プログラムの仕様とその証明を数学で記述する本にあるだろうね。