もっと精度を上げたほうがいいかも、だが難しい
「片方向伝搬法は精度が悪い」と書いたが、簡単な例でも実際に精度が悪い(苦笑)。
精度を上げるには、いくつかの方法がある。
- 論理系SILのなかで論理簡約をがんばる。
- 充足可能性問題の精度を上げる。
- 充足例問題の精度を上げる。
このなかで、充足可能性問題の精度を上げても、全体としてはあまり効果がないかも。充足不可能な制約を検出するとは、実行してはいけないプログラムの検出なので、まー意義はあるのだが、実行してよいプログラムの情報が増えるわけではない（ことが多い）。
論理系SILを働かせるのはそれなりの効果が期待できるが、SILが完全に定式化できてない。決定可能な論理システムかどうかも分からない。
最弱事前条件＝最汎制約の充足例を求めるのが一番いいのだけど、最適な充足例の定義がいまのところマッタク出来ない。原理的に出来ないような気もする。具体化しないで実行時の安全性を定義できるのだろうか？
