補足 - Milresh

補足
言語の意味論
意味論
• プログラミング言語の意味を与える方法
– どの文面はどの意味を持つのか
• ３つの方法
– 操作的意味論 (operational semantics)
• 抽象機械(abstract machine)やインタプリタを定義
• Syntax directed approach ( G. Plotkin )
– 各文面単位ごとに、推論規則または公理にプログラムの文面を取り
込んだ理論体系によってプログラムの挙動を記述方法
– 公理的意味論 (axiomatic semantics)
• Hoare logic
– 表示的意味論 (denotational semantics)
• 数学関数
状態σ
• 状態とは、各変数・メモリ語の現在持つ・格納
している値のこと
– 写像(関数)で表現され、σ: Loc → N (Loc は
localtion, Nは数)
– Xが変数であれば、σ(X)はその値
• 式の評価は数学での意味とする
<a0, σ> → n0
<a1, σ> → n1
______________________________
<a0 + a1, σ> → n0 plus n1
言語の+ operator
数学の加算
命令に対する推論規則
• Assignment
<a, σ> → m
__________________
<X := a, σ> → σ[X/m]
• Sequencing
<c0, σ> → σ’’
<c1, σ’’> → σ’
__________________________________
<c0;c1, σ> → σ’
命令に対する推論規則(2)
• Conditionals
<b, σ> → true <c0, σ> → σ’
______________________________
<if b then c0 else c1, σ> → σ’
• While-loops
<b, σ> → false
______________________
<while b do c, σ> → σ
<b, σ> → true <c,σ> →σ’’ <while b do c, σ’’> → σ’
_______________________________________________
<while b do c, σ> → σ’

Download Report