13-F-6 02/13 15:15 ～ 16:00
「厳密な共通言語」としての形式手法

言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗手段として、本セッションでは「形式手法」を紹介します。形式手法ではシステムの挙動を数学的に記述することにより、自然言語の持つ曖昧性を排除し、仕様が満たされるかどうかを厳密に検証することが可能になります。あなたの頭の中にある仕様がどのように「数学的な記述」に変換されるのか、具体例を通して体験してみませんか？

チェシャ猫[ProofCafe]

ProofCafe

普段の業務では、Docker や Kubernetes を中心としたコンテナオーケストレーション技術の検証と基盤設計を担当。それと並行してプライベートでは、関数型プログラミングや数理的手法によるソフトウェア検証について研究していたりいなかったりする。また、コミュニティ活動として ProofCafe および日本 Haskell ユーザーグループに所属し、各方面の勉強会やイベントにて登壇を行う。トレードマークは猫耳。