チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました

先日行われた JAWS FESTA 東海道 2016 で登壇してきました。

www.slideshare.net

テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。

  • Alloy を使うためにの最低限必要な言語機能を知る
  • シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する

ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。

ccvanishing.hateblo.jp

寄せられた質問

発表後に頂いたいくつかコメントや質問について、ここで説明しておきます。

「全探索」と言っているが、無限の範囲を探索するのは不可能なのでは?

はい、その通りです。Alloy におけるシグネチャは有限集合でしかありえないので、探索はその範囲に限られます。例えば、

run fooPred for 5

とすると各シグネチャの要素数が 5 個以下の場合を探索します。デフォルトは 3 です。

とはいえ、資料中に登場する 3 個の要素を持つ 2 種類のシグネチャ間の関係だけを考えるケースでさえ、考えうる関係の数は 2 の 3 * 3 乗で 512 通りもあります。実用的なモデルを書こうと思えば場合の数は急激に増えていくため、人力でテストケースを組むことを考えれば Alloy も捨てたものではありません。

ちなみにこのような Alloy の設計思想は「もし仕様バグが存在するなら、それは比較的小さなモデルの時点ですでに問題になるはずだ」というアイデアで正当化されています。この考え方は 小スコープ仮説 (small scope hypothesis) と呼ばれています。

AWS リソースを自前でモデル化するのは辛そう。ライブラリ化の予定は?

できたら面白いとは思っていますが、現実的には厳しそうです。

これは、ライブラリを作成しようと思うと、必然的に個別事例では必要のない部分(例えばセキュリティグループのみ考えてネットワーク ACL は使わない、など)までモデルに含まれてしまうためです。Alloy のモデルは関係が必ず集合に結びつく形で定義されているため合成可能性に乏しく、必要な要素のみライブラリから取り出して使用することが困難なのです。

現時点では、個別にそのとき必要な部分を取捨選択してモデル化するのが妥協案だと思います。

Alloy を勉強しようと思ったら何から始めるのがいい?

毎回名前を挙げていますが、以下の書籍がおすすめです。初見だと多少記述がとっつきづらく感じるかもしれませんが、実際に Alloy を動かしつつ読むと理解が深まるでしょう。なおこの本の内容を把握したら後は慣れの問題です。

estore.ohmsha.co.jp

おわりに

今回の発表、実は当初はここまで Alloy に特化せず、参照した論文中で述べられている AWS 内での取り組みをもう少し前面に出そうかと思っていました。スライドの途中で TLA+ の名前が出てくるのは名残です。

ただ TLA+ は完全にオートマトン型の典型的なモデル検査器であり、AWS使う側 とは相性があまり良くなかったため、具体的な内容は結局すべて外してしまいました。その分 Alloy についてはこの発表を聞いた人がとりあえず触ってみる程度のことは説明できたので、まあ結果オーライかなとは思います。

ところで、今年もまた名古屋のコミュニティ合同忘年会 NGK2016B がありますね? 自分はここ数年連続して色々なモデル検査ツールの発表をしているのですが、それはまた別の話。

AWS Summit Tokyo 2016 で形式手法について話してきました

先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。

www.slideshare.net

モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。

ccvanishing.hateblo.jp

NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。

なぜ形式手法なのか?

今回のテーマを一言でまとめると以下のようになります。

インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか?

ある程度の規模のインフラを長期間運用していると、どうしても初期の想定が変質してくることは避け得ません。アプリ側の要件が変わったりして、インフラ側がアドホックな対応を迫られるケースも(本来望ましくないですが)一定の割合で生じるものです。また、担当者が代替わりして暗黙知がうまく引き継がれない状況もあるでしょう。

必然的にカオスの縁にいる我々は、どうやってこの状況に対抗すべきでしょう? アプリ開発であればきっと「単体テスト書こうぜ!」みたいな流れになるわけですが、さてインフラを検証したい場合にどんな手段が取れるのか?

awspec

AWS + テスト」というキーワードで真っ先に思い出すのはおそらく awspec ではないかと思います。

github.com

