公理的意味論を使ってプログラムの正しさを証明する (1)

公理的意味論 (axiomatic semantics) を使って、 プログラムが正しく動くことを証明しようとするこころみ。 まとめ: 公理的意味論では、まず手続き型プログラムの仕様を数学的な命題として記述する。 つぎに、コード中の各部分が正しいふるまいをすることを示し、 それによってプログラム全体が仕様を満たしていることを示す。 公理的意味論において重要なのは「不変式 (invariant)」の考え方である。 これはループ内の同じ場所を実行したときつねに成り立っているような命題で、 不変式を使うと、ある処理を繰り返した結果、正しい値が得られるということを 証明することができる。 この動画では、以下のような関数 mypow を例に、 不変式の基本的なアイデアについて説明する。 (Python にはすでにべき乗を計算する関数 pow や演算子 ** があるが、 ここではループと掛け算だけを使

[todesking]

これ公理的意味論と関係あるのか……