MyEnigma

とある自律移動システムエンジニアのブログです。#Robotics #Programing #C++ #Python #MATLAB #Vim #Mathematics #Book #Movie #Traveling #Mac #iPhone

15. コードの論理的検証 Yechiel Kimchi:『プログラマが知るべき97のこと』

# 目次

# はじめに

『プログラマが知るべき97のこと』

の中から1つのエッセイを選び,

そのエッセイを,クリエイティブコモンズ3.0の条件の元で転載したものです.

Creative Commons ― 表示 3.0 アメリカ合衆国 ― CC BY 3.0

本書の内容は,オープンソースモデルに従い,

ほぼ無制限で利用が可能です.

クリエイティブ・コモンズ表示3.0の条件下で,

自由に使用することができるのです.

つまり,どのエッセイも,

著者の名前を明記すれば,自由に転載,改変が可能であるということです.

ーー"はじめに"から抜粋 pXII


もし,他のエッセイを読みたい場合には,

記事末のリンクを辿るか,

以下のリンク先のTwitterアカウントのつぶやきからお探し下さい.

Twitter Account: 97 Things Bot



また,元の英文によるエッセイを読みたい方は,

こちらを参照して下さい.

Contributions Appearing in the Book - Programmer 97-things


15. コードの論理的検証 イェッチェル・キムチ (Yechiel Kimchi):『プログラマが知るべき97のこと』

ソフトウェアに誤りがないことを論理的に検証するための

「形式的証明 (formal proof)」

という手法があります.

しかし,形式的証明を手作業でやろうとすると,

コードそのものを書くことよりも,

手間がかかってしまい,

しかもその際にミスが起こる恐れがあります.

自動ツールが使えればその方が望ましいのですが,

いつもそれが可能とは限りません.

ここは間をとって,

半形式的証明とでも呼べる方法についてお話しましょう.



まずすべきことは,

対象となるコードをすべて短いセクション

(一行,ファンクションコール1つだけのブロックから,

 10行くらいのブロックまで)

に分割することです.

そうして短く切った上で,

各セッションが正しいかどうかをチーム内で話しあうのです.

その場合,どのセクションについても,

メンバーの中で最も懐疑的な態度の人が

正しいと納得すれば,一応「正しい」とみなしていいでしょう.



コードをセクションに分ける際には,

まずセクションの終端までの間で,

プログラムのステート

(プログラムカウンタや,

 すべての「生きたオブジェクト」を持つ値)

が,簡単に説明できるようになっていることが重要です.

また,セクションの中での機能(状態変化)は

1つのタスクに絞りこまれていて,

これも簡単に説明できることが大切です.

このガイドラインを守ると,

検証が容易になり,

関数の事前条件や事後条件

ループやクラス(のインスタンス)の不変条件(invariant)といった

概念の意味を統一することにもつながります.

個々のセッションをできるだけ他から独立させるよう努力することも重要です.

これも,もちろん検証を容易にすることに役立つわけですが,

セクションに変更を加える際に,

他への影響を考えずに済むという意味でsも,

絶対に必要なことだと言えます.



よく知られていて,

一般的に良いとされている

(しかし実際にはあまり実践されていない)

コーディングプラクティスの多くは,

コードの論理的検証を容易にする上でもやはり役立ちます.

これは逆に言えば,

論理的検証を楽にしようと努力するだけで,

コードのスタイルや構造の改善につながるようになるのです.

実践すべきコーディングプラクティスの例を次にあげておきます.

当然のことながら,こうしたプラクティスが守られているか否かは,

多くの場合,静的コード解析によって自動的にチェックできます.


goto分の使用は避ける.

 使用すると,離れた所にあるセッション同士に強い依存関係が生じてしまう.


変更可能なグローバル変数は作らない.

 変更可能なグローバル変数があると,

 それを使用するすべてのセクションが相互依存関係になってしまう.


変数のスコープは可能な限り小さくする.

 例えば,ローカルオブジェクトは,最初に使用する部分の直前で宣言する.


オブジェクトは可能な限り,不変(immutable)オブジェクトにする.

縦,横にうまくスペースを入れて,できるだけコードを読みやすくする.

 例えば,関連し合う部分には同じようにインデントを入れる,

 セッションの分かれ目には空白行を入れるなど.


オブジェクトや型,関数などにはその特性や機能がすぐにわかる(しかも比較的短い)名前をつける.

 それによりコードが自己ドキュメント化され,

 おおよその意味が,一見するだけで解るようになる.


セクションを入れ子にする必要が出たときには,それを関数にする.

関数は出来る限り短くし,機能は1つに絞り込む.

 古くから言われる「24行制限」は今も有効である.

 ディスプレイのサイズや解像度は変わっているが,

 人間の認知能力は1960年代から全く変化していない.


