プログラマーは定理証明支援系を勉強すべきか？

定理証明支援って何？

最近、定理証明支援に関連するニュースがいくつか飛び込んできました。あるときはOpenSSLのバグを見つけ、あるときは数学の問題を解決しています。
それらに共通する定理証明支援とは何かを簡単に説明します。

定理証明支援の「定理」「証明」とは、いわゆる数学的なそれを指します。
通常の証明は、人が書き、人が読み、人が正しさを判定します。
定理証明支援系では、人が証明をプログラムとして書き、コンピューターが読み、コンピュータが正しさを判定します。
どうやってコンピュータが正しさを確認するのか？を説明するには余白が足りないので割愛しますが、学校で習ったあの数学の証明を、コンピュータが正しいかどうか判定することが可能なのです。
そしてさらに、その証明を書く作業を様々なアプローチで助けてくれます。

何に役に立つの？

定理証明はプログラムの品質保証に役立ちます。
プログラムの仕様を定理として記述し、その正確さを確認し、正確さが保証されたプログラムを出力することができるのです。
例えばリストを変換する関数を作り、その関数が満たすべき性質を定理として記述します。
ここでは変換後のリストの長さが必ず10以下になる、という定理だったとすると、もしその定理が証明できれば、その関数はその性質を保証されます。
そしてその性質を持った関数をプログラムで使用することができるのです。

今すぐ全てのIT企業に導入すべき？

全てのIT企業が導入し活用するのは現実的ではないでしょう。

理由の一つは難易度です。
定理証明はやはり難しく、プログラミングとはまた別のスキルセットが必要になります。

証明の能力は、自分で証明を書く能力と、証明を読む能力に分ける事ができます。
両者には難易度に大きな差があり、前者は圧倒的に難しいです。

また定理を自分で作る、という行為も難題です。
そのため普段プログラムのテストを書くように、コンスタントに証明を書くというのは想像ができません。

そしてわざわざ定理を書かなくても、簡単なテストで十分な品質を得る事ができるケースも多くあります。

勉強すべき？

すべきだと思います。
自分自身がゴリゴリ証明を書いて活用する事はなくても、誰かが証明したプログラムを使うのが当たり前になるのはそう遠い未来ではなさそうです。
そのときに、何が証明されているのか？何が保証されているのか？を正しく理解する事は非常に重要です。
それらを理解するためには、定理証明で何ができるかを理解している必要があります。
既に証明付きコンパイラも登場しています。

勉強したら数学力は上がるの？

あがりません。
数学力をあげたければ、数学を勉強しましょう。

JarファイルからManifestを読む

意外と手こずったのでメモ。
特定のJarのManifestを読む方法です。
単にMETA-INF/MANIFEST.MF をリソースとして読もうとするだけだと、classpathが通っている他のJarからも探してしまいうまく行きませんでした。
以下は呼び出しているクラスを保持しているJarのManifestファイルを読み込んでいます。

Java1.7で確認済み。

Gradle初心者がはまったこと、悩んだ事。

ここ2週間程、プロジェクトのビルド環境を再整理していてGradleをがっつり触りました。
GradleもGroovyも初めてだったのですが、最初は慣れなくて苦労しました。
その代わりGradle脳になってしまえば非常に簡潔に分かりやすく書けて良いですね。素敵です。

以下の内容はGradel 1.8を前提としています。

タスクに複数の依存関係を設定する

タスクのリストをそのままdependsOnに渡す事ができます。

task copyHoge(type: Copy, dependsOn: ['jar', 'copyBat']) {
    from 'nanikashira'
    into 'dokokashira'
}

タスクに変数を渡す

できません。
その代わりgradleコマンドの引数、タスクルール、動的タスク作成などで代用できます。
私の場合は一部の値が違うタスクを何個か作りたかっただけだったので、動的タスク作成を使いました。

['file1', 'file2'].each { def fileName ->
    task "copyFile$fileName" (type: Copy) {
        from 'nanikashira/$fileName'
        into 'dokokashira'
    }
}

task copyFile(dependsOn: tasks.matching { Task task -> task.name.startsWith("copyFile")})

タスクの中で他のタスクを呼ぶ

できません。
依存関係でタスクをチェインさせる形か、メソッドを書く形などに変形して代用しました。

testで１件でも失敗があるとビルド失敗になってしまう

ignoreFailuresをtrueに変更すると、ビルドが継続するようになります。

test {
    ignoreFailures = true
}

sonarプラグインが動かない!

後継のsonarRunnerプラグインだとちゃんと動きました。

Gradle IDEが動かない!

Eclipseでlombokと併用すると動かないバグがあるようです。
なんかlombokとIDEという組み合わせは何かと苦しめられますね・・・。
Eclipse Grade plugin hangs when importing Gradle projects

その他に大事な事

• ビルドフェーズをちゃんと理解する

