プログラミング言語論 第6回　型 情報工学科　篠埜　功.

Presentation on theme: "プログラミング言語論 第6回　型 情報工学科　篠埜　功."— Presentation transcript:

1 プログラミング言語論 第6回　型 情報工学科　篠埜　功

2 型付き言語 静的型付き言語(statically typed language)
コンパイル時に型の整合性を検査する （例）C, Java, Pascalなど 動的型付き言語(dynamically typed language) 実行時に型の整合性を検査する （例）Lisp, Emacs Lisp, Schemeなど

3 型とは （例） int f ( ) { int x, y; x = 4; y = 3 + x; return y; }
静的型付き言語のプログラムは、コンパイル時に型について整合性がとれている必要がある。

4 型検査 コンパイル時に、型について（その言語で定められた基準で）整合性がとれているかどうかを検査する。 プログラムの正当性を部分的に示すことになる。（実行時のエラーを減少させる。） 型情報は静的意味（実行しなくても分かる情報）であり、型検査は静的意味の解析の一種。 型検査はコンパイラの中で、構文解析より後のフェーズで 行う。

5 C言語の変数宣言について （例） int (*a) [13]; この宣言では、変数aはint型の配列（要素数13）へのポインタ型であることを示す。 式 (*a) [ j ] (0  j < 13) の型はint型になる。 例えば、式(* a) [0] はint型である。

6 C言語の変数宣言について （例） int (*a) [13]; int b [2] [13]; と宣言されているとき、 a = b は型について整合性のある代入式である。bはコンパイル時に&b[0]に置き換えられる。この代入式の実行後に等式 (*a) [ j ] = b[0][ j ] (0  j < 13) が成立する。これは、*a = *b = *(&b[0]) = b[0] に[ j ] をつければ得られる。プログラムが型について整合性がとれているかどうかをチェックする仕組みの基礎を学習する。

7 C言語の変数宣言について char ( * ( * x ( ) ) [3] ) ( ) ; の変数宣言の意味は？ 内側から順番に優先順位（次ページ記載）にしたがって読んでいき、最後にcharを読む。すると ( ) * [3] * ( ) char となる。これを逆順にすると char ( ) * [3] * ( ) となる。これを型の後置記法と呼ぶことにする（一般に通用する用語ではない）。これをx : の後に書いた x : char ( ) * [3] * ( ) を型の後置記法による宣言と呼ぶことにする。

8 優先順位 優先順位は、高い順に( ), [ ], * である。宣言されている変数xからこの優先順位に従って読んでいけばよいが、優先順位の括弧がついている場合は順番は変わる。前ページの変数宣言の例 char ( * ( * x ( ) ) [3] ) ( ) ; で優先順位の括弧は の太字の部分である。内側（宣言されている変数x）から順番に優先順位に従って読むと、 ( ) * [3] * ( ) char となる。

9 練習問題1 C言語の変数宣言 char ( * ( * y [3] ) ( ) ) [5] ; を型の後置記法による宣言に直せ。

10 練習問題2 C言語の変数宣言 (1) int * z; (2) int c [13]; を型の後置記法による宣言に直せ。

11 練習問題3 C言語の変数宣言 (1) int (*a) [13]; (2) int b[2][13]; を型の後置記法による宣言に直せ。

12 例 char ( * ( * y [3] ) ( ) ) [5] ; の宣言のもとで、 式 y [2] はどういう型を持つか。 y : char [5] * ( ) * [3] となり、一番外側の[3]を取り除いて、 y [2] : char [5] * ( ) * となる。

13 練習問題4 C言語の変数宣言 int (*a) [13]; のもとで、式 *a の型は何か。

14 推論規則 e :  [ n ] e [ i ] :  e :  ( ) e ( ) :  e :  * * e : 
0  i < n, n は正の整数。 eは式、 は型を表すメタ変数（説明のための変数）。

15 例 C言語の変数宣言 int (*a) [13] ; のもとで、式 *a の型は、int [13]であった（練習問題4参照）。これを、型の後置記法による宣言から推論規則で以下のようにして導くことができる。 a : int [13] * *a : int [13]

16 例 C言語の変数宣言 int (*a) [13] ; のもとで、式 (*a) [3] はint型である。これを、型の後置記法による宣言から推論規則で以下のように導くことができる。 a : int [13] * *a : int [13] (*a) [3] : int

17 練習問題5 C言語の変数宣言 int b [2] [13] ; のもとで、式 b [1] の型を、変数bの型の後置記法による宣言から推論規則で導け。

18 練習問題6 C言語の変数宣言 int b [2] [13] ; のもとで、式 b [1] [4] の型を、変数bの型の後置記法による宣言から推論規則で導け。

19 配列型について e :  [ n ] e :  & 配列型について、以下の推論規則を追加。
ここで、 e :  &は、 e :  *かつeは左辺値（アドレス）を持たないことを表すものとする。 この推論規則は、一番外側が配列型であれば、それをポインタ型に変更してもよいということを表している。

20 代入演算子 = について e :  e’ :  e = e’ :  代入演算子 = について、以下の推論規則を追加する。

21 演算子&について e :  &e :  & e :  & * e :  e :  * e’ :  & e = e’ :  &
演算子&について以下の推論規則を追加する。 e :  &e :  & e :  & * e :  e :  * e’ :  & e = e’ :  & ただし、 の一番右側（一番外側）は&ではない。

22 最初の例 C言語の変数宣言 a : int [13] * b : int [13] [2] のもとで、代入式 a = b が型について整合性があることを以下のようにして確認できる。 b : int [13] [2] b : int [13] & a : int [13] * a = b : int [13] &

23 注意事項 実際のC言語では、関数に引数がある。その他、構造体、共用体など、今回扱っていない構文がある。 C言語では共用体の型はチェックしない。中にどの型のデータが入っているかはプログラマが認識していなければならない。

24 練習問題7 C言語の変数宣言 p : int * a : int [10] のもとで、代入式 p = &a[1] が型に関して整合性があることを示せ。