awspec は servespec に着想を得たツールで、RSpec を利用して AWS リソースをテストできるようになっています。また、人間が直接 spec を記述するだけでなく、現に存在するリソースから awspec generate コマンドを使ってテストケースを自動生成することも可能です。

しかし、すでに存在するリソースをテストするという性質上、設計を考える段階での試行錯誤にはあまり向いていません。また、何かを変更しようとした際にそれをあらかじめ検証するという用途も難しいでしょう。好き好んで Amazon にお布施をしたい人は別として、テストそれ自体に掛かるコスト面も大きな問題です。

IAM Policy Simulator

さて、翻って他の方法を考えてみると、IAM のアクセス権限については、公式がシミュレータを提供してくれています。

docs.aws.amazon.com

実際の操作を行わなくとも dry run で検証できる、というのが大きなメリットで、例えば「削除」の権限をテストするのに実際の削除は発生しません。これがあれば、少なくとも IAM のアクセスポリシーを設定する際には、心ゆくまで試行錯誤ができそうです。

しかし(当たり前ですが)この機能は IAM 限定。となると、以下のような疑問が自然に生じます。

「現物」がなくても検証できる、汎用的な手法はないか?

この疑問への答えとして、現物ではなく形式化したモデルを検証することで有益な結果が得られるのではないか、というのが今回の発表の主題です。

形式手法とその限界

形式手法とは、システムの静的解析の中でも特に

  • システムの仕様を数学的に厳密に記述する
  • その正しさをやはり数学的に保証する

という特徴を持つ一連の手法を指して使われる用語です。現物と離れたところで堅く検証を行う、という意味では今回の目的にはピッタリです。

しかし如何せん、形式手法はコストがかかります。そもそも形式手法が扱える人間が少ないことに加え、大抵のツールでは従来のテストよりもずっと多くの工数が必要になります。そのため実際の形式手法の導入は、そのコストを支払ってもお釣りがくるほど高信頼性が求められる案件に限られているのが現状です。

今回の場合、どの程度ならコストとメリットが釣り合うのかはよく考える必要があります。形式手法を採用するのは手段であって目的ではないわけで、そこに必要以上に時間をかけるのはどう考えても本末転倒です。

このジレンマをなんとかするために登場するツールが Alloy Analyzer です。

アンチテーゼとしての Alloy

Alloy では関係論理を利用してシステムのモデルを定義し、さらにそこに検査したい制約を加えたものを充足可能性問題に変換することで、SAT ソルバを利用して条件を満たす例・満たさない例を全探索します。モデルの定義や制約の記述にはやや慣れが必要ですが、他のツールと異なり検証作業自体は自動化されており、上で述べたコストの問題はある程度クリアできます。

手軽に使用できる反面、当然ある種の欠点もあります。テストと比較して形式手法を語る際、メリットとしてよく「テストは有限個のケースしか検証できない。形式手法では無限個の入力に対して正しさを保証できる」という言い回しがなされることがありますが、Alloy についてこれは成り立ちません。

全探索を行うことからもわかる通り、Alloy による検証では、モデル中の要素の個数を制限する必要があります。この制限は例えば今回であれば「セキュリティーグループが 3 個以下の場合」のような但し書きとして現れます。

実は Alloy の背景には「仕様バグは小さなモデルで十分再現できる」という哲学があります。つまり、セキュリティグループが 10 個以上の場合に初めて現れる問題はそうそうないだろう、というわけです。この哲学は 小スコープ仮説 (small scope hypothesis) と呼ばれており、ある種の割り切りによって支えられています。

おわりに

今回の発表では、インフラの検証に形式手法が使えること、およびそのためのツールとして Alloy Analyzer を紹介しました。Alloy に興味を持った人は、以前の記事でも紹介していますが、以下の参考書が鉄板です。

estore.ohmsha.co.jp

ちなみに余談ですが、実は(AWS を利用する側ではなく)AWS そのものの設計にも形式手法が利用されています。しかも、形式手法を導入するにあたって Alloy が検討されていたにもかかわらず、結果的には要件に合わずに TLA+ という別のツールが採用されるという経緯を辿っています。

