Let's write β

プログラミング中にできたことか、思ったこととか

形式手法

TLA+, SPINをつかってAPIサーバーの仕様を検証した

バックエンドサーバーのAPIの仕様を決めるにあたって、レスポンスの結果が常にみたしていてほしい不変条件がありました。 ビジネスの詳細に触れてしまうので、抽象的に表現すると 内部データのある属性値が1以上になっているならば、かならずレスポンスにふ…