プログラミング言語論
第１２回 C言語のsubsetの意味の定義 （演習付） 情報工学科 篠埜 功
今日の内容
C言語の非常に小さいsubsetの意味を操作的意味論（operational semantics）で定義する。 操作的意味論の中の、自然意味論（Natural Semantics）あるいは構造的な操作的意味論(Structural operational semantics）と呼ばれる意味論で定義する。
算術式の意味
<式> ::= <数字列> | <変数> | ( <式> + <式> ) | ( <式> - <式> ) | ( <式> * <式> ) <変数> ::= X | Y | Z <数字列> ::= <数字> | <数字列> <数字> <数字> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 まず、以下のBNF記法で定義される式を対象とし、その意味を操作的意味論で定義する。 （例） (12 + 34), 3 * (45 – X) など。
状態
C言語における変数は、アドレスに付けられた名前。 算術式中の変数の意味は、そのアドレスに格納されている値。 状態とは、アドレス（{X, Y, Z}）から整数への関数。 すべての値が0の状態を初期状態とする。 例えば、 int X = 3; int Y = 4; という状況では、状態は、 { (X, 3), (Y, 4), (Z,0) } である。
メタ変数について
以下で行う意味定義において、式、数字列、整数、変数、状態を表すための変数（メタ変数）として以下のものを用いる。 式 : a, a1, a2等 数字列 : n, n1, n2等 整数 : m, m1, m2等 変数 : x, y等 状態 : σ, σ1, σ2等
算術式の評価
「算術式 a を状態 において評価すると 整数 m が得られる」 という関係を、 < a, > m と表す。 （例） = { (X, 3), (Y, 20), (Z, 13) } のとき、 < ((10 + 20) * 4), > 120 < (5 * (X + 1)), > 20 が成り立つ。
算術式の評価
((10 + 20) * 4) という式は、まず(10 + 20) を評価し、30を得てから、(30 * 4) を評価して120を得る。 すべての式の評価は一定の規則にしたがって行われる。
算術式の評価規則
式が数字列の場合 < n, > m （mは数字列nに対応する整数) 式が変数の場合 < x, > (x) 式が足し算の場合 < a1, > m1 < a2, > m2 < (a1 + a2 ), > m （mはm1とm2の和）
算術式の評価規則（続き）
式が引き算の場合 < a1, > m1 < a2, > m2 < (a1 - a2 ), > m （mはm1とm2の差） 式が掛け算の場合 < a1, > m1 < a2, > m2 < (a1 * a2 ), > m （mはm1とm2の積）
算術式の評価の例1
状態 = { (X, 3), (Y, 20), (Z, 13) } のもとで、 ((10 + 20) * 4) という算術式を評価規則に従って評価してみる。 < ((10 + 20) * 4), > 120 < (10 + 20), > 30 < 4, > 4 < 10, > 10 < 20, > 20
算術式の評価の例2
状態 = { (X, 3), (Y, 20), (Z, 13) } のもとで、 (5 * (X + 1)) という算術式を評価規則にしたがって評価してみる。 < 5 * (X + 1), > 20 < 5, > 5 < X, > 3 < 1, > 1 < (X + 1), > 4
練習問題
状態 = { (X, 3), (Y, 20), (Z, 13) } のもとで、 ((4 + Y) * (5 + Z)) という算術式を評価規則に従って評価せよ。
解答
状態 = { (X, 3), (Y, 20), (Z, 13) } のもとで、 ((4 + Y) * (5 + Z)) という算術式を評価する。 < ((4 + Y) * (5 + Z)), > 432 < (4 + Y), > 24 < 5, > 5 < Z, > 13 < (5 + Z), > 18 < 4, > 4 < Y, > 20
文
これまで、式の意味を定義した。 式の実行（評価）では、値が得られる。（補足： フルセットのCでは式の評価で状態が変化する場合がある。） 文の実行の効果は、状態の変化。 （例）X = 2; このような 代入文を実行すると、Xの値が書き変わる。 この代入文の実行前の状態を とすると、実行後は、状態の中のXの値が2に変わる。（もちろん、もともとXの値が2の場合は変わらない。）
状態に関する記法
状態 において変数xに整数mが代入された時の状態を [ m / x ] と書く。 （例１） X = 2; この 文を実行すると、状態のXの値が書き変わる。 この代入文の実行前の状態を実行前の状態を とすると、実行後の状態は、 [ 2 / X ] となる。 （例２） X = X + 2; この代入文の実行前の状態を実行前の状態を とすると、実行後の状態は、 [ (X) + 2 / X ] となる。 m if y = x, (y) if y x ( [ m / x ]) (y) =
練習問題
状態 = { (X, 10), (Y, 20), (Z, 30) } のとき、 [ 40 / X ] はどういう状態か。
解答
状態 = { (X, 10), (Y, 20), (Z, 30) } のとき、 [ 40 / X ] はどういう状態か。 X以外の値はそのままで、Xの値が40なので、 [ 40 / X ] = { (X, 40), (Y, 20), (Z, 30) } である。
文の定義
文を、代入文あるいはwhile文の並びで定義する。 <文> :: = <変数> = <式> ; | <文> <文> | while (<式>) { <文> } 文を表すためのメタ変数としてc, c1, c2等を用いる。
文の実行
状態1のもとで文cを実行したら状態が2になる ということを、 < c, 1 > 2 と表す。 （例） 状態 { (X, 10), (Y, 20), (Z, 30) }のもとで 文 Y = 40; を実行すると、状態は { (X, 10), (Y, 40), (Z, 30) } になる。これを、 < Y = 40;, { (X, 10), (Y, 20), (Z, 30) } > < { (X, 10), (Y, 40), (Z, 30) } > と書き表す。
文の実行に関する規則
m < x = a;, > [ m / x ] 代入文の場合 文の並びの場合 < c1, > 1 < c2, 1 > 2 < c1 c2, > 2
Description:
プログラミング言語論第１２回 C言語のsubsetの意味の定義 （演習付） 情報工学科 篠埜 功
Tags:
while | において | のもとで | 数字列 | 練習問題 | 規則を使って導出せよ | 状態はどうなるか | とすると
Created:
12/10/2009 2:30:43 AM
>
Share this presentation
|
Comments