Disciplined Software Engineering Lecture #9 Watts S. Humphrey Software Engineering Institute Carnegie Mellon University Pittsburgh, PA 15213 Sponsored by the U.S. Department of Defense ノートを書いたのは 6, 8, 60だけです。すべて用語集不備への不満です。 PSPの教えにもかかわらずレビューもテストもなしに，コース教材として提供することにします:-) (久保記）

設計記法ー概観 記法の重要性 ﾌﾞｰﾙ代数 ｶﾙﾉｰ図 有用な記号 ﾌﾞｰﾙ関数の利用 簡単化 形式的手法

記法の重要性 ｿﾌﾄｳｴｱ開発における多くの欠陥は誤解と混乱から生じている。 ﾌﾟﾛｸﾞﾗﾑの要求と設計を表現するために使用される記法は、 精密かつ簡潔、 使い易い 共通に理解される 広範囲のｿﾌﾄｳｴｱ機能の表現に適切 であるべきである。 形式的記法はこれらの判断基準を満たしている。

集合の性質ー数学的記法 英語 記号 例 Union, sum A or B, A+B 英語 記号 例 Union, sum A or B, A+B Intersection, product A and B, A*B, AB Complement, not ' A', not A All, universal 1 None, empty set 0

この記法の利用 短所 長所 重要な一つの記法に精通する プログラムの正当性証明ための形式的手法で使用される記法と無矛盾である。 論理を他の表現から区別する。 短所 一般に入力に時間がかかる 精通に練習を要する 同僚が理解できないかもしれない　　　　　　　　　　　

ブール代数 集合の代数 集合の表現 集合の関係を定義し取り扱う。 首尾一貫性＝文が自己無矛盾か 妥当性（ｖａｌｉｄｉｔｙ）＝文が現実を表現しているか 集合の表現 ベン図 基本的関係 全集合と空集合 the universal and empty sets basic relationships Venn diagrams Class representations validity - whether statements represent reality consistency - whether statements are self- consistent defines and manipulates class relationships The algebra of classes “Class”の訳が用語集にない。藤野さんの訳，「集合」のままです。 “Universal Set”の訳も用語集にはない。“Empty Set”も同じ。（久保記）

ベン図 人間 人間 女性 男性 非成人女性 非成人 男性 成人 男性 成人 女性 全集合 A’B’C’ A’BC’ AB’C’ AB’C

集合の性質 - 1 反射律: for every x, x<=x べき（等）律: xx=x, x+x=x 反対称律: if x<=y and y<=x then x=y 推移律: if x<=y and y<=z then x<=z 可換律: xy=yx, x+y=y+x 結合律: x(yz)=(xy)z, x+(y+z)=(x+y)+z 分配律: x(y+z)=xy+xz, x+yz=(x+y)(x+z) 「べき（等）律」は用語集からもってきました。カッコが気になるし，正解は知らないし，困ったけど，とりあえずは用語集のまま。「べき律」と「等律」の二つの日本語用語が一個の英語用語に対応するんですか。（久保記）

集合の性質 - 2 空集合と全集合: xx’=0, x+x’=1, 0<=x<=1 x0=0, x+1=1, x+0=x, x1=x 一貫性: x<=y, xy=x, x+y=y は同値である 吸収律: x(x+y)=x+xy=x ドモルガンの定理: (x’)’=x, (xy)’=x’+y’, (x+y)’=x’y’

例 次のような条件の下でＯＮにしたいスイッチをもっているとする。 ●Ａ または Ｂ または Ｃ がＯＮ ●Ａ かつ Ｂ が ＯＮでないとき ●Ａ かつ Ｃ が ＯＮでないとき このスイッチを次のように表現する、 　　ＯＮ＝（Ａ＋Ｂ＋Ｃ）*［（Ａ*Ｂ）＋（Ａ*Ｃ）］’

ブール式の簡単化 ブール式を簡単化するとき次のようなガイドラインを考えること。 もしプライム’のついた括弧つきの任意の式があるならば、それらを取り除くためドモルガンの定理を使いなさい。 分配法則で因数分解される共通項を探せ。 複雑さを減少させるため代入をする。 積の和の形の式へもっていくよう試みる。

