Commit fc21b664 authored by Robbert Krebbers's avatar Robbert Krebbers

Changelog entry for !177.

parent c93bee1d
...@@ -17,6 +17,8 @@ Changes in and extensions of the theory: ...@@ -17,6 +17,8 @@ Changes in and extensions of the theory:
* [#] Add weakest preconditions for total program correctness. * [#] Add weakest preconditions for total program correctness.
* [#] "(Potentially) stuck" weakest preconditions are no longer considered * [#] "(Potentially) stuck" weakest preconditions are no longer considered
experimental. experimental.
* [#] The adequacy statement for weakest preconditions now also involves the
final state.
* [#] The Löb rule is now a derived rule; it follows from later-intro, later * [#] The Löb rule is now a derived rule; it follows from later-intro, later
being contractive and the fact that we can take fixpoints of contractive being contractive and the fact that we can take fixpoints of contractive
functions. functions.
......
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