これが頭に入ってないとタスクの動作イメージがわかないですね。この章がまさにGradle脳になるための方策を説明している気がします。

• とにかくユーザーマニュアル、リファレンス！

DSLで簡潔な表現ができる反面、リファレンスを読まないと何ができるか分からない、という場面が非常に多かったです。
最終的にはユーザーマニュアルの章番号を覚えてしまいました。

ちょっと愚痴っぽいのも混ざってますが、良いですよGradle。

オブジェクト指向のこころ

@sakamoto_desu この本おすすめですよ http://t.co/TOdRBCZF4A

— ふ''れいす (@bleis) 2013, 5月 22

あれから５ヶ月。やっと読み終わりました。
いやー、ちょっと間に色々やっていたもんで。

結論から言うと、オブジェクト指向に対するもやもやがかなりすっきりしました。
本当に良い本でした。
自分が感じていた違和感をすべて拭ってくれて、頭の中が整理整頓され、プログラミング中の迷いも激減しました。

• オブジェクトは現実世界のコピーではなく責務で分ける
• 継承より委譲
• カプセル化とは流動的要素を隠蔽すること
• 堅牢で柔軟なシステム、要求の変更に強いシステムを目指す

自分の性分としては、頭ごなしの暗記ではなく理屈がひとつながりになっていないと理解した気になれないのですが、この本はその道筋をちゃんと示してくれました。
なぜ、これが重要なのか。なぜそう考えるのか。どう実践していくか。

おすすめです。

やっぱりassertThatは良いよねという話

追記 2016/6/12

テスト結果のメッセージを読みやすくしたいだけなら、assertThatにreasonを書く方が楽ですね。

stackoverflow.com

    @Test
    public void test() {
        File file = new File("/tmp/hoge");
        assertThat(file.getAbsoluteFile() + " should exist", file.exists(), is(equalTo(true)));
    }

java.lang.AssertionError: /tmp/hoge should exist
Expected: is <true>
     but: was <false>

追記終わり

assertThatやっぱ便利ですねー、という話です。

assertEqualsは何のテストに失敗しているのか分かりにくかった

public class AssertEqualTests {

	@Test
	public void test() {
		final File test1 = new File("/tmp/test1.txt");
		final File test2 = new File("/tmp/test2.txt");
		final File test3 = new File("/tmp/test3.txt");
		assertEquals(true, test1.exists());
		assertEquals(true, test2.exists());
		assertEquals(true, test3.exists());
	}

}

ファイルが存在しているかどうかをテストするだけです。
で、これを実行してみると、テストが失敗しました。

java.lang.AssertionError: expected:<true> but was:<false>

これだとどのファイルで失敗したか分からないですね。
まあスタックとレースをちゃんと見れば何行目のassertEqualsで失敗しているか分かるので判定はできるのですが、あまり直感的ではありません。

Matcherを作って原因を分かりやすくしよう!

そこでassertThatとhamcrestの出番です。
もっとわかりやすいメッセージを返してくれるMatcherを作ってみました。

public class FileExist extends TypeSafeMatcher<File> {
 
    private final boolean isEexpectedResult;
    private File inspected;
 
    public FileExist(boolean exceptedResult) {
        this.isEexpectedResult = exceptedResult;
    }
 
    @Override
    public void describeTo(Description description) {
        description.appendText(inspected.getAbsolutePath());
        if (isEexpectedResult) {
            description.appendText(" exist");
        } else {
            description.appendText(" does not exist");
        }
 
    }
 
    @Override
    protected void describeMismatchSafely(File item, Description mismatchDescription) {
        mismatchDescription.appendText(inspected.getName());
        if (isEexpectedResult) {
            mismatchDescription.appendText(" does not exist.");
        } else {
            mismatchDescription.appendText(" exist.");
        }
 
    }
 
    @Override
    protected boolean matchesSafely(File item) {
        this.inspected = item;
        return item.exists() == isEexpectedResult;
    }
 
    @Factory
    public static <T> Matcher<File> exist() {
        return new FileExist(true);
    }
 
    @Factory
    public static <T> Matcher<File> NotExist() {
        return new FileExist(false);
    }
 
}

TypeSafeMatcherを継承して独自Matcherを作っています。
ファイルを受け取って期待通り存在しているか、もしくは存在していないかをテストできます。
そしてdescribeToで成功時のメッセージを、describeMismatchSafelyで失敗時のメッセージを作成しています。

テストは以下のようになります。

public class AssertThatTests {

	@Test
	public void test() {
		final File test1 = new File("/tmp/test1.txt");
		final File test2 = new File("/tmp/test2.txt");
		final File test3 = new File("/tmp/test3.txt");
		assertThat(test1,exist());
		assertThat(test2,exist());
		assertThat(test3,exist());
	}

}

そして実行結果。

java.lang.AssertionError: 
Expected: /tmp/test2.txt exist
     but: test2.txt does not exist.

