1

形式仕様記述シリーズ
シリーズリーダー
国立情報学研究所
石川 冬樹
講師
宇宙航空研究開発機構
小林 努

株式会社 proof ninja今井 宜洋(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

2扱う技術アプローチ
n 厳密な記述を用い強力な検証技術も活用
n 仕様や設計のあいまいさに起因する問題を排除
n 上流工程での問題検出による効率化・高品質化（プログラムに対する強力な検査も）
n テストなどあらゆる活動の基盤を底上げ
class イベント参加登録管理システム
登録済みユーザ集合 : set of 「ユーザ識別子」;
定員 : nat1;
inv card 登録済みユーザ集合 <= 定員
抽選登録する : set of 「ユーザ識別子」 ==> 「ユーザ識別子」
抽選登録する(引数ユーザ集合) == is not yet specified
precard 登録済みユーザ集合 < 定員and exists ユーザ in set 引数ユーザ集合 & ユーザ not in set 登録済みユーザ集合
post
登録済みユーザ集合 = 登録済みユーザ集合~ union {RESULT}
and RESULT in set 引数ユーザ集合 and RESULT not in set 登録済みユーザ集合~;

記述
#$%
&

(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

3

技術の利用イメージ（一例）
重要な制約を明記（これからできるコードは何を守るべきなのか）

実装詳細を捨象
厳密化

自然言語による仕様書や設計書

class イベント参加登録管理システム
登録済みユーザ集合 : set of 「ユーザ識別子」;
定員 : nat1;
inv card 登録済みユーザ集合 <= 定員
抽選登録する : set of 「ユーザ識別子」 ==> 「ユーザ識別子」
抽選登録する(引数ユーザ集合) == is not yet specified
precard 登録済みユーザ集合 < 定員and exists ユーザ in set 引数ユーザ集合 & ユーザ not in set 登録済みユーザ集合
post
登録済みユーザ集合 = 登録済みユーザ集合~ union {RESULT}and RESULT in set 引数ユーザ集合 and RESULT not in set 登録済みユーザ集合~;

上流との整合性確認もフィードバック
置き換えてしまった事例もclass イベント参加登録管理システム
登録済みユーザ集合 : set of 「ユーザ識別子」;
定員 : nat1;
inv card 登録済みユーザ集合 <= 定員

抽選登録する : set of 「ユーザ識別子」 ==> 「ユーザ識別子」
抽選登録する(引数ユーザ集合) == is not yet specified
precard 登録済みユーザ集合 < 定員and exists ユーザ in set 引数ユーザ集合 & ユーザ not inset 登録済みユーザ集合
post
登録済みユーザ集合 = 登録済みユーザ集合~ union {RESULT}
and RESULT in set 引数ユーザ集合 and RESULT not in set
登録済みユーザ集合~;

様々な検査
- テスト
- 証明など強力な検査- 具体例生成による妥当性確認なども(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

4

技術の利用イメージ： 有名な産業界事例
n FeliCaチップ：外部仕様を厳密に記述，テストn 多数の実装者や外部パートナーが活用する対象
n 後工程で検出された不具合のうち，記述の問題に起因するものはゼロに

n パリ地下鉄や空港シャトル，世界各国に展開：正しさが保証されたコードを仕様から導出
n 重要な部品について，数学的証明を通して仕様遵守が保証された形で段階的に詳細化
n 高信頼プロセス：仕様の議論・定義に大半の工数，「正しさを維持し実装へ」，単体テストは不要(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

5

受講生のこれまでの試み
n トップエスイーでのこれまでの演習・制作
n ビジネスプロセス，チップ処理ワークフロー，クラウドストレージ管理，アクセス制御，など多様な領域での試行
n 海外外注先への仕様書記述（日本語問題回避）
n 仕様書・設計書に関する定形化・機械処理（テスト仕様導出の自動化など）

n 最近の実践演習
n 自社システムを想定したケーススタディn 鉄道運賃やTDLファストパスの仕様記述(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

6

講義構成・扱う技術 （１）
記述の技術
システム全体の要求
外界環境に関する仮定

検証の技術

1-2．ライトウェイトな手法で体験
他の手法も広く俯瞰

ソフトウェア要求
形式仕様記述入門Ⅰ
VDM
設計
1-1．数理論理学の基礎も概観（実用上必要な最低限）
実装(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

7

講義構成・扱う技術 （２）
記述の技術

検証の技術

システム全体の要求
外界環境に関する仮定
2-2．強力な検査ツールについても体験
ソフトウェア要求
形式仕様記述入門Ⅱ
VDM
Alloy
設計
2-1．本格的な演習（標準仕様を題材にグループ演習）
実装(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

8

講義構成・扱う技術 （３）
記述の技術
システム全体の要求
外界環境に関する仮定

ソフトウェア
要求

検証の技術3-1．証明を通して徐々に複雑なモデルを構築しつつ強い正当性保証を得る
Event-B
高信頼ソフトウェアのための仕様記述と定理証明の活用
Coq

設計
3-2．証明を強力に活用し正しいプログラムを導出
実装(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

9

講義の履修方針に関するまとめ
n まずは入門「飛ばして後ろだけ」もできなくはないが推奨

1．形式仕様記述入門Ⅰ

n 2では演習が足りないかも
2．形式仕様記述入門Ⅱ

n より強力な検証アプローチに踏み込む
n 3．高信頼ソフトウェアのための仕様記述と定理証明の活用 1, 2を理解した上での発展(C) Fuyuki Ishikawa, National Institute of Informatics, 2021

10

形式仕様記述シリーズ
n （機能）仕様における下記アプローチを習得
抽象モデル化と “What”の厳密な記述
正しさの検証・保証
n 「形式仕様記述」という技術活用への第一歩
n 様々な課題に対して幅広く活きる原則・基盤
n モデルの抽象度制御（WhatとHowの分離）n あいまいさへの対処
n 正しさの定義や種類，様々な検証アプローチ(C) Fuyuki Ishikawa, National Institute of Informatics, 2021