cacm.acm.org

この辺り、ツールの特性の比較などと絡めて考えると面白い話題でもあるのですが、それはまた別の話。

NL 名古屋で Frege の評価戦略について話してきました

先日の 歌舞伎座.tech に引き続き、NL名古屋 - connpassHaskellJVM 言語 Frege について発表してきました。

今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるのか、その内幕を解説しています。

www.slideshare.net

なお当日の様子は NL名古屋 -NLとはなんだったのか- #nlnagoya - Togetterまとめ にまとめられています。長丁場でしたが、各々さまざまなテーマの発表があり、楽しめるイベントだったと思います。

Java のコード生成を試してみよう!

発表中に述べている通り、Frege のコンパイラバイトコードではなく Javaソースコードを出力します。ただしスライド中で言及されているコードは Frege が生成した Java コードそのものではなく、今回の内容との関連が薄い部分をわかりやすく改変したものです。ここでは実際にどのようなコンパイル結果が得られるのかを見てみましょう。

コンパイラとコードの準備

Frege の Java 生成ロジックは、最新バージョン v3.24 から大きく変更になりました。今回の発表で述べられているのはこの新しい方のロジックです。

最新のコンパイラはまだ α 版で、各種ビルドツールではまだ使用できないようなので、直接バイナリをダウンロードします。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.24alpha/frege3.24.61.jar
$ chmod +x fregec.jar

次に、スライド中で登場した竹内のたらい回し関数をサンプルとして使用します。以下の Frege コードを Tarai.fr として保存してください。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else tarai (tarai (x - 1) y z)
                   (tarai (y - 1) z x)
                   (tarai (z - 1) x y)

ビルド結果が散らからないように、出力先として build ディレクトリを作成しておきましょう。

$ mkdir build

コンパイル結果の確認

以下のコマンドでコンパイルを実行します。

$ java -Xss1m -jar fregec.jar -d build Tarai.fr

しばらく待つと build 以下に Tarai.javaTarai.class が生成されます。

今回の目的である build/Tarai.java を確認してみましょう。ファイルの前半はボイラープレートなので無視して、以下の部分が tarai 関数の変換結果です。

final public static int tarai(int arg$1, int arg$2, Lazy<Integer> arg$3) {
  tailrecursion: while (true) {
    final int arg$1f = arg$1;
    final int arg$2f = arg$2;
    final Lazy<Integer> arg$3f = arg$3;
    if (arg$1f <= arg$2f) {
      return arg$2f;
    }
    else {
      arg$1 = Tarai.tarai(arg$1f - 1, arg$2f, arg$3f);
      arg$2 = Tarai.tarai(arg$2f - 1, (int)arg$3f.call(), Thunk.<Integer>lazy(arg$1f));
      arg$3 = Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3f.call() - 1, arg$1f, Thunk.<Integer>lazy(arg$2f)))
          );
      continue tailrecursion;
    }
  }
}

まず気づくこととして、Frege 側の tarai 関数は再帰の形で定義されていましたが、末尾再帰最適化の結果ループ tailrecursion に変換されています。このままだと本題が見えづらいので、Tarai.fr を以下のように書き換えてあえて最適化しないようにしてみましょう。

module Tarai where

tarai :: Int -> Int -> Int -> Int
tarai x y z =
    if x <= y
        then y
        else 0 + tarai (tarai (x - 1) y z)
                       (tarai (y - 1) z x)
                       (tarai (z - 1) x y)

生成される build/Tarai.java は以下のように変化します。

final public static int tarai(final int arg$1, final int arg$2, final Lazy<Integer> arg$3) {
  if (arg$1 <= arg$2) {
    return arg$2;
  }
  else {
    return 0 + Tarai.tarai(
              Tarai.tarai(arg$1 - 1, arg$2, arg$3), Tarai.tarai(arg$2 - 1, (int)arg$3.call(), Thunk.<Integer>lazy(arg$1)),
              Thunk.<Integer>shared(
                    (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3.call() - 1, arg$1, Thunk.<Integer>lazy(arg$2)))
                  )
            );
  }
}

