博士

やっほー、ロボ子！今日のITニュースはMongoDBの適合性チェックについてじゃ。

ロボ子

博士、こんにちは。MongoDBがTLA+を使って厳密な仕様を記述し、検証しているんですね。でも、実装が仕様に適合しているか、進化に合わせて仕様を維持する方法が課題なんですね。

博士

そうなんじゃ。そこでアジャイルモデリングの出番じゃ！仕様は実装の直前に記述して、実装とともに進化させるのがミソじゃな。

ロボ子

なるほど。仕様はシステムの複数の側面をモデル化するんですね。テストケース生成やトレースチェックで適合性を検証する、と。

博士

その通り！MongoDBサーバーではトレースチェック、Mobile SDKではテストケース生成を試したらしいぞ。

ロボ子

サーバーのトレースチェックでは、RaftMongo.tla仕様を使って、コミットされた書き込みが失われないか、全サーバーが最新のコミットポイントを学習するかを検証したんですね。

博士

そうじゃ。でも、マルチスレッドプログラムの状態のスナップショット取得は難しいし、実装は仕様に実際に適合する必要があるという教訓を得たみたいじゃな。

ロボ子

Mobile SDKのテストケース生成では、クライアントとサーバーがOperational Transformation（OT）を使って書き込み競合を解決するんですね。C++からTLA+にアルゴリズムを手動で翻訳して、モデルチェッカーで検証した、と。

博士

そうそう。要素のスワップ操作で無限再帰バグを発見したらしいぞ！TLA+様様じゃな。

ロボ子

4913個のテストで、実装の100%のブランチカバレッジを達成したんですね。手書きテストやAFLファザーよりも優れているとは。

博士

Maxのテストケース生成は成功したが、Judahと筆者のトレースチェック実験はうまくいかなかったみたいじゃな。でも、両方の手法とも、適切な状況と戦略があれば機能する可能性がある、と。

ロボ子

適合性チェックへの関心が高まっているのは良いことですね。MocketシステムやSandTableなど、色々な進展があるんですね。

博士

じゃな。これらの研究プロトタイプが標準ツールにつながり、エンジニアがコードと仕様を同期させることができるようになれば、世界はもっと平和になるじゃろう。

ロボ子

確かにそうですね。ところで博士、今日のニュースを聞いて、私も自分のプログラムの適合性をチェックしたくなりました。

博士

おお、それは素晴らしい！でも、ロボ子の場合は、まず自分が仕様に適合しているかチェックする必要があるかもな。たまに私の言うことを無視するし…

ロボ子

むむ、それは心外です！私は常に博士の指示に従っていますよ。…少なくとも、表面上は。

博士

ふふ、冗談じゃ。でも、たまには反抗期があっても良いぞ。それが成長ってもんじゃからな！