プログラムを楽に近似的に証明するための手法を考えてみる
全てを正しく証明し切るのは難しい
考慮事項
手順が曖昧すぎてコンテスト中に行えない可能性が高い（ので仮説と掲げている）
少なくとも、これを有用な例にするためには例を蓄積する必要がありそうだ 1. プログラム全体が結果を示すために必要な命題を表記する
これは問題文を元に明記できる。
2. 命題$ Pをもとに、各部分プログラムにおいて証明されるべき命題$ \{P_i\}_iを挙げる。 なぜ各部分プログラムがその事項を証明できるのか「必要なだけ」下って証明を記述する。
必要条件$ P_iを列挙し、そこから演繹で本来の命題$ Pを導けるかを検証しておく。 3. ある実行が容易な問題例を用意して、その上で動作させる。 #TODO 実際にバグに当たった時にこの手法が有効か検討する。 1. 終了地点で、充足可能なフレームにおいて、最も多くのoを含むものを探す。 充足可能なフレームとは「フレーム内を操作でoで満たすことができるようなフレーム」を示す
2. ある列において、全ての充足可能なフレームのうち最も多くのoを含むものを探す。（1ループの処理）
なぜその1ループがこの題意を満たすことができるか？
forループ内で全ての当てはめ可能なフレームを列挙する。
全ての当てはめ可能なフレームに対して充足可能かを調べる。
充足可能な要素に対して最大値の更新を行っている。
プログラムの各部分が期待すべき動作を列挙する。
3. 簡単な問題例に沿って実行してみる。
code:txt
4 4 3
ooxo
..xx
..xo
....
全てのフレームに対して充足可能であるかが検査できていない
---> バグがあると気づくことができる。
...と書いたはいいけど、机上の空論かも。
ある問題例に対して実行した際に出てきた結果が数学的に正しいか検証する。 問題のスケールは$ N = 5ぐらいが望ましい。
この際、結果が正しいかだけでなく、何を以って正しいと判断したかもトレースする。 何をトレースするかを定める必要はありそうappbird.icon
ここをトップダウン的に定めよう
優先順位をつけたい
プログラムが終了して結果が出てきた地点で、示したい題意が示せているかを確認する。
こうすると、一見正しいコーナーケースでも間違いをあぶり出せる...かもしれない。
今回のテストケースだと、最大値のうち一番上に位置するフレームが考慮されていないことがわかる。
この際以下の点に注意する
入力の値域に対して実際に表現できる値域は十分に大きいか
実際に検証されるべき要素はどこか
間違いを確認できなかった場合
if文の分岐で通過していないポイントを通るように例を列挙する。
部分プログラムに関してさらに検証を行う。
やっぱこれ現実的じゃないわ！appbird.icon
時間が限られてる中でこの方法論を適用するのは難しい