プログラムの正当性証明入門(2) - 共立出版コンピュータサイエンス誌『bit』