📝プログラミング意味論

🔥虚無との戦い

プログラム意味論 | Semanticsとは

プログラム意味論. formal semantics, mathmatical semantics ともいう.

プログラムの正しさや正確さを理論づけるための方法.

形式的検証 - Wikipedia

4 つのアプローチがある.

操作的意味論
公理的意味論
記述的意味論
論理的意味論

Operational semantics: 操作的意味論

Explains a program in terms of its execution on a rigorously defined abstract machine

どのパラダイムにおいても適用できる.

Kernel Language
Abstract Machine

ref: 操作的意味論 - Wikipedia

プログラムの正しさを数学的に証明することを目指す.

Specification: プログラムの入力と出力を定義したものを
Program: プログラミング言語によってかかれたデータ

Program が Specification を満たしているかを証明する. そのために,

Semantic (意味の対応付け)
Abstruct Machine (抽象化された実行環境)

という概念を導入する.

Program は kernel Language に分解され, Kernel Language の構成要素が Abstruct Machine と対応付けられる.

                          Semanitic
Program --> kernel Language ----->  Specification
                          Abstrucut Machine

コンピュータの理論は, Kernel Language と Abstruct Machine によって離散数学 (Discrete Mathmatics) を元に議論することが可能になる.

Mathematical induction

recursive function (再帰関数) の正しさは, 数学的帰納法 (mathematical induction) で証明する.

example

Specification

0! = 1
n! = n × (n-1)!  when n>0

Program

fun {Fact N}
   if N==0 then 1 else N*{Fact N-1} end
end

Semanitc Expression

E={Fact → fact, N → n, R → r} (AbstcutMachine)
σ={fact=(proc ... end,CE),n=0,r} (memory)
CE={Fact → fact}. ( Contectual Environment)
 
{Fact N R}, E, σ

広義の意味では, 関数に forcusing したプログラミング.

Axiomatic semantics: 公理的意味論

Explains a program as an implication: if certain propertieshold before the execution, then some other properties will hold after the execution

状態があるモデルに適している.ステートマシンの証明. 数理論理学に基づいてプログラムの正当性を証明する手法.

公理的意味論 - Wikipedia

Coq

定理証明支援系言語.

モデル検査

モデル検査 - Wikipedia

VDM

モデル検査用のソフトウェア
- VDM information web site - VDM とは?

Proof-Driven Development (証明駆動開発)

Denotational semantics: 記述的意味論

Explains a program as a function over an abstract domain, which simplifies certain kinds of mathematical analysis of the program

宣言的プログラミングの証明に適する.

Logical semantics: 論理的意味論

Explains a program as a logical model of a set of logicalaxioms, so program execution is deduction: the result of a program is a true property derived from the axioms

宣言的計算モデルに適する.

up: 📁Programming Paradigms