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

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