diff --git a/CHANGELOG.md b/CHANGELOG.md index ec6d1bd7aec4d8057051ce37084c742956e65b1d..548ce8d50ec9ac2aa45205bac7d7bf99bf4ce83b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,15 +13,14 @@ Changes in and extensions of the theory: * Constructions for least and greatest fixed points over monotone predicates (defined in the logic of Iris using impredicative quantification). * Add a proof of the inverse of `wp_bind`. -* Support verifying code that might get stuck by distinguishing - "non-stuck" vs. "(potentially) stuck" weakest preconditions. (See - [Swasey et al. OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ - Φ }}` ensures that, as `e` runs, it does not get stuck. The stuck - `WP e @ E ?{{ Φ }}` ensures that, as usual, all invariants are - preserved while `e` runs, but it permits execution to get stuck. The - former implies the latter. The full judgment is `WP e @ s; E {{ Φ - }}`, where non-stuck WP uses *stuckness bit* `s = not_stuck` while - stuck WP uses `s = maybe_stuck`. +* Support verifying code that might get stuck by distinguishing "non-stuck" + vs. "(potentially) stuck" weakest preconditions. (See + [Swasey et al., OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ Φ }}` + ensures that, as `e` runs, it does not get stuck. The stuck `WP e @ E ?{{ Φ + }}` ensures that, as usual, all invariants are preserved while `e` runs, but + it permits execution to get stuck. The former implies the latter. The full + judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s + = not_stuck` while stuck WP uses `s = maybe_stuck`. Changes in Coq: