6.170 Laboratory in Software Engineering Lecture 4 - OpenCourseWare(OCW)を勉強するWiki

MIT OpenCourseWare ＞ 6.170 Laboratory in Software Engineering, Fall 2001 ＞ 6.170 Laboratory in Software Engineering Lecture 4

MIT OpenCourseWare 6.170 Laboratory in Software Engineering, Fall 2001, Lecture 4: Data Abstraction 1 のまとめ

ラジオの方では 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はまだ拾うことができます。)

4.1　Introduction

メソッドのspecificationの話。specificationなしにメソッドの実装の権限委譲はできない。specificationは契約として働く。

• プログラマ(implementor)　契約を守る責任がある
• クライアント(client) 　契約に即したメソッドを使う（specification＝事前条件）

バグはインターフェースの振る舞いの理解し間違いで起こる。プログラマはみんな、頭の中で自分のspecificationを持ってるんだけど、みんなが書き下すわけじゃないしね。

specificationは、クライアントにとってはコードを読む手間が省けて良い。プログラマにとっては、実装を変えるたびにクライアントにわざわざ言わなくていいのでコード作るのが早くなる。

この講義は前の2つの講義の依存のdecouplingに関係しているけど、依存があるのかどうかだけじゃなくて、どんな依存があるかみていこうね。

（※スペシフィケーションってインターフェースを想定してるのかと思ったけど ここの章を見る限り、契約を意識してるっぽい。契約ってあれね、メイヤーのアレ。なのでここからかなり契約な話になる。
ちなみに、このテキストでいうスペシフィケーションってメイヤーの契約に似てるんやけど、微妙に違う。ここが気になってて、つまり、このテキストを書くためにMIT側が独自に定義した考えなのか、あるいはメイヤーの契約の概念が発展して業界の一般的な解釈がこのテキストにあるような形になったのか？ ）

4.2 Behavioral Equivalence

次のコードはどう違う？

static int findA (int [] a, int val) {
for (int i = 0; i < a.length; i++) {
if (a[i] == val) return i;
}
return a.length;
}

static int findB (int [] a, int val) {
for (int i = a.length -1 ; i > 0; i--) {
if (a[i] == val) return i;
}
return -1;
}

もちろんコードが違うのはそうだけど、入れ替えが可能(substitute)かどうかって言うのを問題にする。これらは実際振舞いもちがう。

• valがなければfindAははlengthを返すけどfindBは-1を返す
• もしもvalと同じ値が２ヵ所に合ったら、Aは小さいindexを返して、Bは大きいほうを返す

でもこれ、valが１回だけarrayで現れたときならおんなじ振る舞いをするから、そういうときだけ入れ替えられる。specificationではこう書く。

requires: val occurs in a
effects: returns result such that a[result] = val

4.3 Specification Structure

スペシフィケーションって以下の3つの条件で書かれる。

• 事前条件　requires節で書かれる
• 事後条件　effects節で書かれる
• フレーム条件　modifies節で書かれる

事前条件はクライアントが守る条件。あるメソッドを呼ぶときにこの事前条件が満たされていないと呼べない。（開発者は事前条件が保証されているもんとして実装できるから楽になる）
事後条件は実装者が守る条件。この条件を満たすように実装する。（クライアントはこの条件にしたがった結果が返ることを期待できる）
フレーム条件ってのは事後条件とからむけど、何を変更するかを記述する。modifies x; って書いてたら、それはxが変更されまっせーっていうこと。
なんか「不変表明」の逆っぽいけど、読んでるとちょっと違う気がする。

で、この条件が省略されたときの解釈ですが、事前条件が省略されると、それはどんな場合でも事前条件が満たされると解釈してOK。（クライアントが気にせんといかん条件が無いってことね） こういういつでもOKてきなメソッドを、「total」という。ほいで、事前条件がfalseになることがあるメソッドを「partial」という。
フレーム条件を省略すると、何も変更しないってこと。
で、事後条件を省略すると、それは意味がなく、何もせんってことになる。

4.4 Declarative specifications

ぶっちゃけ、スペシフィケーションは2つに分けることができる。

• Operational specifications　→メソッドの呼び出し順とか
• Declarative specifications　→戻り値の型とか

で、Declarative specificationのほうが簡単なんで、こっちからいきましょ。

例えばStringBufferのreverse() っていうメソッドを考える。これはあれね、自分自身を逆さ言葉にするメソッドですな。
reverse()メソッドのDeclarative specificationsはこんな感じになる。

reverse()
modifies: this
effects:
　length (this.seq) = length (this.seq’)
　all k: 0..length(this.seq)-1 | this.seq’[k] = this.seq[length(this.seq)-k-1]

modifies: this ってなってるんは、StringBufferが自身を変えるってことですな（Stringは自分な変えないで新しく生成する）

で、efffectsで書かれてる事後条件を見ると、まず変換前と変換後で文字列長が同じっでことと、あるk番目の文字が変換するとlength-k-1番目にくる（つまり逆さ言葉になる）っていうのが事後条件になってますな。
事前条件はないので、配列長が0とかのときでも呼んでOK →トータルなメソッドってことですな。
あ、this.seq’って変換後の値ね。ダッシュがつくときとpostって付けるときはいつでも変換後って意味ね。

もひとつ例を。次はStringのstartsWith。あれね、引数の文字列で始まってるかどうかのチェックをするメソッド。

