プログラム検証入門(完)_構造的プログラミングとの恋愛，「検証はプログラムの正しさを保障しない」か?