ここから、識別子をわかりやすく x y z に変更して不要な修飾子も削ったものがスライド中に登場したコードです。

static int tarai(int x, int y, Lazy<Integer> z) {
  if (x <= y) {
    return y;
  } else {
    return tarai(
        tarai(x - 1, y, z),
        tarai(y - 1, (int)z.call(), Thunk.<Integer>lazy(x)),
        Thunk.<Integer>shared(
            (Lazy<Integer>)(() -> tarai((int)z.call() - 1, x, Thunk.<Integer>lazy(y))))
    );
  }
}

まとめ

本記事では、発表中に端折り気味だった Java のコード生成部分について、実際のたらい回し関数のコンパイル結果を挙げて補足しました。スライドも合わせて確認してもらえると幸いです。

ちなみに、今回のたらい回し関数は単純に int をとって int を返すだけの関数でした。しかし実際の Frege コードにはもっと複雑な言語機能がいくらでも登場し、

などを Java 上で再現するために語るべきことは尽きません。いずれこのブログのネタにでもしますが、それはまた別の話。

歌舞伎座.tech #9 で Frege について話してきました

先日行われた 歌舞伎座.tech#9「異種プログラミング言語格闘勉強会」 - connpassHaskellJVM 言語である Frege について発表してきました。

今回の勉強会のテーマは「様々な言語に触れて視野を広げる」ということだったので、細かな言語仕様にはあえて触れていません。Frege 自体の紹介と、あとは JVM 言語として一番キャッチーな機能である Java 呼び出しについて解説しました。

www.slideshare.net

勉強会自体も、マイナ言語の話を一度にこれだけ聞けるというのは珍しくなかなか面白い経験でした。ちなみに個人的に一番の収穫だったのは Pony。歌舞伎座.tech#9でPonyについて発表しました - だいたいよくわからないブログ に発表者のブログ記事があります。

話さなかったこと

今回の発表で触れなかった部分にも、興味を惹くトピックがいくつか残っています。

例えば、今回メインに据えた Java バインディング周りでは

  • frege-native-gen について
  • 基本型、特に String の扱い
  • null や例外の扱い

さらに、Java 呼び出しとは別の Haskell にない機能として

  • ドット演算子による Lens 風の関数呼び出し

また、開発環境周りでは

などが二の矢として温めてある状態です。

これらについては近いうちにこのブログのネタにしようかとも思っているのですが、それはまた別の話。

すごい JVM 言語 Frege をたのしく学ぼう!

言わずと知れた Haskell の定番教科書『すごい Haskell たのしく学ぼう!』に登場するサンプルコードを、プログラミング言語 Frege に翻訳してみました。

github.com

Frege について

Frege は、JVM 上で動く純粋関数型プログラミング言語です。

github.com

最近、JVMLisp である Clojure の存在感を増してきている気がしますが、Frege はいわばその Haskell 版ですね。

文法的には Haskell + Javaメソッドを呼び出すための追加構文、といった感じ。細かな違いはありますが、Haskell が読める人間であれば理解に苦労することはないでしょう。実際『すごい Haskell』に登場するコードは、大部分が変更なく Frege に「丸写し」することが可能でした。

逆に、Java 方面から入って初めて関数型に挑戦したい人にとってはかなり敷居が高く感じられるはずです。動機として悪くはないと思いますが、良くも悪くも、先に(あるいは同時進行的に)Haskell のさわりを学んでおく必要があるでしょう。

Frege を試すには

Online REPL で実行

環境構築の手間さえ惜しむ怠惰なあなたのために、Web 上で Frege を実行できるデモサイトが用意されています。

右ペインにソースコード、左ペインが REPL で、compile ボタンを押すと REPL にモジュールがロードされた状態になります。GHCi と同じノリで使えるのでいろいろ試してみましょう。

コンパイルして実行

前提として JDK 7 もしくは JDK 8 が必要です。JDK 9 は問題が確認されている ので避けましょう。

まず Frege のリリースページ から jar ファイルで提供されているコンパイラをダウンロードします。 この記事を書いている時点での最新バージョンは 3.23.422 です。

