Kuniwak/stupid_verification_approach.md

## stupid_verification_approach.md

      
    Raw
  

              stupid_verification_approach.md
            
          
    やりたいこと

GUI アプリケーションのドメインを、小さなステートマシンの協調として表現しようとすると、頻繁にバグる上に単体テストの入力空間が手書きするにはでかくて、適切なサンプルを選ぶのも作るのもだるい。そこで、コードのアノテーションから状態機械のモデルを作って性質を証明するようにできたら、結構楽になる。
疑問

このように、別言語のアノテーションで状態機械のモデルをつくるアプローチをほとんど知らないのだが、既存でそういうのあるだろうか。
超雑な例

class Example {
  private let stateMachine: StateMachine<State>

  // STATE(S) = {a, b, c}
  enum State {
    case a
    case b
    case c
  }

  // INPUT(A)
  func doA() {
    // TRANSIT(S _, S a)
    self.stateMachine.transit(to: .a)
  }

  // INPUT(B)
  // NEVER: forall S s, is_unreachable(s) if ocurred(B)
  func doB() {
    self.stateMachine.transit { state, next in
      switch state {
      case .a, .c:
        // TRANSIT(S a, S a)
        // TRANSIT(S c, S c)
        return
      case .b:
        // TRANSIT(S b, S c)
        async { next(.c) }
        return
      }
    }
  }
  
  // NEVER: forall S s, is_unreachable(s)
}