仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blog

こんにちは、SWETの鈴木穂高（@hoddy3190）です。 私はこちらの記事に記載の通り、形式手法の可能性を模索しています。 現在はツールやゲームの仕様を形式的に記述すること（形式仕様記述）で、仕様の欠陥をなるべく早く見つける取り組みにチャレンジしています。 今回は仕様記述をするにあたりよく使う重要な記述テクニックである「Promotion」を紹介します。 形式仕様記述とAlloyというツールを知っている人を対象にしています。 もし形式仕様記述やAlloyをご存じない方は、以前私がbuilderscon tokyo 2019で発表したときに使った資料をご覧ください。 Promotionとは 一般にソフトウェアシステムは複数のコンポーネントから構成されます。 システム全体としての状態（以下、システム状態）は各コンポーネントの状態の組み合わせからなります。 たとえどんなに奥深くのどんなに小さ

[AyeBee_TY]

「品質はベンダが担保してバグが出たら引責するからOK、ただし品質向上のためのコスト増は認めない」って現場ばかりなのでなかなか取り入れられないやつ。かなしい。

[taka_sek]

最近形式仕様記述の世界に入門したけど、状態の変化を静的な数式で表現すると頭のスイッチ切り替わっていって、いろいろな考慮漏れに気づけるので良い

[crexist]

面白い取り入れてみたいな。"自然言語で書かれてる仕様にバグはほとんどなかった""書かれてない仕様にバグが集中してる" というのはどーしようもない気がするけどね。

[otihateten3510]

超高品質が求められる界隈ではこういう感じなのかなと想像してる（けどサービス界隈ってここまで要求するとコストが上がっちゃうよね）

[usadamasa]

なるほどわからん。