プログラミング言語論1

プログラミング言語論
第11回型について
（C言語を題材として。演習付）
情報工学科木村昌臣
篠埜功
型
int f ( ) {
int x, y;
x = 4;
y = 3 + x;
return y;
}
型について整合性がとれている必要がある。
型
コンパイル時に、型について（その言語で定め
られた基準で）整合性がとれているかどうか
を検査する。
プログラムの正当性を部分的に示すことになる
。（実行時のエラーを減少させる。）
静的意味（実行しなくても分かること）の解析。
型の整合性検査は構文のチェックに属するが、
構文解析では行わず、後のフェーズで行う。
C言語の型宣言について
（例）
int (* daytab) [13];
この宣言では、変数daytabはint型の配列（要
素数１３）へのポインタ型であることを示す。
式 (* daytab) [ j ] (0 <= j < 13) の型は
int型でなければならない。
C言語の型宣言について
（例）
int (* daytab) [13];
int B [2] [13];
と宣言されているとき、
daytab = B
は正しい代入式である。
（確認） Bの値が&B[0]であり、この代入文の実行後に
* daytab = *&B[0] = B[0] が成立し、
(* daytab) [ j ] = B [0] [ j ] (0 <= j < 13) が成立。
今日は、C言語プログラムが型について整合性がとれて
いるかどうかをチェックする仕組みの基礎を学習する。
C言語の型宣言について
B[ i ] は左辺値（アドレス）をもつ定数であり、B[ i ]
の値は &B[ i ] [ 0 ] である。
２次元配列に関する等式
&B[ i ] + j = &B[ i + j ]
&B[ i ] [ j ] + k = &B[ i ] [ j + k ]
i, j, kは整数。
C言語の型宣言について
char ( * ( * x ( ) ) [ ] ) ( )
の宣言の意味は？
内側から順番に優先順位にしたがって読む。
( ) * [ ] * ( ) char
となる。
x : char ( ) * [ ] * ( )
を型宣言、
char ( ) * [ ] * ( )
を型の後置記法と呼ぶこととする。
優先順位
char ( * ( * x ( ) ) [ ] ) ( )
の宣言の意味は？
( ) が一番優先順位が高く、* より [ ] が
優先順位が高い。
内側から順番に優先順位にしたがって読むと、
( ) * [ ] * ( ) char
となる。
練習問題
char ( * ( * y [3] ) ( ) ) [ 5 ]
の宣言を型の後置記法による宣言に直せ。
練習問題
(1) int * z
(2) int C [ 13 ]
を型の後置記法による宣言に直せ。
練習問題
(1) int ( * daytab ) [13]
(2) int B[2] [13]
を型の後置記法による宣言に直せ。
例
char ( * ( * y [3] ) ( ) ) [ 5 ]
の宣言のもとで、
式 y [ 2 ] はどういう型を持つか。
y : char [ 5 ] * ( ) * [3]
となり、一番外側の[3]を取り除いて、
y [2] : char [ 5 ] * ( ) *
となる。
練習問題
int ( * daytab ) [13]
の宣言のもとで、
式 * daytab の型は何か。
推論規則
e:[n]
e[i]:
e:()
e():
e:*
*e:
0 <= i < n, n は正の整数。
eは式、 は型を表すメタ変数（説明の
ための変数）。
例
int ( * daytab ) [13]
の宣言のもとで、
式 * daytab の型は、int [13]であった。
これを、型宣言から推論規則で導くことができる。
daytab : int [13] *
* daytab : int [13]
例
int ( * daytab ) [13]
の宣言のもとで、
式 (* daytab) [3] の型は、何になるか。
これを、型宣言から推論規則で導くと、以下のよう
になる。
daytab : int [13] *
* daytab : int [13]
(* daytab) [3] : int
練習問題
int B [2] [13]
の宣言のもとで、
式 B [1] の型は、何になるか。
これを、型宣言から推論規則で導け。
練習問題
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] &
注意事項
実際のC言語の型チェックのためには、推論規則
の追加をすればよい。
C言語では、共用体の型はチェックしない（できない
）。中にどの型のデータが入っているかはプログ
ラマが認識していなければならない。
練習問題
p : int *
A : int [10]
の型宣言があるとき、代入式
p = & A[1]
が型に関して整合性があることを示せ。

Download Report