簡単化の例 - 1 電球の例をつかう On = (A+B+C)*[(A*B)+(A*C)]’ ドモルガンの定理を適用する On = (A+B+C)*[A’+(B’*C’)] B+Cを x で, B’*C’を x’ でそれぞれ置き換える On = (A+x)*(A’+x’)

簡単化の例 - 2 式は完全に簡単化された。しかし集合の積の和の形に変換した方がいい。 On = (A+x)*(A’+x’) On = [(A+x)*A’]+[(A+x)*x’] On = [(A*A’)+(x*A’)]+[(A*x’)+(x*x’)] On = (x*A’)+(A*x’) ここで x を B+C で置き換える On = [(B+C)*A’]+[A*(B’*C’)] On = (A*B’*C’)+[A’*(B+C)]

簡単化の練習問題 つぎの式を簡単化せよ 1. F = X+(X’*Y) 2. F = (X+Y)+[(X*Z)+Y] 3. F = (X’*Y’*Z’)+(X*Y*Z’)+(X*Y’*Z’) 4. F = [X’*(Y+Z’)]’*(X+Y’+Z)*(X’*Y’*Z’)’

問題 1 の答え この式から始める F = X+(X’*Y) 分配律を使うと F = (X+X’)*(X+Y) ここで、全集合の性質によって X+X’ = 1 および 1*(X+Y) = X+Y ゆえに、答えは F = X+Y

問題 2 の答え F = (X+Y)+[(X*Z)+Y] この式から始める。 分配律を適用すると F = (X+Y)+(X+Y)*(Z+Y) F = (X+Y)*[1+(Z+Y)] 全集合の性質によって, 　1+Z+Y=1 ゆえに、答えは F = X+Y

問題 3 の答え F = (X’*Y’*Z’)+(X*Y*Z’)+(X*Y’*Z’) から始める。 F = Z’*(X’Y’+XY+XY’) 共通のX 項を因数としてくくり出すと次式になる。 F = Z’*[X’Y’+X(Y+Y’)] = Z’*(X’Y’+X) さて, 分配律によって F = Z’*(X’+X)*(Y’+X) = Z’*(Y’+X)

問題 4 の答え F = [X’*(Y+Z’)]’*(X+Y’+Z)*(X’*Y’*Z’)’ から始める。 先ず ドモルガンの定理を適用すると, 次式になる。 F = (X+Y’Z)*(X+Y’+Z)*(X+Y+Z) 共通の X 項を因数としてくくり出すと次式になる。 F = X+Y’Z*(Y’+Z)*(Y+Z) 共通の Z 項をくくり出すと F = X+Y’Z*(Z+Y’Y) = X+Y’Z

カルノー図 - 1 6 変数以下の式はカルノー図が簡単化ﾌﾟﾛｾｽに役立つ。 カルノー図は、一つの式に変数の全ての可能な組み合わせを表現するための構造的な方法である。 そこでの括り出しは、関係のある項を結びつけ、それにより簡単化する方法をとる。

カルノー図 - 2 ブール式は最小項の形式で表現できる。 最小項は変数のすべて可能な組み合わせの積である。 X と Y の最小項はつぎである: X’*Y’, X*Y’, X’*Y, XY ｎ 個の変数の最小項は 2**n 個ある。

カルノー図 - 3 XY’ X’Z YZ YZ X 00 01 11 10 X 00 01 11 10 X X 1 1 X X 00 01 11 10 X 00 01 11 10 X X 1 1 X X XY’+X’Z YZ X 00 01 11 10 X X 1 X X

4 変数カルノー図 YZ WX 00 01 11 10 00 X 01 X X X 11 X X 10

5 変数カルノー図 XYZ VW 000 001 011 010 110 111 101 100 00 01 11 10

図の上の括り出し - 1 ２つの隣り合ったセルが共に１をもつとき、それらのセルは括り出すことができ、そのとき２つのセルに対して異なる値をとる変数は消去する。 例えば、 0100 と 0101 のセルは括り出すことができ、変数 Z は消去する。 このことは次のような図の上で見ることが出来る。

図の上の括り出し - 2 YZ WX 00 01 11 10 00 X 01 X X X 11 X X 10

図の上の括り出し - 3 同様に, ４つの隣り合ったセルが１をもつとき, その時これらのセルは括り出すことができ、その４つのセルに対して異なる値をとる２つの変数は消去できる。 例えば, 0101, 0111, 1101, および 1111 のセルは括り出せて、 変数 w と y　は消去される。 このことは次の図の上で示される。

