diff options
| author | Brian Campbell | 2019-07-31 15:16:17 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-07-31 16:43:51 +0100 |
| commit | 2b64d1215c7b77d8cc37a4ab3c9ff2cc5a07e12b (patch) | |
| tree | b791c70a987fdad72fa7e1be15dea01f303fe32a /lib/coq/Sail2_state.v | |
| parent | 98cced7ef3cf89333e0e09d4ebf9ca3262b4e947 (diff) | |
Coq: reasoning for until loops
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
Diffstat (limited to 'lib/coq/Sail2_state.v')
| -rw-r--r-- | lib/coq/Sail2_state.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index bd18783f..dc635cb4 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -130,7 +130,8 @@ Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool else returnS vars else failS "Termination limit reached". -Definition whileST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := +Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := + let limit := measure vars in whileST' limit vars cond body (Zwf_guarded limit). (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> @@ -142,7 +143,8 @@ Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc) else failS "Termination limit reached". -Definition untilST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := +Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := + let limit := measure vars in untilST' limit vars cond body (Zwf_guarded limit). |