public boolean startsWith(String prefix)
／／ Tests if this string starts with the specified prefix.
／／ effects:
／／ if (prefix = null) throws NullPointerException
／／ else returns true iff exists a sequence s such that (prefix.seq ^ s = this.seq)

これは事後条件しかなく、prefixがnullなら、ヌルポを投げるってのと、prefixとある文字列sを連結させると、自分自身と等しくなるような文字列sが存在するときにtrueを返しなさいってのだけ。

で話題は変わって、Declarative specificatioってのは、non-determinism（非決定論？）って呼ばれるものをどう表現するかを見てみる。ま、non-determinismつうか、under-determinedness（未決定性？）っていうほうがいいけどね。

で、スペシフィケーションってあんま細かくきめんほうが実装は簡単やったりするやん？ てーことは、非決定項ってのは実装はスペシフィケーションを満たす可能な全ての振る舞いを公開するべきやと提案してる（？よく意味がつかめない。原文→「The term non-determinism suggests that the implementation should exhibit all possible behaviors that satisfy the specification, which is not the case.」）

実際の例としてはこんなの。

public void addObserver(Observer o)
／／ modifies: this
／／ effects: this.observers’ = this.observers + {o}

これは、引数のoを自分のもつobserversに追加してるってことね。（なので、modifies: this）

public void notifyObservers()
／／ modifies the objects in this.observers
／／ effects: calls o.notify on each observer o in this.observers

で、追加したオブザーバに通知を行ってるやつのスペシフィケーション。
ここで言いたいのは、この通知って自分が持ってるobserversの集合要素のobserver一つ一つに対して通知を変けるんやけどそのときの要素の順番とかは一切気にしていない。もし、順番によってなんかの影響が出たとしても、このスペシフィケーションはしったこっちゃない。
これが非決定の例。

4.5. Exceptions and Preconditions

いつ事前条件を使うか、使うとしたらどういう風にチェックするか。重要なことは、事前条件はチェックされることを要求しないってこと。チェックに結構コストがかかったりチェックが難しかったりするしね。

前に言ったとおり、non-trivial preconditionはメソッドをpartialにする。これはクライアントにとって、事前条件を守んなきゃいけなくてめんどくさい。だからJava APIクラスでは変な使い方をされるとexceptionを出す。もっとロバストに使えるようにね。

でも事前条件が有効に働くことだってある。二分木(binary tree)を考える。これが、値の順番をちゃんと保ってるかどうかいちいちチェックしなきゃいけないと思う？　そんなの大変だよね。だからこれらは保たれてる(invariant)と考える。これを一般化した不変表明(representation invariants)ってのを後の講義で説明するね。

事前条件を使うかどうかはエンジニアリングの判断。実行時にかかるチェックのコストとメソッドのスコープを考える。メソッドの使用がローカルだけだったら事前条件を使っても良いと思うけど、みんなが使うものに事前条件をつけるのはちょっとね。あと、チェックにすごくコストがかかるときにはしかたないかもね。（JavaのArraysの例）

でももし事前条件を使うことになったとしても、事前条件が違反されていないかどうかチェックする機能は入れられる。exceptionで話したとおり。開始時には無理でも計算時に発見できる。

もしもpreconditionが違反されてたら、unchecked exceptionを投げるべき。

4.6 Shorthands

public boolean startsWith(String prefix)
effects:
if (prefix = null) throws NullPointerException
else returns true iff exists a sequence s such that (prefix.seq ^ s = this.seq)

を

public boolean startsWith(String prefix)
throws: NullPointerException if (prefix = null)
returns: true iff exists a sequence s such that (prefix.seq ^ s = this.seq)

って省略して書いたりする。Java APIスタイルにのっとってる？

4.7 Specification Ordering

一方、あるメソッドを他のメソッドと入れ替えたいときにspecificationをどう比べればいいかってのを考える。

specification A がspecification Bより少なくとも強い、っていうと、

• Aの事前条件はBのより強い
• AがBの事後条件より弱くない（Bの事前条件を満たしてる上で）

逆に言うとpostconditionはいくらでも強くできるし、事前条件をいくらでも弱くできる。

4.8 Judging specifications

さてどうやっていいメソッドを作ったら良いか。まずsupecificationを書いてみること。絶対確実なルールはないけどガイドラインはある。

• specificationは首尾一貫(coherent)すべき　たくさんの違ったケースを持つべきじゃない。すごくネストしたif節なんかはトラブルのサインだ。
• メソッドを呼んだときの結果は有益(informative)なもの　たとえばJavaのHashmap、nullも値として入れることができるのに、コールしたときのキーに対する値がないときもnullだからちょっと困る。
• specificationは十分強く　わかんないexceptionは出さないように、でもクライアントが気ままに使えるように。
• specificationは十分弱く　URLを指定したらいつもWebページがとってこれるとは限らないように、できないことはできないといっておこう。

4.9 Summary

specificationはプログラマとクライアントの重要なファイアウォールになる。これは開発の分割を可能にする。クライアントはソースコードを見なくて良いし、開発者はコードの使われ方を気にしなくて良い。Declarative Specificationは実際では一番使いやすい。また、事前条件はクライアントにとって使いにくくするけど、正しく使えばソフトウェアのデザイナーにとって使えるから知っておこうね。

---

today's visitor： -
total visitor： -