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

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

ピクシブ株式会社様にてモデル検査器 Alloy の入門ハンズオン開催中！しかも今までにないハッシュタグの盛り上がりです。今回は @shimashima35 さんから引き合いを頂きました。後編も乞うご期待！ #モデル検査ハンズオン pic.twitter.com/3M1WhIQEF6
— チェシャ猫 (@y_taka_23) February 20, 2019

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

形式手法とは

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

開催までの経緯

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

参加希望者を 5、6 人集めていただければ出張講師やりますよ。今までの例だと初回は平日の夜に 2 時間程度、内容は Alloy に初めて触る人向けの入門ですが要望に応じて調整可能です。よかったらご検討下さい。#モデル検査ハンズオン https://t.co/x6TQlGqVR2
— チェシャ猫 (@y_taka_23) January 31, 2019

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

座学

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

演習

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

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

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