Automatic Inference of Necessary Preconditions

Preview

This week I’ll present “Automatic Inference of Necessary Preconditions” by Cousot, Cousot, Fähndrich, and Logozzo (VMCAI 2013). They focus on the necessary preconditions for an alarm to happen and define several techniques to hoist the necessary conditions to method entry points to infer contract requirements in a Design by Contract programming environment.

Summary

The paper focuses on the problem of automatically infer preconditions. It argues that inferring sufficient preconditions for a program to not be correct is a difficult problem mainly because we need to introduce approximations (widening) to tackle constraints involving cycles in the CFG hence we will end up in stronger sufficient preconditions which may not work for some correct programs. Then the paper focuses on a dual problem: inferring necessary preconditions. In case of a necessary precondition violation, the program will definitely fail and the contract requirements will always be weaker than the weakest liberal precondition. The paper uses three abstract interpretation-based techniques to infer different kinds of preconditions:

1. All-paths precondition analysis: This analysis hoists a precondition whose value doesn’t change in any program paths to the method entry.
2. Conditional-path precondition analysis: This analysis infers disjunctive predicates by taking into account the tests that lead to different program points. It uses dual widening to compute an underapproximation of the necessary precondition in case of loops.
3. Quantified precondition analysis: This analysis synthesizes universally quantified preconditions to handle preconditions that need to hold all elements for an array.

Finally, the proposed analysis combined these three techniques with a worklist algorithm to compute an interprocedural fixpoint for necessary preconditions.

Discussion

Miroslav suggested that designing an analysis that can generate existential preconditions can handle certain kinds of loops (like loops that check for existence of a null element) more precisely. However, general theory of arrays equipped with both existential and universal quantifiers is undecidable. We had a couple ideas to make this kind of approaches work, such as having a separate analysis inferring only existentials or designing a coarser abstract domain for quantified array formulas to ensure termination.