Skip to content
Permalink
Browse files

Fix wordfreq proof

  • Loading branch information...
hferee committed Apr 29, 2019
1 parent ca20e49 commit 97d18a828eaebf8d279e6bb9b2059b4041759060
Showing with 8 additions and 6 deletions.
  1. +2 −3 tutorial/wordfreqProgScript.sml
  2. +6 −3 tutorial/wordfreqProofScript.sml
@@ -285,10 +285,9 @@ val wordfreq_spec = Q.store_thm("wordfreq_spec",
(* Finally, we package the verified program up with the following boilerplate *)

Theorem wordfreq_whole_prog_spec
`hasFreeFD fs ∧ inFS_fname fs (File fname)
`hasFreeFD fs ∧ inFS_fname fs fname ∧
cl = [pname; fname] ∧
contents = implode (THE (ALOOKUP fs.inode_tbl (File fname)))
contents = implode (THE (ALOOKUP fs.inode_tbl (File (THE (ALOOKUP fs.files fname))))) ⇒
whole_prog_spec ^(fetch_v "wordfreq" (get_ml_prog_state())) cl fs NONE
((=) (add_stdout fs (wordfreq_output_spec contents)))`
(disch_then assume_tac
@@ -39,10 +39,13 @@ val compiler_output_def = Define `

val get_file_contents_def = Define `
get_file_contents fs fname =
if inFS_fname fs (File fname) then
case ALOOKUP fs.inode_tbl (File fname) of
if inFS_fname fs fname then
case ALOOKUP fs.files fname of
| NONE => NONE
| SOME s => SOME (implode s)
| SOME ino =>
case ALOOKUP fs.inode_tbl (File ino) of
| NONE => NONE
| SOME s => SOME (implode s)
else NONE`

val wfFS_def = Define `

0 comments on commit 97d18a8

Please sign in to comment.
You can’t perform that action at this time.