Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?

やりたいこと

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)
}
@Kuniwak

This comment has been minimized.

Copy link
Owner Author

commented Mar 2, 2019

色々教えていただいたキーワード:

  • jml
  • acsl
  • verifast
  • vcc
  • framac
  • infer
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.