Noam Zilberstein

Outcome Logic

The goal of the Outcome Logic project is to develop a unifying foundation for program analysis in the modern era. Hoare Logic has been the de facto foundational theory of program analysis for the last 50 years. However, in that time numerous new requirements have arisen including the ability to reason about computational effects (such as probabilistic choice, concurrency, and quantum computation) and the ability to reason about program incorrectness.

Like Hoare Logic, Outcome Logic (OL) uses pre- and postconditions to specify program behavior in a compositional way. However, unlike Hoare Logic, OL pre- and postconditions are satisfied by a monoidal collection rather than an individual program state. This collection could be a set of nondeterministic program outcomes or a probability distribution over the outcomes in a randomized program, among others. The semantics of an OL triple is that running the program on any collection satisfying the precondition will result in a collection satisfying the postcondition:

OL is a generalization of Hoare Logic, in fact we can embed Hoare Logic in OL using an assertion logic that only allows reasoning about individual program states. OL has a proof system that is sound and relatively complete. Most of the proof rules mirror those of Hoare Logic, but the rule for while loops is more general, allowing us to derive all the standard rules for loops invariants (partial correctness), loop variants (total correctness), and probabilistic loops.

Computational Effects

Original formulations of Hoare Logic from the 1960s and 1970s already accounted for some computational effects such as nontermination and nondeterminism, however they were not handled in a uniform way. Two variants of Hoare Logic (partial and total) deal with programs that may not terminate vs programs that definitely terminate, respectively. In addition, Hoare Logic has limited facilities to reason about outcomes that arise due to nondeterminism; typically, the only option is to use a single assertion that applies to all reachable states.

Outcome Logic provides a new logical connective, the outcome conjunction, which states that the collection of program outcomes can be split to satisfy two different predicates individually. In the case of nondeterminism, the collection is a set and the basic assertions (P and Q below) describe nonempty subsets of the outcomes.

Nontermination can similarly be expressed as the lack of outcomes. Outcomes do not have to arise due to nondeterminism, but can also be modelled as the result of probabilistic choice. In the future, we would also like to formalize more computational effects in this way, such as outcomes that arise due to different concurrent interleavings of a program, or quantum computation.

Correctness and Incorrectness Reasoning

Peter O’Hearn recently advocated the need for incorrectness reasoning–reasoning about the presence of bugs. Incorrectness poses new challenges including the need to find true positive bugs and the ability to under-approximate program paths in order to scale to larger codebases. This led to the development of Incorrectness Logic, a program logic that is dual to Hoare Logic.

Outcome Logic offers an alternative foundational theory of incorrectness that is not dual to Hoare Logic, but rather a generalization of Hoare Logic. OL’s handling of nontermination and nondeterminism mean that it can identify true positive bugs because it gives reachability guarantees (unlike Hoare Logic). In fact, we have proven that any untrue OL triple can be disproven in the same logic meaning that if some correctness specification is not valid, then the bug can be expressed in OL.

Based on this result, we plan to devlop static analysis algorithms that can both verify correctness and find bugs in a codebase using a shared collection of procedure summaries.

People

Publications