$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.23.288/frege3.23.422-ga05a487.jar
$ chmod +x fregec.jar

次に、Frege が生成するファイルの書き出し先ディレクトリを準備しておきます。

$ mkdir build

そしてビルドする サンプルコード をダウンロードします。

$ wget https://raw.githubusercontent.com/Frege/frege/release22/examples/SimpleIO.fr

ここまでで、ディレクトリ構造はこんな感じ。

$ tree
.
+--- SimpleIO.fr
+--- build
`--- fregec.jar

以下のコマンドでコンパイルできます。

$ java -Xss1m -jar fregec.jar -d build SimpleIO.fr
$ tree
.
+--- SimpleIO.fr
+--- build
|    `--- examples
|         +--- SimpleIO$1$1.class
|         +--- SimpleIO$1.class
|         +--- SimpleIO$1Fprompt_28850$1.class
|         +--- SimpleIO$1Fprompt_28850.class
|         +--- SimpleIO$2$1.class
|         +--- SimpleIO$2.class
|         +--- SimpleIO$IJ$$mainƒ52393afc.class
|         +--- SimpleIO$IJ$eofƒ5207be3f.class
|         +--- SimpleIO$IJ.class
|         +--- SimpleIO.class
|         `--- SimpleIO.java
`--- fregec.jar

コンパイルされた .class ファイルは以下のコマンドで実行できます。ちなみに SimpleIO の中身は、標準入力から数字を受け取って偶数か奇数かを判定するというものです。

$ java -Xss1m -cp build:fregec.jar examples.SimpleIO

もう少し知りたい人のために

現状、入手できる Frege の情報は残念ながらそれほど多くありません。とりあえず 公式 Wiki を読みましょう。またほぼ全ての関連情報は README 内のリンク集にまとまっています。

文法要素などでわからないところがあるときは、GitHub の Frege リポジトリ内を検索するとヒントが見つかるかもしれません。また、幸か不幸か Frege のコミュニティはとても小さいので、Twitter で #frege タグをつけて英語でツイートすると意外と中の人がアドバイスをくれたりします。

まとめ

今回は、HaskellJVM 言語である Frege について紹介しました。良くも悪くも Haskell に対する理解が必要ではありますが、そこさえ乗り越えてしまえばほぼ Haskell を書きながら Java エコシステムの肩に乗れるという意味でなかなか面白い言語です。

なおこの記事では触れませんでしたが、JVM 言語の例に漏れず Frege から Javaメソッドを呼び出すことが可能で、しかもその方法はかなり巧妙に設計されています。具体的には副作用を持つメソッドST モナドにマップするのですが、それはまた別の話。

Alloy で自動定理証明っぽいやつ

このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。

とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させることを目標にします。

なお、以下で部分的に引用しているモデル定義の完全版は alloy_sequent.als · GitHub にアップロードしてあります。

モデル化してみる

命題論理式の実装

まず対象となる論理式を Alloy で記述します。

abstract sig Formula {}

sig Atom extends Formula {}

sig Not extends Formula {
    of : one Formula,
}

abstract sig BinaryLogicOperator extends Formula {
    left  : one Formula,
    right : one Formula,
}
sig And, Or, Imply extends BinaryLogicOperator {}

二項演算子たちを定義する際、独立に定義せず間に抽象シグネチャ BinaryLogicOperator を挟んで extends で継承しています。これは Alloy 上の関係には多相性がなく、同じ名前の関係は同じシグネチャ間にしか定義することができないためです。つまり演算子をそれぞれ個別に定義した場合、引数を指す関係名を、例えば andRight : And -> Formula のように演算子ごとにつける必要が生じてしまいます。

そこで、引数を left, right とした BinaryLogicOperator を経由することで、すべての演算子に共通して課したい制約を

fact formulaeAreAcyclic {
    all f : Formula | f not in f.^(of + right + left)
}

のように統一的に記述できるというわけです。

シークエントの実装

さて、次にシークエントの定義を記述します。

sig Sequent {
    antecedents : set Formula,
    succedents  : set Formula,
}

通常の記法で言えばシークエント  \Gamma \vdash \Delta \Gammaantecedents,  \Deltasuccedents です。

