プログラミング言語論1

プログラミング言語論
第12回型について（先週の続き）
および
C言語のsubsetの意味の定義
（演習付）
情報工学科木村昌臣
篠埜功
先週の補足１
型の後置記法について
今は関数の引数がない等、制限されたCを考えてい
るので、型宣言の構造が一列になっている。
（例）
char ( * (* x ( ) ) [ ] ) ( ) ; が
x : char ( ) * [ ] * ( ) のように一列に書けたのは、
xの型が Sfn (Pnt (Arr (Pnt (Sfn (Char)))))
のように一列の構造を持っていたから。
(Sfnは、引数を持たない、単純な関数型のつもり)
Simple
先週の補足１
関数に引数がある場合は、関数型の部分で返り値の
型と引数の型の２つの情報が必要になり、そこで枝分
かれが起こり、構造が一列ではなくなる。
char ( * (* x ( int ) ) [ ] ) ( double ) ;
の場合、xの型は、
Fn (Int, Pnt (Arr (Pnt (Fn (Double, Char)))))
のように枝分かれがある。
一般には、C言語の型は木構造をなす。
先週の補足２
配列の左辺値について
（例）
int main () {
int a [10];
printf (“%p\n”, a); /* aの値は、a[0]のアドレス &(a[0]) */
printf (“%p\n”, &a); /* &aの値は、aのアドレス */
printf (“%p\n”, a+1);
/* 4が足される */
printf (“%p\n”, (&a)+1); /* 40が足される */
return 0;
intが4byteの場合
}
a と &aの値（右辺値）は同じだが、型が異なる。
a は要素数１０の配列型、&aは要素数１０の配列へのポインタ型。
練習問題
int B [2] [13]
の宣言のもとで、
式 B [1] [4] の型は、何になるか。
これを、型宣言から推論規則で導け。
配列型について
配列型について、以下の推論規則を追加。
e:[n]
e:&
ここで、 e :  &は、 e :  *かつeは左辺値を持た
ないことを表すものとする。
この推論規則は、一番外側が配列型であれば、それ
をポインタ型に変更してもよいということを表している。
代入演算子 = について
代入演算子 = について、以下の推論規則を追加。
e :  e’ : 
e = e’ : 
ただし、eは左辺値を持つ式であり、かつ定数ではな
い。
演算子&について
演算子&について以下の推論規則を追加。
e:
&e :  &
e:&
*e :
e :  * e’ :  &
e = e’ :  &
ただし、 の一番右側（一番外側）は&ではない。
最初の例
daytab : int [13] *
B : int [13] [2]
の型宣言があるとき、
daytab = B
が型について整合性があることを確認。
daytab : int [13] *
B : int [13] [2]
B : int [13] &
daytab = B : int [13] &
練習問題
p : int *
A : int [10]
の型宣言があるとき、代入式
p = & A[1]
が型に関して整合性があることを示せ。
今日のトピック
• C言語の非常に小さいsubsetの意味を操
作的意味論（自然意味論）で定義する。
算術演算式の意味
以下のBNF記法で定義される式を対象とし、その意
味を操作的意味論で定義する。
<式> ::= <数>
| <変数>
| ( <式> + <式> )
| ( <式> - <式> )
| ( <式> * <式> )
<変数> ::= X | Y | Z
<数字> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
<数> ::= <数字> | <数> <数字>
（例） (12 + 34), 3 * (45 – X) など。
状態
C言語における変数は、アドレスに付けられた名前。
算術式中の変数の意味は、そのアドレスに格納されている値。
状態とは、アドレス（{X, Y, Z}）から整数Zへの関数。
すべての値が0の状態を初期状態とする。
例えば、
int X = 3;
int Y = 4;
という状況では、状態は、
{ (X, 3), (Y, 4), (Z,0) }
である。
算術演算式の操作的意味
前ページで定義した式の構文解析結果を対象として
意味を定義する。
構文解析結果は以下の式で表す。
a ::= n | x | (a + a) | (a – a) | (a * a)
aは、式（の構文解析結果）を表す。
nは、整数を表す。
xは、変数を表す。
数(数字の列)は、構文解析の段階で整数に変換すること
にする。
式の評価
「算術式 a を状態  において評価すると
整数 n が得られる」という関係を、
< a,  >  n
と表す。
（例）
0 = { (X, 3), (Y, 20), (Z, 13) } のとき、
< ((10 + 20) * 4), 0 >  120
< (5 * (X + 1)), 0 >  20
が成り立つ。
式の評価規則
((2 + 3) * 4) という式は、まず(2 + 3) を評価し、5を得てから、
(5 * 4) を評価して20を得る。
すべての式の評価は一定の規則にしたがって行われる。
式の評価規則
式が整数の場合
< n,  >  n
式が変数の場合
< x,  >   (x)
式が足し算の場合
< a0,  >  n0
< a1,  >  n1
< (a0 + a1 ),  >  n
（ここで、nはn0と
n1の和）
式の評価規則（続き）
式が引き算の場合
< a0,  >  n0
< a1,  >  n1
< (a0 - a1 ),  >  n
（ここで、nはn0と
n1の差）
式が掛け算の場合
< a0,  >  n0
< a1,  >  n1
< (a0 * a1 ),  >  n
（ここで、nはn0と
n1の積）
式の評価の例1
状態 0 = { (X, 3), (Y, 20), (Z, 13) } のもとで、
((10 + 20) * 4) という算術式を評価規則に従って評価し
てみる。
< 10, 0 >  10
< 20, 0 >  20
< (10 + 20), 0 >  30
< 4, 0 >  4
< ((10 + 20) * 4), 0 >  120
式の評価の例2
状態 0 = { (X, 3), (Y, 20), (Z, 13) } のもとで、
(5 * (X + 1)) という算術式を評価規則にしたがって評
価してみる。
< X, 0 >  3
< 5, 0 >  5
< 1, 0 >  1
< (X + 1), 0 >  4
< 5 * (X + 1), 0 >  20
練習問題
状態 0 = { (X, 3), (Y, 20), (Z, 13) } のもとで、
((4 + Y) * (5 + Z)) という算術式を評価規則に従って
評価せよ。
文
• これまで式の意味を定義した。
• 式の実行（評価）では、値が得られる。（フルセットの
Cでは式の評価で状態が変化する場合がある。）
• 文の実行の効果は、状態の変化。
（例）X = 2;
このような代入文を実行すると、Xの値が書き変わる。
この代入文の実行前の状態を とすると、実行後は、状
態の中のXの値が２に変わる。（もちろん、もともとXの値
が２の場合は変わらない。）
状態に関する記法
• 状態において変数xに値mが代入された時の状
態を [ m / x ] と書く。
( [ m / x ]) (y) =
m
if y = x,
 (y) if y  x
