blob: e98773e9be3a70e8a78d636d8be372db15ec883c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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
|
