プログラミング言語論1

プログラミング言語論
第9回 型について
(C言語を題材として。演習付)
情報工学科 篠埜 功
型とは
(例)
int f ( ) {
int x, y;
x = 4;
y = 3 + x;
return y;
}
型付き言語のプログラムは、
型について整合性がとれて
いる必要がある。
型
コンパイル時に、型について(その言語で定めら
れた基準で)整合性がとれているかどうかを検
査する。
プログラムの正当性を部分的に示すことになる。
(実行時のエラーを減少させる。)
静的意味(実行しなくても分かること)の解析。
型の整合性検査は構文解析では行わず、後の
フェーズで行う。
C言語の型宣言について
(例)
int (* a) [13];
この宣言では、変数aはint型の配列(要素数1
3)へのポインタ型であることを示す。
式 (* a) [ j ] (0  j < 13) の型はint型になる。
例えば、式(* a) [0] はint型である。
C言語の型宣言について
(例)
int (*a) [13];
int b [2] [13];
と宣言されているとき、
a=b
は型について整合性のある代入式である。
bは&b[0]のことであり、この代入式の実行後に
(*a) [ j ] = b[0][ j ] (0  j < 13) が成立。
今日は、C言語プログラムが型について整合性がとれて
いるかどうかをチェックする仕組みの基礎を学習する。
(参考)
2次元配列に関し以下の等式が成立する。
&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 ] ;
の宣言を型の後置記法による宣言に直せ。
解答
char ( * ( * y [3] ) ( ) ) [ 5 ] ;
の宣言を型宣言の形に直す。
内側から順に読むと、
[3] * ( ) * [ 5 ] char
となり、逆順にして、
y : char [ 5 ] * ( ) * [3]
となる。
練習問題
(1) int * z;
(2) int C [ 13 ];
を型の後置記法による宣言に直せ。
解答
(1) int * z;
(2) int C [ 13 ];
を後置記法に直すと、
(1) z : int *
(2) C : int [13]
となる。
練習問題
(1) int ( * daytab ) [13];
(2) int B[2] [13];
を型の後置記法による宣言に直せ。
解答
(1) int ( * daytab ) [13];
(2) int B[2] [13];
を後置記法に直すと、
(1) daytab : int [13] *
(2) B : int [13] [2]
となる。
例
char ( * ( * y [3] ) ( ) ) [ 5 ] ;
の宣言のもとで、
式 y [ 2 ] はどういう型を持つか。
y : char [ 5 ] * ( ) * [3]
となり、一番外側の[3]を取り除いて、
y [2] : char [ 5 ] * ( ) *
となる。
練習問題
int ( * daytab ) [13];
の宣言のもとで、
式 * daytab の型は何か。
解答
int ( * daytab ) [13];
を後置記法に直すと、
daytab : int [13] *
となり、式 * daytab の型は
* daytab : int [13]
となる。
推論規則
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 : int [13] [2]
となる。これを出発点とし、式B[1]の型を推論規則
を使って導出する。
B : int [13] [2]
B [1] : int [13]
練習問題
int B [2] [13] ;
の宣言のもとで、
式 B [1] [4] の型は、何になるか。
これを、型宣言から推論規則で導け。
解答
int B [2] [13] ;
の宣言のもとで、
まず、後置記法で書きなおすと、
B : int [13] [2]
となる。これを出発点とし、式B[1][4]の型を推論規
則を使って導出する。
B : int [13] [2]
B [1] : int [13]
B [1] [4] : int
配列型について
配列型について、以下の推論規則を追加。
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]
が型に関して整合性があることを示せ。
解答
A : int [10]
A[1] : int
p : int *
& A[1] : int &
p = & A[1] : int &