プログラム検証入門(2)_自動検証はなぜ困難が，プログラム意味論とは