実装コードから仕様を吸い出して Z3 / TLA+ でバグを払い出す — 実践プレイブック
formal-methods-playbook.md 実装コードから仕様を吸い出して Z3 / TLA+ でバグを払い出す — 実践プレイブック 既存システムの実装を「事実上の仕様」とみなし、それを形式化することで 「テストでは踏めないバグ」と「実装が暗黙に決めている仕様」を炙り出すための手順書。 仕様書が無い / あてにならない / 仕様と実装がずれている、という現場を前提にする。 0. 基本姿勢: コードが de-facto 仕様である 仕様書ではなく 実装が現に何をしているか を仕様の源にする。やることは3段: 吸い出し (extract): コードから「実装が主張している仕様」と「暗黙に決めている挙動」を分けて抜く 形式化して反例探索 (refute): 主張をモデル化し、それが全入力/全順序で本当に成り立つかを機械に攻撃させる 突き合わせ (reconcile): 出た反例を「こ
「サイゼリヤで1000円あれば最大何kcal摂れるのか」をSMTソルバー(Z3)で解いてみた。 - Qiita
前書き サイゼリヤ1000円ガチャをつくってみた(Heroku + Flask + LINEbot) 「サイゼリヤで1000円あれば最大何kcal摂れるのか」を量子アニーリング計算(Wildqat)で解いてみた。 完全に二番煎じですが、古典コンピューターが好きなので、個人的に古典コンピューター最強のなんだかよく分からないけどよく分からないものをよく分からないうちに解いてくれるソフト、z3を使ってサイゼリア問題を解いてみました。 問題 サイゼリヤのメニューを重複無しで合計1000円以下になるように選んだときに、最大の総カロリーになるようなメニューの組み合わせを求めよ。 サイゼリヤのメニューは https://github.com/marushosummers/Saizeriya_1000yen こちらを使わせて使わせて頂きました。メニューは100種類ぐらいみたいで、カロリーは整数値で、プロコ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - thomasjball/PyExZ3: Python Exploration with Z3
