Formal Specification Language

• https://www.ifi.uzh.ch/dam/jcr:a39169f2-dc62-4507-ab8a-de35942fb09b/RE_I_Slides_Part_II_10-13.pdf
  theorem-proof の話になる

• 形式手法でデータ構造を記述・検査してみよう：Alloy編 - DeNA Testing Blog

  • term 小スコープ仮説: 小さい例でもだいたいの反例は見つかるはず

• Object Constraint Language モデル記述に制約を付けたみたいな

  • 契約プログラミングみたいに事前条件事後条件みたいなの書ける

• Alloy 6 の新機能 Mutable Field と線形時相論理

model-checking と同じで探索空間が直積なので膨大

• Frontend E2Eテストの安定化の取り組み | メルカリエンジニアリング

  • 単調性を利用して探索空間減らせたりしないのだろうか

• Saturation-Based Model Checking of Higher-Order Recursion Schemes
  https://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/csl2013.pdf

  • Higher Order Recursion Scheme ってなんだ
  • 高階モデル検査
    • 再帰がある無限木の検査が出来るらしい
      • 抽象モデル検査 の分野 model-checking