#
1a82f8bd |
|
24-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: SepDSpec
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
0f38e200 |
|
25-Feb-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Many proof repairs.
|
#
47119bf4 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
fc9fc068 |
|
28-Jan-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
Session SepDSpec finished for isabelle2016-RC2
|
#
164f1db6 |
|
14-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
proof/capDL-api: 2015 update
|
#
acf0abe1 |
|
21-Jul-2014 |
Andrew Boyton <andrew.boyton@nicta.com.au> |
Cleanup of a number of definitions of the separation algebra for capDL. * The definitions of the separation "arrows" is slightly nicer and more consistent. - We have a nicer correspondence between sep_map_c and sep_map_s. - sep_map_irq now specifies exactly what the IRQ table contains (that it *only* has one entry, not that it contains at least that entry). - Nicer LaTeX output for the arrows. * A number of minor renaming of constants and types. - cdl_component => cdl_component_id - sep_entity => cdl_component - state_sep_projection => sep_state_projection - obj_to_sep_state => object_to_sep_state * Removed a few unused lemmas.
|
#
84595f42 |
|
17-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
release cleanup
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|