(* $Header: /users/lal/black/hol/Disser/RCS/partialInf.sml,v 1.28 1997/05/28 22:14:08 black Exp $ *) (* *created "Thu Oct 26 16:02:50 1995" *by "Paul E. Black" *) (* *modified "Wed May 28 16:12:02 1997" *by "Paul E. Black" *) (*----------------------------------------------------------------------- C inference rules for partial correctness rules after Mike Gordon and Peter Homeier -----------------------------------------------------------------------*) system "/bin/rm partialInf.thms"; new_theory "partialInf"; new_parent "semeq"; add_theorems_to_sml "semeq"; new_parent "wellformed"; use "utilities.sml"; (* for LIFT_QUANT_RULE *) (*----------------------------------------------------------------------- C axiom schemas -----------------------------------------------------------------------*) (* Declare equivalence between a C boolean expression and a HOL bool expr *) val IS_VALUE = new_definition ( "IS_VALUE", (--`! (cexpr:CExpr) (holexpr:bool). IS_VALUE cexpr holexpr = T`--) ); (*----------------------------------------------------------------------- Define how to specialize varargs in formals. -----------------------------------------------------------------------*) new_constant{Name = "specialize_varargs", Ty = ==`:Cvar list->ParamList->Cvar list`==}; (*----------------------------------------------------------------------- Define how to do substitutions in a predicate. c <| [a/b] (Meaning: replace every b in c with the corresponding a) is written as SUBS c a b Note: the sense of the replacement is opposite that of SUBSE. -----------------------------------------------------------------------*) new_constant{Name = "SUBS", Ty = ==`:bool->Cvar list->Cvar list->bool`==}; (*----------------------------------------------------------------------- Define how to do substitutions in a predicate with expressions. c <| [x := e] (Meaning: replace every x in c with the corresponding e) is written as SUBSE c x e Note: the sense of the replacement is opposite that of SUBS. -----------------------------------------------------------------------*) new_constant{Name = "SUBSE", Ty = ==`:bool->Cvar list->CExpr list->bool`==}; (*----------------------------------------------------------------------- Define how to do substitution of an array with an expression. c <| a[i] := e (Meaning: replace a in c with a new function having the value e at location i) is written as SUBSAE c a i e -----------------------------------------------------------------------*) new_constant{Name = "SUBSAE", Ty = ==`:bool->Cvar->CExpr->CExpr->bool`==}; (*----------------------------------------------------------------------- Define how to universally quantify a predicate over a list of variables, similar to !x.post. For example, UNIVQUANT [(Var "x"),(Var "y")] x/\y/\z yields \x1 y1.x1 /\ y1 /\ z -----------------------------------------------------------------------*) new_constant{Name = "UNIVQUANT", Ty = ==`:Cvar list->bool->bool`==}; (*---------------------------------------------------------------- rules of inference for partial correctness ----------------------------------------------------------------*) load_library {lib = find_library "ind_def" , theory = "-"}; local val ParType = (--`Partial:bool->CStmt->bool->bool`--) in val {desc=Partial_rules, induction_thm=Partial_ind} = Inductive_def.new_inductive_definition { name = "Partial", patt = ((--`^ParType pre stm post`--), []), fixity = Prefix, rules = [ {(* expressions without side effects *) side_conditions = [(--`specpost = SUBSE post [c_result] [e]`--), (--`NoSE e`--)], hypotheses = [], (*----------------------------------------*) conclusion = (--`^ParType specpost (Simple e) post`--)}, {(* expressions with side effects *) (* SKIMP - this should specify some SUBS-like relation between pre and post *) side_conditions = [(--`NoSE (Lval l)`--)], hypotheses = [], (*----------------------------------------*) conclusion = (--`^ParType pre (Simple (LUnary op l)) post`--)}, {(* simple Assignment *) side_conditions = [(--`specpost = SUBSE post [x] [e]`--), (--`NoSE e`--)], hypotheses = [], (*----------------------------------------*) conclusion = (--`^ParType specpost (Simple (Assign (Vref x) e)) post`--)}, {(* assignment to arrays *) side_conditions = [(--`specpost = SUBSAE post a i e`--), (--`NoSE i`--), (--`NoSE e`--)], hypotheses = [], (*----------------------------------------*) conclusion = (--`^ParType specpost (Simple(Assign(Aryref a i) e)) post`--)}, {(* Semantic equivalence *) side_conditions = [(--`SEM_EQ stm1 stm2`--)], hypotheses = [ (--`^ParType pre stm1 post`--)], (*----------------------------------------*) conclusion = (--`^ParType pre stm2 post`--)}, {(* Sequence Rule *) side_conditions = [], hypotheses = [ (--`^ParType pre1 stm1 interim`--), (--`^ParType interim stm2 post2`--)], (*----------------------------------------*) conclusion = (--`^ParType pre1 (Seq stm1 stm2) post2`--)}, {(* Precondition strengthening *) side_conditions = [(--`stronger ==> pre`--)], hypotheses = [ (--`^ParType pre stm post`--)], (*----------------------------------------*) conclusion = (--`^ParType stronger stm post`--)}, {(* Postcondition weakening *) side_conditions = [(--`post ==> weaker`--)], hypotheses = [ (--`^ParType pre stm post`--)], (*----------------------------------------*) conclusion = (--`^ParType pre stm weaker`--)}, {(* Specification conjunction *) side_conditions = [], hypotheses = [ (--`^ParType pre1 stm post1`--), (--`^ParType pre2 stm post2`--)], (*----------------------------------------*) conclusion = (--`^ParType (pre1 /\ pre2) stm (post1 /\ post2)`--)}, {(* Specification disjunction *) side_conditions = [], hypotheses = [ (--`^ParType pre1 stm post1`--), (--`^ParType pre2 stm post2`--)], (*----------------------------------------*) conclusion = (--`^ParType (pre1 \/ pre2) stm (post1 \/ post2)`--)}, {(* Empty Statement Axiom *) side_conditions = [], hypotheses = [], (*----------------------------------------*) conclusion = (--`^ParType pre EmptyStmt pre`--)}, {(* Two-armed Conditional (if...then...else) *) side_conditions = [(--`IS_VALUE expr test`--)], hypotheses = [ (--`^ParType (pre /\ test) stm1 post`--), (--`^ParType (pre /\ ~test) stm2 post`--)], (*----------------------------------------*) conclusion = (--`^ParType pre (IfElse expr stm1 stm2) post`--)}, {(* While (backward jump) *) side_conditions = [(--`SEM_EQ (Seq preTest (Seq (Simple testExpr) postTest)) (Simple expr)`--), (--`NoPostSE preSeEx`--), (* NoSE testExpr implied by IS_VALUE testExpr *) (--`NoPreSE postSeEx`--), (--`(preTest = EmptyStmt) \/ (preTest = (Simple preSeEx))`--), (--`(postTest = EmptyStmt) \/ (postTest=(Simple postSeEx))`--), (--`IS_VALUE testExpr test`--)], hypotheses = [ (--`^ParType invariant preTest testState`--), (--`^ParType (testState /\ test) postTest bodyCond`--), (--`^ParType bodyCond stm invariant`--), (--`^ParType (testState /\ ~test) postTest post`--)], (*----------------------------------------*) conclusion = (--`^ParType invariant (CWhile expr stm) post`--)}, {(* Blocks optionally with local variables *) side_conditions = [], (* SKIMP - this should handle local variables *) hypotheses = [ (--`^ParType pre stm post`--)], (*----------------------------------------*) conclusion = (--`^ParType pre (Block llv stm) post`--)}, (* we need the rule of adaptation, too *) {(* Function calls *) side_conditions = [], hypotheses = [ (--`WF_fnp pre (Func name vvals globls b) post`--), (--`WF_c (Simple (Call name ps))`--), (* expand varargs *) (--`vals = specialize_varargs vvals ps`--), (--`vals' = variants vals (APPEND (FV_a qpost) globls)`--), (--`y = APPEND (vals:Cvar list) globls`--), (* u = vals' since there is no call-by-name in C *) (* v = vals since there is no call-by-name in C *) (--`x = APPEND (vals':Cvar list) globls`--), (--`x0 = logicals x`--), (--`y0 = logicals y`--), (--`x0' = variants x0 (FV_a qpost)`--), (--`specpost = SUBS post (APPEND vals' x0') (APPEND vals y0)`--), (--`postimpq = SUBS (specpost ==> qpost) newC_Result genrC_Result`--), (--`univpost = SUBS (UNIVQUANT x postimpq) x x0'`--), (--`specpre = SUBS pre vals' vals`--), (--`newpre = SUBSE (specpre /\ univpost) vals' (PL2CEL ps)`--)], (*----------------------------------------*) conclusion = (--`^ParType newpre (Simple (Call name ps)) qpost`--)} ]} end; val c = ref 1; save_thm("Simple_nse_rule", LIFT_QUANT_RULE (el (!c) Partial_rules));c:=(!c)+1; save_thm("Side_effect_rule",LIFT_QUANT_RULE (el (!c) Partial_rules));c:=(!c)+1; save_thm("Assign_vref_rule", LIFT_QUANT_RULE (el (!c)Partial_rules));c:=(!c)+1; save_thm("Assign_aryref_rule",LIFT_QUANT_RULE(el (!c)Partial_rules));c:=(!c)+1; val Sem_equiv_rule = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("Sem_equiv_rule", Sem_equiv_rule); save_thm("Sequence_rule", LIFT_QUANT_RULE (el (!c) Partial_rules)); c:=(!c)+1; val Pre_strengthen_rule = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("Pre_strengthen_rule", Pre_strengthen_rule); val Post_weaken_rule = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("Post_weaken_rule", Post_weaken_rule); save_thm("Conjunction_rule", el (!c) Partial_rules); c:=(!c)+1; save_thm("Disjunction_rule", el (!c) Partial_rules); c:=(!c)+1; val SKIP_AX = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("SKIP_AX", SKIP_AX); val IfThenElse_rule = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("IfThenElse_rule", IfThenElse_rule); val basic_While_rule = LIFT_QUANT_RULE (el (!c) Partial_rules); c:=(!c)+1; save_thm("Block_rule", LIFT_QUANT_RULE (el (!c) Partial_rules)); c:=(!c)+1; save_thm("Call_rule", LIFT_QUANT_RULE (el (!c) Partial_rules)); c:=(!c)+1; (*--------------------------------------------------------------------------- Derived theorems ---------------------------------------------------------------------------*) (*-------------------- Prove Associativity of Seq --------------------------*) val Seq_semantic_assoc2 = ONCE_REWRITE_RULE [SEM_EQ_SYM] Seq_semantic_assoc; val Sequence_assoc1 = prove ( (--`!pre stm1 stm2 stm3 post. Partial pre (Seq(Seq stm1 stm2)stm3) post ==> Partial pre (Seq stm1(Seq stm2 stm3)) post`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC Sem_equiv_rule THEN EXISTS_TAC (--`Seq(Seq stm1 stm2)stm3`--) THEN ASM_REWRITE_TAC [Seq_semantic_assoc] ); save_thm("Sequence_assoc1", Sequence_assoc1); val Sequence_assoc2 = prove ( (--`!pre stm1 stm2 stm3 post. Partial pre(Seq stm1(Seq stm2 stm3))post ==> Partial pre(Seq(Seq stm1 stm2)stm3)post`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC Sem_equiv_rule THEN EXISTS_TAC (--`Seq stm1(Seq stm2 stm3)`--) THEN ASM_REWRITE_TAC [Seq_semantic_assoc2] ); save_thm("Sequence_assoc2", Sequence_assoc2); (* this isn't needed, but it seems useful *) val SEQ_ASSOC = prove ( (--`!pre stm1 stm2 stm3 post. Partial pre(Seq stm1(Seq stm2 stm3))post = Partial pre(Seq(Seq stm1 stm2)stm3)post`--), REPEAT GEN_TAC THEN EQ_TAC THENL [ ACCEPT_TAC (SPEC_ALL Sequence_assoc2), ACCEPT_TAC (SPEC_ALL Sequence_assoc1) ] ); (*----------------------- prove one armed conditional ----------------------*) save_thm("IfThen_rule", prove ( (--`!expr pre code post test. IS_VALUE expr test /\ Partial (pre /\ test) code post /\ (pre /\ ~test ==> post) ==> Partial pre (If expr code) post`--), REPEAT STRIP_TAC THEN (* change it into the semantically equivalent ... *) MATCH_MP_TAC Sem_equiv_rule THEN (* ... two armed conditional and ... *) EXISTS_TAC (--`IfElse expr code EmptyStmt`--) THEN (* ... establish that they are the same (by axiom) *) REWRITE_TAC [IfElse_EQ_If] THEN (* reduce the two armed conditional to its hypotheses, ... *) MATCH_MP_TAC IfThenElse_rule THEN (* ... state the test, and prove most of the hypotheses. *) EXISTS_TAC (--`test:bool`--) THEN ASM_REWRITE_TAC [] THEN (* change precondition of "pre /\ ~test" ... *) MATCH_MP_TAC Pre_strengthen_rule THEN (* ... into post and match it with |- Partial post Empty post *) EXISTS_TAC (--`post:bool`--) THEN ASM_REWRITE_TAC [SKIP_AX] )); (*---------------------------------------------------------------------------- Prove a general while with built-in postcondition weakening. The post weakening makes it easier to use in a tactic: the tactic can leave an implication subgoal if the computed postcondition doesn't match the goal. ----------------------------------------------------------------------------*) save_thm("While_rule", prove ( (--`!invariant stm postCond expr preTest testState test postTest bodyCond testExpr preSeEx postSeEx post. Partial invariant preTest testState /\ Partial (testState /\ test) postTest bodyCond /\ Partial bodyCond stm invariant /\ Partial (testState /\ ~test) postTest postCond /\ SEM_EQ (Seq preTest (Seq (Simple testExpr) postTest)) (Simple expr) /\ NoPostSE preSeEx /\ NoPreSE postSeEx /\ ((preTest = EmptyStmt) \/ (preTest = Simple preSeEx)) /\ ((postTest = EmptyStmt) \/ (postTest = Simple postSeEx)) /\ IS_VALUE testExpr test /\ (postCond ==> post) ==> Partial invariant (CWhile expr stm) post`--), REPEAT STRIP_TAC THEN (* weaken the postcondition to "interim /\ ~test" *) MATCH_MP_TAC Post_weaken_rule THEN EXISTS_TAC (--`postCond:bool`--) THEN (* finish off the "postCond ==> post" part *) ASM_REWRITE_TAC [] THEN (* replace with the conditions of the basic rule *) MATCH_MP_TAC basic_While_rule THEN (* instantiate all variables *) MAP_EVERY EXISTS_TAC [(--`preTest:CStmt`--),(--`testState:bool`--), (--`test:bool`--),(--`postTest:CStmt`--),(--`bodyCond:bool`--), (--`testExpr:CExpr`--),(--`preSeEx:CExpr`--),(--`postSeEx:CExpr`--)] (* finish using all those assumptions *) THEN ASM_REWRITE_TAC [] )); close_theory(); export_theory(); (* end of $Source: /users/lal/black/hol/Disser/RCS/partialInf.sml,v $ *)