Commit 042393e6 authored by Ralf Jung's avatar Ralf Jung

more experimental changelog

parent df0f72f0
...@@ -14,14 +14,14 @@ Changes in and extensions of the theory: ...@@ -14,14 +14,14 @@ Changes in and extensions of the theory:
* Constructions for least and greatest fixed points over monotone predicates * Constructions for least and greatest fixed points over monotone predicates
(defined in the logic of Iris using impredicative quantification). (defined in the logic of Iris using impredicative quantification).
* Add a proof of the inverse of `wp_bind`. * Add a proof of the inverse of `wp_bind`.
* Support verifying code that might get stuck by distinguishing "non-stuck" * [Experimental feature] Support verifying code that might get stuck by
vs. "(potentially) stuck" weakest preconditions. (See distinguishing "non-stuck" vs. "(potentially) stuck" weakest
[Swasey et al., OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ Φ }}` preconditions. (See [Swasey et al., OOPSLA '17] for examples.) The non-stuck
ensures that, as `e` runs, it does not get stuck. The stuck `WP e @ E ?{{ Φ `WP e @ E {{ Φ }}` ensures that, as `e` runs, it does not get stuck. The stuck
}}` ensures that, as usual, all invariants are preserved while `e` runs, but `WP e @ E ?{{ Φ }}` ensures that, as usual, all invariants are preserved while
it permits execution to get stuck. The former implies the latter. The full `e` runs, but it permits execution to get stuck. The former implies the
judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s latter. The full judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses
= NotStuck` while stuck WP uses `s = MaybeStuck`. *stuckness bit* `s = NotStuck` while stuck WP uses `s = MaybeStuck`.
Changes in Coq: Changes in Coq:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment