 It is also worth mentioning here that the work of Dijkstra (1976) on weakest precondition calculus is very much related to dynamic logic (and Hoare’s logic). In fact, what Dijkstra calls the weakest liberal precondition, denoted \(\mathbf{wlp}(S,Q)\), is the same as the box operator in dynamic logic: \(\mathbf{wlp}(S,Q) = [S]Q\), while his weakest precondition, denoted \(\mathbf{wp}(S,Q)\), is the total correctness variant of this, meaning that this expression also entails the termination of statement \(S\) (Cousot 1990).