本来、これらは「論理式の列」として個数と順番を考えて保持されるべきですが、今回は古典命題論理しか考えないので個数も順番も無視して単なる集合 set として扱います。部分構造論理が好きな人は潔く諦めましょう。

推論規則の実装

シークエントができたら、推論規則も Alloy に載せましょう。

論理式の場合と同じく、もとになる抽象シグネチャを定義します。

abstract sig InferenceRule {
    premises   : some Sequent,
    conclusion : one Sequent,
}

前提 premises は最大 2 個になり得るので some で、結論 conclusion は必ず 1 個なので one で定義しておきました。

なお、公理は前提が空なる推論規則であると考えて premisesset で定義することも考えられますが、この場合、検証の際に証明図を構成する InferenceRule の数が増えてしまいます。ここでは探索空間の最適化を優先することにして、公理は始シークエント InitialSequent として別途定義することにします。

そして、InferenceRule を継承して個々の推論規則を実装します。今回のように継承先によって異なる性質が要求される場合、Alloy ではシグネチャファクトで制約を記述するのが便利です。例えば以下の規則

sig NotRight extends InferenceRule {
} {
    one premises
    some f : Formula, n : Not {
        f in premises.antecedents
        f in n.of
        n in conclusion.succedents
        premises.antecedents - f = conclusion.antecedents
        premises.succedents = conclusion.succedents - n
    }
}

は否定の導入規則


    \displaystyle
    \frac{A, \Gamma \vdash \Delta}{\Gamma \vdash \Delta, \lnot A}

に対応しています。

同様にして各論理演算子に対応する規則 NotLeft, AndRight, AndLeft, OrRight, OrLeft, ImplyRight, ImplyLeft を定義しておきます。

なお、すでに述べた通りシークエントに登場するコンテクストを集合として実装しているため、構造規則が必要ない(逆に言えば表現できない)ことに留意しましょう。また cut 規則も本質的には必要ないはずなのであらかじめ外しておきます。

証明図の実装

最後に、ここまで登場した要素を積み上げて全体で一つの証明図になるよう制約を加えます。

fact noIsolatedFormulae {
    Formula in Sequent.(antecedents + succedents)
}

sig RootSequent in Sequent {
} {
    this not in InferenceRule.premises
}

sig InitialSequent in Sequent {
} {
    some antecedents & succedents
}

fact rulesFormAProofTree {
    one RootSequent
    Sequent - InferenceRule.conclusion = InitialSequent
    no r : InferenceRule | r in r.^(conclusion.~premises)
    all s : Sequent - InitialSequent | one conclusion.s
}

ここでは、シークエントの中で特殊なポジションを持つものが in 記法により定義されています。 証明されるべき最終的な主張が RootSequent, また公理として扱われる始シーケント


    \displaystyle
    A, \Gamma \vdash \Delta, A

InitialSequent です (2015/12/23 誤植を修正)。

証明図全体は制約 rulesFormAProofTree により、RouteSequent を根とし、InitialSequent を葉とする二分木になります。

検証してみる

無矛盾性の検証

まず、ここまでに定義した Alloy モデルを使って、矛盾を表す前件、後件ともに空なるシークエントが証明されない(であろう)ことを確認してみましょう。

assert consistency {
    no s : Sequent | s.antecedents = none && s.succedents = none
}
check consistency for 3

assert に対して check を実行すると、Alloyアサーションに対する反例を探索します。シークエント計算が正しくモデル化されていれば、ここでは反例が発見されないはずです。

排中律の検証

もう一つ、今度は簡単な定理の例として排中律の証明を Alloy に探索させてみましょう。求めるべき主張は  \vdash A \lor \lnot A なので以下の pred を満たす証明図を run で探索させれば OK です。

pred excludedMiddle {
    some x : Atom, n : Not, o : Or {
        x in o.left
        n in o.right
        x in n.of
        RootSequent.antecedents = none 
        RootSequent.succedents = o
    }
}
run excludedMiddle for 3

以下のような結果が出力されます。

f:id:y_taka_23:20151223185313p:plain

