diff options
Diffstat (limited to 'content/zettel/3c3g6a.md')
| -rw-r--r-- | content/zettel/3c3g6a.md | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3c3g6a.md b/content/zettel/3c3g6a.md new file mode 100644 index 0000000..e98773e --- /dev/null +++ b/content/zettel/3c3g6a.md @@ -0,0 +1,27 @@ ++++ +title = "Abstract Predicates being Unevaluable" +date = "2022-11-17" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3g6"] +forwardlinks = ["3a8g5g"] +zettelid = "3c3g6a" ++++ + +One issue with having abstract predicates is that they could just not be +evaluable, because the semantics of abstract predicates is so much more +rich than standard predicates. For example, one must assume that one can +evaluate the whole predicate, which means that one must show that all +the computations will terminate and not get stuck. Another solution +would be to use three-valued logic to perform the equivalence check, +which would be able to reason about cases that are unevaluable. This +would be possible because a three-valued logic checker has now been +implemented in CompCertGSA ([\#3a8g5g]). However, the main problem that +I am anticipating is that when doing the reverse proof, one has to be +able to show that the original program that generated the symbolic state +is also evaluable, which would require reasoning about the evaluability +explicitly anyways. If that is the case, then using three-valued logic +only adds complexity to the proof. + + [\#3a8g5g]: /zettel/3a8g5g |