Commit ca3c807e by Ralf Jung

### changelog nits

parent 0523bbf3
 ... @@ -13,15 +13,14 @@ Changes in and extensions of the theory: ... @@ -13,15 +13,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 * Support verifying code that might get stuck by distinguishing "non-stuck" "non-stuck" vs. "(potentially) stuck" weakest preconditions. (See vs. "(potentially) stuck" weakest preconditions. (See [Swasey et al. OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ [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 ensures that, as `e` runs, it does not get stuck. The stuck `WP e @ E ?{{ Φ `WP e @ E ?{{ Φ }}` ensures that, as usual, all invariants are }}` ensures that, as usual, all invariants are preserved while `e` runs, but preserved while `e` runs, but it permits execution to get stuck. The it permits execution to get stuck. The former implies the latter. The full former implies the latter. The full judgment is `WP e @ s; E {{ Φ judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s }}`, where non-stuck WP uses *stuckness bit* `s = not_stuck` while = not_stuck` while stuck WP uses `s = maybe_stuck`. stuck WP uses `s = maybe_stuck`. 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!