From ca3c807eae69f59afd624cf5d257f85cdd2fe481 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 5 Dec 2017 18:27:58 +0100
Subject: [PATCH] changelog nits
---
CHANGELOG.md | 17 ++++++++---------
1 file changed, 8 insertions(+), 9 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index ec6d1bd7..548ce8d5 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:
--
GitLab