Skip to content

Instantly share code, notes, and snippets.

@Kuniwak
Last active March 2, 2019 08:57
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Kuniwak/95e6ba8b1831b2e9d007d3e50c28b251 to your computer and use it in GitHub Desktop.

やりたいこと

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
Copy link
Author

Kuniwak 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