まとめ

とりあえず、今回は試みとして最も単純な古典命題論理のシークエント計算を Alloy でモデル化し、証明を自動探索させてみました。

この他にも例えば、真偽値をシグネチャとして用意し、論理式の評価結果を制約として加えれば、シークエント計算の健全性を示すことができるかもしれません。また、他の体系、例えば直観主義に変更すれば、上で示した排中律の証明は発見できなくなったりするはずです。次なる拡張の方向性はいくつかありそうですが、それはまた別の話。

NGK2015B で AWS + Alloy について話してきました

先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。

www.slideshare.net

当日の動画は [3] NGK2015B(名古屋合同懇親会 2015 忘年会) - YouTube から見ることができます。

TL;DR

  • AWS でインフラ運用中
  • でも設定が大人の都合でカオスになりがちだったりして辛い
  • よろしい、ならば形式手法だ

サンプルコードを動かしてみよう!

まずはインストールしてみる

公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。

java -jar alloy4.2.jar

でウィンドウが起動すれば OK です。

なお、dmg 版も提供されていますが、Mac の人は(少なくとも現状)これをインストールしてはいけません。"Requires Java 6" と宣言している通り、内部のソルバ部分の実装が古い Java ランタイムに依存しているようで、Java 8 では起動できません。ちなみに現在 id:osiire さんが修正版を fork しています。

github.com

早速、検査してみる

今回の LT で使用したサンプルコードが Alloy による AWS セキュリティグループのモデリング · GitHub にあるので、手元にダウンロードして Alloy で開いてみましょう。

そしておもむろに Execute をクリック(または command + E)で

f:id:y_taka_23:20151213173756p:plain

条件に合う設定が自動で探索されるはず。おめでとうございます。これであなたも立派な Alloy エンジニア!

ちょっと条件を変えてみる

Next を押すと、条件に合致する例が次々と表示されるのがわかると思います。しかし数が多すぎるし、各々の違いが解りにくいですね?

探索させる条件である run に対して、それぞれの要素(Alloy では atom と呼びます)の個数を制限することができます。以下のように変更して再度実行してみましょう。

run {
    some disj i1, i2 : Instance, proto : Protocol, port : Port
    | inboundOK[i1, i2, proto, port] &&
      outboundOK[i1, i2, proto, port]
} for 2 Instance, 2 IP, 1 CIDR, 1 SecurityGroup, 2 Rule, 1 Port

ちょっとだけ図がすっきりしました。ちなみに、上記を 1 Rule にすると探索が失敗することも確認してみましょう。インスタンス間の通信が成立するためにはインバウンドルールとアウトバウンドルールが少なくとも 1 つずつ必要ですからね。

さて、セキュリティグループのルールに直接 CIDR を指定すると、何のサーバなのかわからないし、後々管理が辛くなりそうですね?「すべてのルールについて、source / destination は(CIDR ではなく)セキュリティグループ名で指定する」という制約を加えるには以下のようにすれば OK。

run {
    some disj i1, i2 : Instance, proto : Protocol, port : Port
    | inboundOK[i1, i2, proto, port] &&
      outboundOK[i1, i2, proto, port]
    Rule.(source + destination) in SecurityGroup
}

他にも思いつく制約をいろいろ試してみましょう。

そしてその先へ……

さて、Alloy を少し触ってみてちょっと面白そうだと思ったあなたに、第一にお勧めしたいのがこちら。

www.amazon.co.jp

Alloy の背景にある関係モデルも含めてしっかり解説されており、密度の高い良書です。サンプルや練習問題も trivial なものから歯ごたえのあるものまで幅広く掲載されており、これを完全にフォローすれば Alloy を使う上でもはや不足はないと言ってよいでしょう。

また、書名に Alloy は入っていないのですが、こちらの書籍も面白いと思います。

www.amazon.co.jp

Alloy そのものというよりは、実際の仕様や開発ライフサイクルに対してどのように形式手法が関わるのかについて焦点を当てた、より実務者向けの参考書です。

ところで自分はといえば、

みたいな野望があったりなかったりするのですが、それはまた別の話。