2015/12/13 by Andrew E. Santosa, Santosa, Andrew E.
Computer Science · Decision Sciences · #D.3.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Probabilistic and Robust Engineering Design #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1512.04013
arxiv created 2015/12/13 · openalex publication_date 2015/12/13 · arxiv updated 2015/12/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.