プログラム理論特論 第8回 亀山幸義 [email protected] http://logic.is.tsukuba.ac.jp/~kam/progtheory 中間レポートについて 必ず返事します。5日以上たって返事がこないときはもう一 度メイルしてください。 6月2日17:00までに到着したレポートについては受理した旨の返 事をメイルしました。 それ以降も順次メイルします。 書式上の問題がいくつか散見されました。 「テキスト、PS, PDFのどれか」と指定しているのにWORDで送ってくる 学籍番号と名前をレポートに冒頭に書かない(メイル自身の署名とは 別に、レポートのファイルにも名前を書くのは当然) メイル本文に、何の断り書きもなく、いきなりレポートが添付されてい る。(当然、どの授業の何というレポートを提出しようとしているか、書 くべき。書類を誰かに郵送するときには、必ず「送り状」をつけるべき であるのと同様) ただ、中間レポートの採点で問題にすることはありません。 レポートの解答等は後に web page に掲載します。 今日のあらすじ 今回: オブジェクト指向言語の型システム 抽象データ型 6月10日は休講です。 次回は6月17日です。 Pointクラスのオブジェクトたち y (-1,2) (3,5) (1,1) x ColoredPointクラスのオブジェクトたち y (-1,2) (3,5) (1,1) x オブジェクト指向 Object-Oriented 制御中心ではなくデータ中心の記述 プログラムは、手続きや関数の定義の集まりではなく、 データ定義の集まり 特徴 情報の隠蔽、カプセル化 継承:プログラムの再利用 Pointクラスの定義を利用してColoredPointクラスを定義する サブタイピング クラスの定義で列挙された操作関数(メソッド)以外では、オブジェ クトの内部構造をさわることはできない Pointクラスのオブジェクトを引数にとる関数には、ColoredPointク ラスのオブジェクトも適用できる self/super を用いた再帰呼び出し 抽象データ型 「普通」のデータ型(具体的なデータ型、抽象データ 型でないデータ型) この講義でこれまで対象としてきたデータ型 どのように型を構成するかを具体的に指定することによっ て、データ型を定める。 例: real ×(int→ string) 型の構成方法から自動的に以下のことが定まる その型をもつデータ(プログラム)をどうやって構成するか 例 MとNから(M,N)を構成する その型をもつデータをどうやって使うか 例 (M,N)からその left や right をとる 抽象データ型 Abstract Data Type, ADT 抽象データ型 型をどのように構成するか、ではなく、その型を 持つデータをどうやって構成するか、どうやって 使うかを定める [逆転の発想] データ型の実現ではなく、データ型の仕様 例:「学生名簿」データ型 具体的データ型 学籍番号と氏名のペアをリストにしたもの 学生を一人追加、学籍番号に対応する学生の氏名を探す 例:「学生名簿」データ型 抽象データ型 学生名簿型のデータには以下の操作だけを使う 空の学生名簿を作る new 学生を一人追加 add 学籍番号に対応する学生の氏名を探す assoc 例:「学生名簿」データ型 具体的なデータ型と抽象データ型の関係 具体的なデータ型は、抽象データ型の条件(仕様)を満た す。 抽象データ型の条件を満たす具体的なデータ型の構成方 法は、ここで与えたものに限らない。 例:「スタック」抽象データ型 スタックは、new, push, pop 操作と、スタックトップの 要素を知る関数、スタックが空かどうか知るための関 数が備わっているデータ構造 これ以外の性質は一切 仮定しない pop(new)、top(new)の値 は何でも良い 抽象データ型の有用性 抽象データ型は「(外部)仕様」、具体的なデータ型は「実装」 抽象データ型 具体的なデータ型 実装方法を外から見ることができる meibo型データにおいて、「”Nakajima” の次に “Ito” が登録されてい るかどうか」を知ることはできるか? ソフトウェアの段階的開発 stepwise refinement 記述された型情報、等式は外から見え、それ以外のこと(その抽象データ 型をどう実装しているか)は見えない[情報の隠蔽, information hiding] 最初に、抽象データ型を用いてアルゴリズムを設計し、 次に、これを具体的なデータ型で置き換える ソフトウェアの保守(更新)において 同じ抽象データ型を満たす、より高速のデータ型に置き換えることが 可能(ソフトウェアの性能向上) 大規模ソフトウェアの分散開発 ソフトウェア部品の再利用 抽象データ型の理論[参考] 等式のみで記述されている場合、抽象データ型を満 たす「最も一般的な(具体的な)データ型」が存在する ことが保証できる。[initial algebra, 始代数] 最も一般的 OBJなどの言語 では、ADTを書 けばそのまま 具体的な定義 と思って実行し てくれる 抽象データ型を満たす 具体的なデータ型 ADTからオブジェクトへ オブジェクトは、ADTの考え方に影響されて いる しかし、ADTと同じではない。 クラスの定義には、「具体的な実装方法」も記述 されている。 さらに、JAVA言語などでは、「外に見せるもの」 「外に見せないもの」を細かく指定できるように なっている。 継承inheritanceとサブタイピング 一番上の クラス Pointクラス ColoredPoint クラス ○○ColoredPoint クラス ○○Point クラス f: Point → int f(x) の x の位置に 書けるオブジェクトの クラスは? x: ColoredPoint f: Point→int から f(x): int を導けるようにしたい OO言語を型理論で表現・理解する OO言語 型理論 クラス レコード型 オブジェクト レコード型をもつ項 メソッド 関数 継承 サブタイプ OO言語の型理論:レコード型 OO言語の型理論:サブタイピング1 OO言語の型理論:サブタイピング2 サブタイピングの例 int ≦ real と仮定する int →int ≦ int →real {x:int,y:real,z:real} ≦ {x:int,y:real,z:real} real→int ≦ int→int real→int ≦ int→real ! int→int と real→real の間に≦関係は成立しない {x:int,y:int,z:int} ≦ {x:int} {xy:{x:int,y:real}, z:int} ≦ {xy:{x:real,y:real},z:real} 例(の準備) 要素を1つしか持たない型 Unit 要素の値に意味がないときに使用する 0引数の関数を、1引数の関数とみなしたいとき print文を、関数とみなしたいとき Unit型はレコード型の一種とみなすこともできる。 Unit ={} 例:Pointクラス 例:ColoredPointクラス 例:ColoredPointクラス 例:ColoredPointクラス 例 OO言語の型理論 型付きラムダ計算に、レコード型とサブタイピングを 加えた体系 型の健全性定理は成立する 型推論は困難 OO言語の型理論 ここで述べた方法は、基本的な仕組みのみ定式化し た 副作用をもたない部分に限定 代入文を定式化していないので、get_x などのメソッドの中身を項 として表現できなかった サブタイピングと継承の違い 型情報が失われることがある moving_color_point の例 継承した側で、メソッドの中身を書き換えることができる その場合、どのメソッドが適用されるべきかは型情報(静的な情報)だ けではわからない。-> 型を動的に決める必要がある 次回(以降) 次回(6月17日、6月24日) – やり残した事 – 講義のまとめ – 最終レポートの出題 6月10日は休講です。
© Copyright 2024 ExpyDoc