Comparing Weakest Precondition and Weakest Liberal Precondition

TL;DR

This paper explores the relationship between weakest precondition and weakest liberal precondition, showing their equivalence in deterministic, terminating sequential programs, and clarifying their relative strength in general.

Contribution

It provides a detailed comparison of weakest precondition and weakest liberal precondition, including conditions under which they are equivalent or differ.

Findings

Weakest liberal precondition is neither stronger nor weaker than weakest precondition in general.

They are equivalent for deterministic, terminating sequential while programs.

The choice of definition does not matter in specific deterministic, terminating cases.

Abstract

In this article we investigate the relationships between the classical notions of weakest precondition and weakest liberal precondition, and provide several results, namely that in general, weakest liberal precondition is neither stronger nor weaker than weakest precondition, however, given a deterministic and terminating sequential while program and a postcondition, they are equivalent. Hence, in such situation, it does not matter which definition is used.