テクノロジー

チェシャ猫さんを招いて、形式手法Alloyハンズオンを開催しました

shimashima shimashima
2019.3.5
シェア
ツイート
ブックマーク
トゥート

みなさんこんにちは!ピクシブで唯一のテスト専任エンジニアの @shimashima です。

2月20日に、kubernetesや形式手法で有名な チェシャ猫 さんを講師として招いて、形式手法の一つであるAlloyのハンズオンを開催しました。

今日はその紹介をしてみようと思います。

形式手法とは

国立情報学研究所の石川冬樹氏の定義によると 数理論理学等に基づき品質の高い ソフトウェアを効率よく開発するための 科学的・系統的アプローチ となります。これだとちょっとわかりにくいですが、ソフトウェアの仕様記述に自然言語ではなく数学をベースとした厳密な言語を用いることで、曖昧さがなく漏れや矛盾が生じにくくする手法です。 使われる言語としては今回のハンズオンで利用したAlloyの他にTLA+、VDM/VDM++、Z言語などがあります。

開催までの経緯

もともと私自身が形式手法に興味をもっていて、社内Slackの品質関連を話すチャンネルで数回ほど形式手法関連の情報を流していました。興味をもつ人もいたのですが、私自身実際に触ったことがなく使うのは難しそうという話をしていたところにチェシャ猫さんのTweetが目に入りました。

チェシャ猫さんに声をかけつつ社内で興味のある人を募ったところ8人程度手が上がったので、是非ということで依頼しハンズオンを社内で開催することになりました。

座学

前半は、スライドを使った形式手法とAlloyについての説明が行われました。 形式手法の紹介では、今回使うAlloyが含まれるモデル検査とCoqなどの定理証明との差異も解説されました。 形式手法一般の紹介の後はAlloyについての説明になります。Alloyの文法説明が論理学を交えて行われました。

演習

後半は実際の課題に対してAlloyでモデルを作っていく課題に取り組みました。題材は簡単なファイルシステムです。 ファイルシステムの木構造を抽象化して以下の順序で抽象化しAlloyで記述していきます。

  1. ファイルやディレクトリなどのデータ構造を定義する
  2. データ構造がファイルシステムの木構造と矛盾しないように制約を定義していく。Alloyではその場で実行してみることで制約に従った事例が表示されるので、制約が間違っているかがその場でわかる。
  3. 過剰な制約がないことを、 pred という論理式をつかって示す。
  4. 「親を持たないオブジェクトが常にちょうど 1 個だけ存在する」ことを、 assert check というAlloyの仕組みをつかって反例を探してみる。

対象がファイルシステムという比較的馴染みのあるものが題材で、演習時間も60分以上ありましたが私を含め参加者は皆苦戦しました。 Alloyに触ること自体がほぼ初めてで文法などに慣れていないこともありますが、通常のプログラムを書くのとパラダイムが違うため異なる思考法をしなければならないからだと思います。 結果、9名の参加者のうち最後まで到達したのは1名のみで、他の人はだいたい2つ目の制約条件記述で悩んでいました。

おわりに

2時間という限られた時間でしたが、形式手法にどっぷり浸かることができました。 参加者はほぼ全員形式手法未経験でしたが、形式手法Alloyの一端を知ることができたと思います。

講師のチェシャ猫さん、本当にありがとうございました。 当日参加できなかったエンジニアを含めて社内で補講を行い、後編も依頼したいと考えています。

ピクシブでは、形式手法を使ってソフトウェアの品質を向上させるエンジニアを募集中です。 【中途採用】技術スペシャリスト

シェア
ツイート
ブックマーク
トゥート