図の上の括り出し - 4 YZ WX 00 01 11 10 00 X 01 X X X 11 X X 10

図の上の括り出し - 5 以上可能な括り出し３つをすべて行わうと、結果の式は次のようになる。 F = w’yz + wxy’ + xz こことは次の図の上で見ることが出来る。

図の上の括り出し - 6 YZ WX 00 01 11 10 00 X 01 X X X 11 X X 10 W’YZ+W’XY’+XZ

簡単化の練習問題 カルノー図を使用して、次の４つの式を簡単にせよ。 1. F = X+(X’*Y) 2. F = (X+Y)+[(X*Z)+Y] 3. F = (X’*Y’*Z’)+(X*Y*Z’)+(X*Y’*Z’) 4. F = [X’*(Y+Z’)]’*(X+Y’+Z)*(X’*Y’*Z’)’

問題 1 の答え 関数は F = X+(X’*Y)である。 括り出しを行うと結果は F = X+Y YZ X 00 01 11 10 1 1 00 01 11 10 1 1 1 1 1 1 1 YZ 括り出しを行うと結果は F = X+Y X 00 01 11 10 1 1 1 1 1 1 1

問題 2 の答え 関数は F = (X+Y)+[(X*Z)+Y] = X+Y+XZ+Y = X+Y+XZ 括り出しを行うと結果は YZ X 00 01 11 10 1 1 1 1 1 1 1 YZ 括り出しを行うと結果は F = X+Y X 00 01 11 10 1 1 1 1 1 1 1

問題 3 の答え 関数は 括り出しを行うと結果は F = Y’Z’+XZ’ = Z’(Y’+X) F = (X’*Y’*Z’)+(X*Y*Z’)+(X*Y’*Z’) = X’Y’Z’+XYZ’+XY’Z’ YZ X 00 01 11 10 1 1 1 1 YZ 括り出しを行うと結果は F = Y’Z’+XZ’ = Z’(Y’+X) X 00 01 11 10 1 1 1 1

問題 4 の答え - 1 関数は次式である： この式は３つの図でカバーされる。 F = [X’*(Y+Z’)]’*(X+Y’+Z)*(X’*Y’*Z’)’ = (X+Y’Z)*(X+Y’+Z)*(X+Y+Z) この式は３つの図でカバーされる。 X+Y’Z YZ X 00 01 11 10 1 1 1 1 1 1 X+Y’+Z X+Y+Z YZ YZ X 00 01 11 10 X 00 01 11 10 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1

問題 4 の答え - 2 全体の関数はこれらの３つの図 の積である。つまり ３つの図の すべてが１をもつところは 1 で， 他の所は０の図である。図は右 のようになる。 YZ X 00 01 11 10 1 1 1 1 1 1 この図で括り出しを行って答えは F = X+Y’Z YZ X 00 01 11 10 1 1 1 1 1 1

ゼロの括り出し １を括り出すときには、カルノー図上の１を全部塗りつぶす。このことにより、式の最小項形式をえる。 同じカルノー図の０を全部塗りつぶすことにより括り出しを行うことも可能である。このときには、それに続いてドモルガンの定理を適用する。 このときには、その式の最大項形式、つまり集合和の積の形式が得られる。

ゼロの括り出しの例 右の図の１を全部塗りつぶすことで、 括り出しを行うと次式が得られる。 F = X+Y+Z YZ X 00 01 11 10 1 1 1 1 1 1 1 1 一方、 0を全部塗りつぶすことにすると 次式が得られる。 F’ = X’Y’Z’ これにドモルガンの定理を適用すると 最大項形式の答えが選られる。 F = X+Y+Z YZ X 00 01 11 10 1 1 1 1 1 1 1 1

もう一つの括り出しの例 右の図の１を全部塗りつぶすして括り出しを すると、最小項形式の結果が得られる。 F = XY’+X’Y+Z YZ X 00 01 11 10 1 1 1 1 しかし、 0を全部塗りつぶすことにすると、 次が得られる F’ = X’Y’Z’+XYZ’ ドモルガンの定理を適用すると最大項 形式の答えが得られる。 F = (X+Y+Z)*(X’+Y’+Z) = (X+Y)*(X’+Y’)+Z 1 1 1 YZ X 00 01 11 10 1 1 1 1 1 1 1

