(******************************************************************************) (* Holfoot can proof partial correctness of programs using separation logic. *) (* *) (* The entire proof is done using HOL 4. This includes not just the the *) (* proof of some verification conditions, but also the generation of these *) (* conditions. This includes formal definitions of the programming and *) (* specification language as well as verified inferences. *) (* *) (* The semantics of the specs guarantee that no memory expect the explictly *) (* mentioned is accessed. This means that the array bounderies are always *) (* respected. Moreover, no it is guarenteed that no memory leak is present. *) (* However, Holfoot does not prove termination. *) (******************************************************************************) (******************************************************************************) (* Boilerplate (Load everything) *) (******************************************************************************) (* load the libries use (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/header.sml") *) val _ = HOL_Interactive.toggle_quietdec(); open sortingTheory listTheory; val _ = HOL_Interactive.toggle_quietdec(); (******************************************************************************) (* Prove an auxiliarz lemma *) (******************************************************************************) val SORTED_EL_DEF = prove (``SORTED R L = (L = []) \/ (!n. n < LENGTH L - 1 ==> R (EL n L) (EL (SUC n) L))``, Induct_on `L` THENL [ SIMP_TAC std_ss [SORTED_DEF], Cases_on `L` THEN FULL_SIMP_TAC list_ss [SORTED_DEF] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ Cases_on `n` THEN FULL_SIMP_TAC list_ss [], `R (EL 0 (h'::h::t)) (EL 0 (h::t))` by FULL_SIMP_TAC std_ss [] THEN FULL_SIMP_TAC list_ss [], `R (EL (SUC n) (h'::h::t)) (EL (SUC n) (h::t))` by FULL_SIMP_TAC std_ss [] THEN FULL_SIMP_TAC list_ss [] ] ] ) (******************************************************************************) (* Start proving the spec procedurewise. *) (******************************************************************************) val file = concat [examplesDir, "/vstte_2011/twowaysort.dsf"]; (* Print the source code to check wether the file can be found *) val _ = print_file_contents file; (* Parse program and start verifying the procedure "swap": holfoot_set_goal_procedures file ["swap"] This allows starting to write a tactic for "swap". This is very simple in the case of "swap". *) val swap_TAC = (*run automation with additional rewrite. That's sufficient!*) xHF_SOLVE_TAC [add_rewrites [SWAP_ELEMENTS_def]]; (* Proving "two_way_sort" is much more lengthy. holfoot_set_goal_procedures file ["two_way_sort"] *) val two_way_sort_TAC = (*run automation, this time for cases are left. 3 of these correspond to the verification of the loop invariant. One corresponds to the final proof after the loop is finished. *) xHF_SOLVE_TAC [add_rewrites [PERM_REFL], generate_vcs] THEN REPEAT STRIP_TAC THENL [ (* loop invariant: case a[i] = 0 *) HF_VC_TAC THEN REPEAT STRIP_TAC THEN Cases_on `n < i_const'` THENL [ FULL_SIMP_TAC std_ss [], `n = i_const'` by DECIDE_TAC THEN ASM_REWRITE_TAC[] ], (* loop invariant: case a[i] != 0 /\ a[j] = 1 *) HF_VC_TAC THEN REPEAT STRIP_TAC THEN Q.PAT_ASSUM `1:num = EL _ _` (ASSUME_TAC o GSYM) THEN Cases_on `j_const' < n` THENL [ FULL_SIMP_TAC std_ss [], `n = j_const'` by DECIDE_TAC THEN ASM_REWRITE_TAC[] ], (* loop invariant: case a[i] != 0 /\ a[j] != 1 *) Q.EXISTS_TAC `rdata` THEN Q.EXISTS_TAC `LENGTH rdata` THEN ASM_SIMP_TAC arith_ss [] THEN HF_SOLVE_TAC THEN HF_VC_TAC THEN FULL_SIMP_TAC arith_ss [EL_SWAP_ELEMENTS, LENGTH_SWAP_ELEMENTS] THEN REPEAT STRIP_TAC THENL [ `i_const' < LENGTH rdata` by DECIDE_TAC THEN `PERM rdata (SWAP_ELEMENTS j_const' i_const' rdata)` by (METIS_TAC [PERM_SWAP_ELEMENTS]) THEN METIS_TAC [PERM_TRANS, PERM_SYM], Cases_on `n = i_const'` THEN ASM_REWRITE_TAC[] THEN `MEM (EL j_const' rdata) data'` by METIS_TAC [MEM_EL, PERM_MEM_EQ] THEN `IS_BOOL_TO_NUM (EL j_const' rdata)` by FULL_SIMP_TAC std_ss [EVERY_MEM] THEN METIS_TAC [IS_BOOL_TO_NUM_REWRITE], Cases_on `n = i_const'` THENL [ `i_const' = j_const'` by DECIDE_TAC THEN `MEM (EL j_const' rdata) data'` by METIS_TAC [MEM_EL, PERM_MEM_EQ] THEN `IS_BOOL_TO_NUM (EL j_const' rdata)` by FULL_SIMP_TAC std_ss [EVERY_MEM] THEN METIS_TAC [IS_BOOL_TO_NUM_REWRITE], Cases_on `n = j_const'` THEN ASM_REWRITE_TAC[] THEN `i_const' < LENGTH rdata` by DECIDE_TAC THEN `MEM (EL i_const' rdata) data'` by METIS_TAC [MEM_EL, PERM_MEM_EQ] THEN `IS_BOOL_TO_NUM (EL i_const' rdata)` by FULL_SIMP_TAC std_ss [EVERY_MEM] THEN METIS_TAC [IS_BOOL_TO_NUM_REWRITE] ] ], (* After loop *) HF_VC_TAC THEN Q.EXISTS_TAC `data` THEN ASM_SIMP_TAC std_ss [PERM_REFL, SORTED_EL_DEF] THEN REPEAT STRIP_TAC THEN DISJ2_TAC THEN REPEAT STRIP_TAC THEN Cases_on `n < i_const` THEN ASM_SIMP_TAC arith_ss [] ] (* put everything together (3 s) *) val final_thm = holfoot_tac_verify_spec file NONE [("swap", swap_TAC), ("two_way_sort", two_way_sort_TAC)];