OpenCourseWare(OCW)を勉強するWiki
6.170 Laboratory in Software Engineering Lecture 6
最終更新：
匿名ユーザー
-
view
MIT OpenCourseWare ＞ 6.170 Laboratory in Software Engineering, Fall 2001 ＞ 6.170 Laboratory in Software Engineering Lecture 6
MIT OpenCourseWare 6.170 Laboratory in Software Engineering, Fall 2001, Lecture 6: Representation Invariants and Abstraction Functions のまとめ
ラジオの方では vol. にあたりました。Lecture Noteを読むときの助けにしてください。
6.170 Laboratory in Software Engineering, Fall 2001のLecture NoteのPDFはこちら
(※2006年4月16日現在、上記講義は6.170 Laboratory in Software Engineering, Fall 2005にアップデートされたようですが、PDFはまだ拾うことができます。)
6.170 Laboratory in Software Engineering, Fall 2001のLecture NoteのPDFはこちら
(※2006年4月16日現在、上記講義は6.170 Laboratory in Software Engineering, Fall 2005にアップデートされたようですが、PDFはまだ拾うことができます。)
6.1 Introduction
ここでは抽象型を理解するための2つのことを扱う
- 不変表明？(representation invariant) 型のインスタンスがちゃんと形式的(well-formed)か。テストをより役立てる。
- 抽象関数？(abstraction function) 不変表明の実装。これを理解せずに抽象型をいじるのはむずかしい。
6.2 What is a Rep(Representation) Invariant?
不変表明ってのは、抽象型のインスタンスがwell-formedであるかどうかっていう制約。数学的に言えば、抽象型のオブジェクトを取ってそれがwell-formedかどうかでtrueかfalseを返すもの。
RI : Object -> Boolean
前の章から使ってるListの例を使うと、List型はEntry型のheaderを持ってる。Entry型は前のオブジェクトをさすprev:Entryと、次のオブジェクトをさすnext:Entryを持ってて、あと要素をあらわすObject型のelementを持ってる。
（59ページの図参照。筆者はこれをオブジェクトモデル(Object Model)と呼んでいる。）
（59ページの図参照。筆者はこれをオブジェクトモデル(Object Model)と呼んでいる。）
オブジェクトモデルはデータ型のrepresentationを示してる。これは色んなレベルの抽象的なものを表してるから、userからはEntry型を意識しないから、これがない絵を描くかもしれないね。(60ページの図)
ちなみにここでオブジェクトモデルって言ってる図の表現規則は、
- It shows, for example, that the header field holds a reference to an object of class Entry. This property is important but not very interesting, since the field is declared to have that type; this kind of property is more interesting for the contents of polymorphic containers such as vectors, whose element type cannot be expressed in the source code.(すいませんよくわかんなかった)
- ! マークは、必ず1つ参照してることを示す (e.g. List.header)
- ? マークは、ゼロか1つを指してることを示す (e.g. Entry.next)
オブジェクトモデルで表現できない不変表明だってある。
- e1.next = e2ならe2.prev=e1であることとか
- リストの一番最初のダミーエントリーがnullのelementを持ってるとか
あと、リストの大きさを表すsizeが、Entryの数-1であることとかね。
不変表明を考えるときは、どんな制約が存在して、どんな制約がないかを考えるのが大切。
さて、じゃあ今までの話をまとめると、
for every instance of the class LinkedList
the header field is non-null
the header field has a null element field
there are (size + 1) entries
the entries form a cycle starting and ending with the header entry
for any entry, taking prev and then next returns you to the entry
もうちょっと形式的にまとめると、
all p: LinkedList |
p.header != null
&& p.header.element = null
&& p.size + 1 = | p.header.*next |
&& p.header = p.header.next p.size + 1
&& all e in p.header.*next | e.prev.next = e
today's visitor： -
total visitor： -
total visitor： -