関数のパラメータはできるだけ減らす(最高でも4つまでにする)


これは必ずしも,関数で扱うデータを減らすということを意味しない.

関連するパラメータを1つのオブジェクトにまとめることで,

オブジェクトの不変条件を一箇所に集中させることができる.

それにより,凝縮性,整合性の検証が容易になる.


ブロックからライブラリに至るまで, コードのどの単位においても,インタフェースは出来る限り狭くすべし.


外部とのコミュニケーションが減れば,

その分だけ検証すべき事柄も減ることになる.

オブジェクト内部の状態を戻す「getter」があると,

その分検証の負担は増える.

処理対象となる情報を提供するようオブジェクトに要求する,

というのは望ましくない.

オブジェクトには,そのオブジェクトがすでに持ってる情報の処理をさせるべきである.

言い換えると,カプセル化とは結局の所,

インタフェースを狭くするということである.


クラスの不変条件を保つという観点から「setter」の使用は推奨できない.


setterがあると,オブジェクトの状態が変化することになり,

不変条件が満たされなくなってしまう.



コードの正しさを論理的に検証すると同時に,

コードの内容についても検証し,

チーム内で話しあえば,

より理解を深めるのに役立ちます.

自分が理解したことを,互いに伝え合えば,

全員にとって利益になるでしょう.


■著者データ

[イェッチェル・キムチ (Yechiel Kimchi)]

数学者(エルサレムのヘブライ大学で抽象集合論の博士号を取得)

計算機科学者(イスラエルのテクニオンのコンピュータ科学学部で10年以上教鞭を執っている)

そしてソフトウェア開発者(15年以上にわたり,大規模なハイテク企業での開発の仕事と,

自ら経営するベンチャ企業でのコンサルタントの仕事を掛け持ちしている)である.

はじめはCで仕事をしていたが,後にC++を使うようになった.

オブジェクト指向に強い関心を黐,

正しく,保守しやすく,効率的なソフトウェアがどうすればできるのかを常に追求している.

実践的なNP困難問題*1を効率的に解決するための

ヒューリスティック手法*2考案するという素晴らしい業績を残しているが,

彼本人は,

何千人というイスラエル人ソフトウェアエンジニアを教育し,

彼らに一定の影響を与えることができたことが

最大の業績だと考えている.


関連記事

1.分別のある行動 Seb Rose:『プログラマが知るべき97のこと』 - MY ENIGMA

2.関数プログラミングを学ぶことの重要性 Edward Garson:『プログラマが知るべき97のこと』 - MY ENIGMA

3.ユーザが何をするかを観察する (あなたはユーザではない) Giles Colborne:『プログラマが知るべき97のこと』 - MY ENIGMA

4.コーディング規約を自動化する Filip van Laenen:『プログラマが知るべき97のこと』 - MY ENIGMA

5.美はシンプルさに宿る Jorn Olmheim:『プログラマが知るべき97のこと』 - MY ENIGMA

6.リファクタリングの際に注意すべきこと Rajith Attapattu:『プログラマが知るべき97のこと』 - MY ENIGMA

7.共有は慎重に Udi Dahan:『プログラマが知るべき97のこと』 - MY ENIGMA

8. ボーイスカウト・ルール Robert C. Martin:『プログラマが知るべき97のこと』 - MY ENIGMA

9. 他人よりまず自分を疑う Allan Kelly:『プログラマが知るべき97のこと』 - MY ENIGMA

10. ツールの選択は慎重に Giovanni Asproni:『プログラマが知るべき97のこと』 - MY ENIGMA

11. ドメインの言葉を使ったコード Dan North:『プログラマが知るべき97のこと』 - MY ENIGMA

12. コードは設計である Ryan Brush:『プログラマが知るべき97のこと』 - MY ENIGMA

13. コードレイアウトの重要性 Steve Freeman:『プログラマが知るべき97のこと』 - MY ENIGMA

14. コードレビュー Mattias Karlsson:『プログラマが知るべき97のこと』 - MY ENIGMA

MyEnigma Supporters

もしこの記事が参考になり、

ブログをサポートしたいと思われた方は、

こちらからよろしくお願いします。

https://gumroad.com/l/myenigmasupportersgumroad.com

*1:NPとは、計算複雑性理論における問題の複雑性クラスで、Non-deterministic Polynomial time(非決定性多項式時間)の略である。NP - Wikipedia

*2:ヒューリスティック手法とは、人の脳の学習や生物の進化のプロセスを模倣し,「試行錯誤」を実現して解をもとめる手法.めるまが「複雑系とビジネス」 No.16 〜ヒューリスティック〜