📝プログラミング意味論

📝プログラミング意味論

up: 📁Programming Paradigms

プログラム意味論 | 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 #

定理証明支援系言語.

モデル検査 #

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

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

Tags

Backlinks