ゼロの括り出し 1 の括り出しがときどき、１つか２つまずい位置におかれた0によって複雑になることがある。これは次のように処理することが出来る。 あたかも都合の悪い0が１であるとみてその図の括り出しを行う。 そののち括り出した因子をそれぞれ小さな図とみて0を括りだす。

ゼロの括り出しの例 - 1 ２つの都合の悪い0を別にすれば この図の括り出しは非常に単純で ある。 F = Y’+W’Y = Y’+W’ YZ WX 00 01 11 10 00 1 1 1 01 1 1 1 しかし、W’X’Y’Z’ と W’XYZに0が ある から，これを括り出さねばなら ない。 11 1 1 10 1 1

ゼロの括り出しの例 - 2 第1の因子、 Y’は変数W,X,と Zからなる小さな図ﾟを創る。 この図上で、W’X’Z’ が括り 出される: F1 = Y’*(W’X’Z’)’ = Y’*(W+X+Z) ここの本質は Y’  not W’X’Z’ の括り出しである。. YZ WX 00 01 11 10 00 1 1 1 01 1 1 1 11 1 1 第2の因子の括り出しは F2 = W’Y*(XZ)’ = W’Y*(X’+Z’) よってこの関数は次になる。 F = Y’*(W+X+Z)+W’Y*(X‘+Z’) 10 1 1

多変数の括り出し カルノー図は6変数まで可能である。 それを超えると、特別なコツが必要になる。 もし式のほとんどの項が6以下の変数からなり、その他の変数が２，３個の場合に限り、 0の括り出しに近い方法が使える。 この方法は例外括り出しと呼ばれ、変数の数がいくらあっても使える。

例外括り出し - 1 次の関数の括り出しを4変数のカルノー図の上で行う。 F = AX’Y’+WXY’+W’Y’Z+XY’Z+W’XY’Z’+WX’Y’ 1. 変数 W, X, Y, および Z を使って関数を構成する. 2. A をもつ項については、 1の代わりに、その桝目に A を入れる。 3. ゼロを括り出す際、 A を A+0 として扱う。

例外括り出し - 2 初めに、 W, X, Y, と Z を含む項のみを 使って図をつくる。 次は, Aを含む項である。 0がある には0を入れる。 F1 = WXY’+W’Y’Z+XY’Z+W’XY’Z’+WX’Y’ F2 = AX’Y’ YZ YZ WX 00 01 11 10 WX 00 01 11 10 00 1 00 A A 01 1 1 01 11 1 1 11 10 1 1 10 A A

例外括り出し - 3 初めに、A が１であると仮定して １を括り出す。 F1 = Y’ 次に、Aの項を括り出す。そのとき A をA+0として取り扱う。 F = Y’*[A+(W’X’Z’)’] = Y’*(A+W+X+Z) YZ WX 00 01 11 10 00 A 1 01 1 1 11 1 1 10 1 1

他の有用な記号 次のような基本的な数学記号もまたプログラム機能を定義する際に有用である。 - “集合の1つの要素である”ことを意味する - “集合の1つの要素である”ことを意味する - “その集合の要素ではない”ことを意味する - “その集合の全要素に対して”を意味する - “その集合の要素が存在する”を意味する

記法の例 データセット D がファイルに含まれるならファイルを更新する (D File) :: Update i when (i even) :: add x(i) 任意の数 i が負であるときレジスターをクリアーする i when (i < 0) :: Clear

関数の完全性 もし関数の集合が全ての可能な条件をカバーしているときその集合は完全であると言う。 完全な関数集合に対しては、関数の和に対応するカルノー図が図上の位置すべてをカバーする。 図上の位置が多重にカバーされることはありうる。

関数の直交性 関数集合に属するどの二つの関数も同じ条件をカバーすることがなければ、その集合は直交していると言う。 これは任意の関数と任意の他の関数の積が0であることを意味する。 i, j where (i j) => F(i)*F(j) = 0 図は完全にはカバーされていないかもしれない。

完全かつ直交 1つの関数集合はつぎの条件を満たすとき，完全であり、かつ直交している。 関数全体ですべての要素をカバーする。 どの2つの関数も同じ要素をカバーしない。

