[TLA+] TLA+と形式仕様言語 [目的と準備] | DevelopersIOこむろ＠札幌です。 今年も社内の人から「それ何の役に立つの？」「それXXで良くない？」と言われ、大体において理解されないニッチな分野で生きていきたいと思います。よろしくお願いします。 はじめに 仕様変更や改修によってプログラムにちょっとしたパラメータやフラグを追加したことはないでしょうか。僕はあります。そしてそれを追加するにあたって そのパラメータはどのような状態を持ち、状態を追加することで機能に影響はあるのか 追加したパラメータによってシステムの正常な動作が阻害されないか（もしくは破綻しないか） 取りうるパラメータのパターン全てで正しく動作するのか これら全てに明確に問題ないと答えられるでしょうか。（僕は無理です） 設計レビューやテスト等で全てをチェックするのはなかなか大変です。何らかの明確な根拠をもって問題ないと言っている人がどの程度いるでしょうか。 人の手によるチェックは限界がありま
![[TLA+] TLA+と形式仕様言語 [目的と準備] | DevelopersIO](https://cdn-ak-scissors.b.st-hatena.com/image/square/89031a72e135dcc98dbacf69370c9c72c122192b/height=288;version=1;width=512/https%3A%2F%2Fdevio2023-media.developers.io%2Fwp-content%2Fuploads%2F2019%2F01%2FTLA_logo_splash_image_3.png){kind=logo}