test2.txtが存在していないというのが一目でわかりますねー。素敵です。
Matcherを簡単に作れるというのは、結果の分かりやすくする事にも役立つんですね。

ちょっとはまったこと。

Matcherを作るとき、どうしてもdescribeMismatchSafelyが見つからず@Overrideがエラーを吐いてしまいました。
原因は我らがstackoverflowで見つかりました。

• junitライブラリ内部の古いhamcrestを参照してるんじゃない？今はhamcrestは別ライブラリだよ
• Junitを4.10以上にして、junit.jarとhamcrest-core.jarをビルドパスに加えてみ
• hamcrest-core.jarはjunit.jarより上位にしてね

第19回折紙探偵団コンベンション

今年も折紙探偵団コンベンションに参加してきました。

盛況でしたねー。
相変わらず老若男女国内外と様々な人達が参加していました。
折り紙のファン層って不思議ですね。

今回は初めてユニット系や難易度が低めの教室に参加しました。
いや・・・その・・・久しく折っていなかったので難易度が高めのを折る自信が無かっただけです。はい。

• U-cube ★★★ 霞 誠志
• セミ ★★★ 世浪 健
• 富士山 静岡View ★★ 鈴木美恵子
• バランスとんぼ ★★★ 中村淑子

最大でも星３個（中級？）。弱気な選択でしたが、リハビリにはちょうど良く楽しめました。

U-cube

バランスとんぼ。

セミ。

以下は展示されていた作品です。
正直、これらを見るだけでも大満足です。

バラ？実物にしか見えないですね。

ハチ。実物は7センチくらいで細かく作り込まれてます。

エヴァ初号機！

三頭龍。

某アメコミ。

Java8のLambdaの型推論が実行時にならいと型が分からない理由（追記あり）

JJUGナイトセミナー「Inside Lambda」に参加してきました。
Java8のLambdaの概要と、実装方法についてのお話でした。
非常に面白かったのですが、その中でLambdaの型推論が実行時にならいと型が分からないという話があったのでまとめてみます。

Lambdaの型推論

Lambda式の中ではコンパイラが推測できる場合は型を省略する事が可能です。

Comparator<Integer> comp = (x , y) -> x -y;

しかし、実際に型が決まるのはコンパイル時ではなく実行時になります。
それはなぜでしょうか？

Lambdaの実装

その答えは、ナイトセミナーの宮川さんの発表で理解できました。
それは、Lambdaがinvokedynamicを使って実装されているからです。
invokedynamicについては・・・これまた宮川さんの資料が分かりやすいです。
私の理解では、

• JVMで実際にメソッドを実行したりするのがInvokeなんたらのお仕事
• その中でもinvokedynamicはJava以外の動的型付け言語をJVMで動かすための機能
• そのためinvokedynamicは実行中にクラスファイルを動的に生成したりできる

という感じです。
で、Java8のLambdaはinvokedynamicを使って実装されているそうです。
そのため、実際に型が分かるのが実行時ということになります。

仕様？

@nagaseyasuhito いえ、違います。invokedynamicを使うかどうかは実装の問題です。 #jjug

— Yuichi Sakuraba (@skrb) 2013, 7月 22

@nagaseyasuhito invokedynamicが使われていないで、コンパイル時に無名クラスを作っていた時代もありましたよ ^ ^;;; #jjug

— Yuichi Sakuraba (@skrb) 2013, 7月 22

実装がたまたまそうなっている、という話だそうです。
なのでJava8が正式リリースされた時には、ひょっとしたらコンパイル時に型が決まるようになっているかもしれませんね。

実害はあるのか？

ちょっと考えてみたのですが思いつきませんでした。
実行時に決まるからどんな型になるかわからない？！って事はないですよね、これ。
あくまでコンパイラも型推論チェックをやっているので、実際に予期せぬ型になってしまうことはなさそうです。

まとめ

Scalaを使おう!

追記

きしださんからコメントをもらいました。

@sakamoto_desu 「型推論が実行時にならいと型が分からない」というの、「型がわからない」という表現は違うと思います。型は「Comparator<Integer>」だとわかっているので。

— きしだ (@kis) 2013, 7月 26

@sakamoto_desu 型推論としてはコンパイル時に「Comparator<Integer>」だと確定した時点で型が決まって、これ以上は型推論の話ではないです。

— きしだ (@kis) 2013, 7月 26

@sakamoto_desu そうですそうです。Runnable r = hoge(); で、hogeメソッドが返してきて実際に変数rに割り当てられるインスタンスの型が実行時まで決まらないのと、言語上でやってるかVM上でやってるかの違いだけで同じものという感じです。

— きしだ (@kis) 2013, 7月 26

というわけで、正確には「ラムダ式の型は実行時にならないと決まらない」という話でした。
タイトルも含めて書き直そうかとも思ったのですが、きしださんにコメントもらえた記念ということで追記だけにしておきます。