完全かつ直交している関数 f, g, h は完全である f, g, h は直交している 00 01 11 10 00 01 11 10 f 00 01 11 10 00 01 11 10 f g gh fh f g 1 g f fh fg 1 h g f f, g, h は完全かつ直交である。 00 01 11 10 f f g h 1 h g h f

形式的方法 - 1 ソフトウェア設計の形式的方法は数学の概念をベースに開発されてきた。 形式的方法の前提は次である。 コンピュータプログラムは数学の文として扱うことができる。 したがって、数学の原理が適用できる。 正しいプログラムの設計は、したがって、定理の導出として取り扱うことが出来る。 数学的に厳密な方法はかくして正しいプログラムをつくりだすはずである。

形式的方法 - 2 形式的方法は典型的には，プログラムの前置条件、後置条件、およびプログラム不変条件を使う。 そこでのプログラムは、不変条件を保存しながら、前置条件を後置条件に変換する。 プログラムの正しさは、次のように証明する。 プログラムは、前置条件を後置条件に変換する。 プログラムは、不変条件を保存する。

形式的方法 - 3 新しいプログラムを形式的方法で開発するとしたら、 後置条件から出発する 。 前置条件を導出する。 不変条件を決定する。 前置条件を後置条件に変換しその不変条件を保存するプログラムを定義する。 もしそのプログラムが繰り返しを含むならば、各サイクルはループ終了に向かって進行すべきである。

形式記法への賛成論 形式記法は精密である。 形式記法は複雑な機能を簡潔に表現できる。 形式記法は形式的方法を学習するときの基礎をなす。

形式記法への反論 形式記法は学習に時間がかかる。 形式記法について、それを設計に使用するのに必要なレベルで精通するには、さらに多くの時間がかかる。 あなたの仲間たちは形式記法を理解できないかもしれない。

このコースの形式的記法 支持者達は形式的方法は品質のよいｿﾌﾄｳｴｱを開発するための厳密な方法を与えると主張する。懐疑派は費用効果的でないと反論する。 形式的方法は、設計の正当性を示しているが、それが一般にされるにはつぎが要求される。 ユーザﾞの訓練 形式的に証明する方が、ソフトウェアの設計の中で行うよりもエラーが少ないユーザ 形式的手法はこのコースではこれ以上は扱わない。

形式的方法関連の示唆 - 1 もしあなたが形式的方法に精通している、あるいは訓練を受けていれば、 形式的方法をＰＳＰで使いなさい。 あなたのあなたの品質と生産性を測定しなさい。 あなたの結果を同様の方法を使用する他の人の結果と比較しなさい。 あなたの結果をあなたが形式的方法によらない場合の結果と比較しなさい。 この方法があなたにとって効果があるかどうかを判断しなさい。 あなたが何か発見したら、それを他の人に話しなさい。

形式的方法関連の示唆 - 2 もしあなたが形式的方法に精通してなければ、以下を検討しなさい。 ユーザに彼らのデータを見せてもらう。 コースをとるか、参考書で勉強する。 自分自身で試してみる。 あなたの品質と生産性を前後で計測し、形式的方法があなたにとって効果があるかどうか判断する。 あなたが何か発見したら、それを他の人に話しなさい。

演習課題 #9 テキストの付録Ｂ (p.353-373)を読んで、例題を実施しなさい。 PSP2.1を使用して、Ｎ個の実数のリンクリスト(linked list)を昇順にｿｰﾄするプログラム8Aを書きなさい。 PSP2.1の説明は付録Ｃ(p.394-397)を、プログラム8Aの仕様は付録Ｄ(p.492-493)を参考にしなさい。 “linked list”の訳が用語集にない。（久保記）

講義９のまとめ - 1 1. 貧弱な設計記法はエラーの原因である。 2. 定義された厳密な記法を使用することによって、 1. 貧弱な設計記法はエラーの原因である。 2. 定義された厳密な記法を使用することによって、 あなたはあなたの設計の品質を改善できるし、欠 陥をなくすことができる。

講義９のまとめ - 2 3. 利用可能なものの中から適切な記法を選択し、 使用しなさい。 3. 利用可能なものの中から適切な記法を選択し、 　　使用しなさい。 4. あなたのソフトウェア開発に形式的方法を試みなさ　　い。そしてそれがあなたの役に立つか調べなさい。