（例１） X = 2;
この文を実行すると、状態のXの値が書き変わる。
この代入文の実行前の状態を実行前の状態を とすると、実行後の
状態は、 [ 2 / X ] となる。
（例１） X = X + 2;
この代入文の実行前の状態を実行前の状態を とすると、実行後の
状態は、 [  (X) + 2 / X ] となる。
練習問題
状態  = { (X, 10), (Y, 20), (Z, 30) } のとき、
 [ 40 / X ] はどういう状態か。
文の定義
文を、代入文の並びで定義する。
<文> :: = <変数> = <式> ;
| <文> <文>
文の構文解析結果を以下で表す。
c ::= x = a;
| c c
c は文を表す。
x は変数を表す。
a は算術式を表す。
文の実行
状態のもとで文cを実行したら状態が’になる
ということを、
<c,  >  ’
と表す。
（例）状態 { (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) } >
と書き表す。
文の実行に関する規則
代入文の場合
<a,  >  n
< x = a;,  >   [ n / x ]
文の並びの場合
<c1,  >  1 <c2, 1>  2
< c1 c2,  >  2
例１
状態  = { (X, 10), (Y, 20), (Z, 30) } において文Y=40; を
実行すると状態はどうなるか。
< 40,  >  40
< Y = 40;,  >   [ 40 / Y ]
< { (X, 10), (Y, 40), (Z, 30) } >
例２
状態  = { (X, 10), (Y, 20), (Z, 30) } において
文X = 3; Y=40; を実行すると状態はどうなるか。
< 3,  >  3
< X = 3;,  >   [ 3 / X ]
< 40,  >  40
< Y = 40;,  [ 3 / X ] >  ( [3 / X]) [ 40 / Y ]
< X = 3; Y = 40;  >  ( [3 / X]) [ 40 / Y ]
< { (X, 3), (Y, 40), (Z, 30) } >
練習問題
状態  = { (X, 10), (Y, 20), (Z, 30) }
において、文 X = Y + 2; Y = Y + 3 を実行したら
状態はどうなるか。規則を使って導出せよ。

Download Report