Simplification of Safe Kleene Predicate Logic Formulas Using Boolean Simplification and Term Normalization
Logic formulas are used for specifying preconditions for methods in computer programs. Those preconditions employ predicate logics and are evaluated whenever a method is called. Thus we want preconditions to evaluate as fast as possible. This thesis focuses on preconditions for data manipulating methods which are generated with a weakest precondition transformer.
Two approaches for simplifying such preconditions, which are three-valued Kleene predicate logic formulas, are proposed. The first approach abstracts from predicate to propositional logics. Then the properties of the generated preconditions are exploited to reduce them to the two-valued domain and apply existing two-valued minimization approaches.
The second approach focuses on the predicates, which are neglected in the first approach due to the propositional abstraction. A rule based simplification is proposed which focuses on reducing the computational complexity, i.e. the time they need to evaluate at runtime, of preconditions. Furthermore, this simplifications results in a normal form for predicate structures.