/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | tripleScript.sml | 12 TRIPLE (assert,model) pre code post = 13 FST post ==> FST pre /\ 14 SPEC model (assert (SND pre)) code (assert (SND post))` 84 `(!x. ~FST (post (F,x))) ==> 85 (!x. TRIPLE i (pre x) c (if g x then pre (f x) else post (d x))) ==> 86 (!x. TRIPLE i (pre x) c (post (TERM_TAILREC f g d x)))`, 150 `!x. case_sum pre post x = if ISL x then pre (OUTL x) else post (OUTR x)`, 154 `(!x. TRIPLE i (pre x) c (case_sum pre post (f x))) ==> 155 (!c x state. ~(FST (post ( [all...] |
H A D | tripleLib.sml | 68 fun abbrev_conv pat post = 70 then ALL_CONV post 72 then if pat = post 73 then ALL_CONV post 74 else ASSUME (mk_eq (post, add_prime pat)) 77 THENC RATOR_CONV (abbrev_conv (rator pat))) post 78 else if pat = post 79 then ALL_CONV post 80 else NO_CONV post
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | wpTools.sig | 14 (* The main tactics for reducing Leq pre (wlp prog post) *)
|
H A D | wpScript.sml | 1046 ``!cond body pre post. 1047 Leq pre (Cond cond (wlp body pre) post) ==> 1048 Leq pre (wlp (While cond body) post)``, 1065 ++ DISCH_THEN (MP_TAC o Q.SPEC `post`) 1068 (`expect_gfp (\e s. (if cond s then wlp body e s else post s))`, `g`) 1095 ``!pre mid post. 1096 Leq mid (wlp a post) /\ 1098 Leq pre (wlp (Assert pre a) post)``, 1104 ``!post. Leq Magic (wlp Abort post)``, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | temporalScript.sml | 29 val T_OR_F_def = Define `T_OR_F p post ^f ^seq = p ^f ^seq \/ 30 (EVENTUALLY (NOW post)) ^f ^seq` 33 SPEC_1 model pre code post err <=> 36 (T_OR_F (NEXT (EVENTUALLY (NOW post))) err))`; 44 `SPEC model pre code post <=> 45 TEMPORAL model code (T_IMPLIES (NOW pre) (EVENTUALLY (NOW post)))`, 82 ``SPEC_1 model pre code post err ==> 83 SPEC model pre code (post \/ err)``, 100 ``SPEC model pre code (post \/ err) ==> 105 ~SEP_REFINE (post * CODE_POO [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | straightlineLib.sml | 43 val post = th |> concl |> rand value 48 fun mk_new_post (post,tuple,new_tuple) = 50 if post = tuple then REFL post else ASSUME (mk_eq(post,new_tuple)) 52 val (lhs1,rhs1) = dest_pair post 63 val lemma = mk_new_post (post,tuple,new_tuple)
|
H A D | stack_analysisLib.sml | 29 fun get_updates pre post = let 31 val qs = list_dest dest_star post 50 val (_,pre,_,post) = dest_spec (concl th) 51 in (hyp th, pre, post) end 72 val (assum,pre,post) = get_assum_pre_post th 74 fun all_posts post = 75 if is_cond post then let 76 val (_,p1,p2) = dest_cond post 78 else [post] 79 in map (fn post [all...] |
H A D | graph_specsLib.sml | 118 (* make post into just state *) 120 val (_,_,_,post) = dest_spec (concl th) 121 fun fix_post_conv post = let 122 val ps = list_dest dest_star post 146 val goal = mk_eq(post,mk_star(mk_comb(rator state,new_s),pc)) 156 fun fix_if_post_conv post = 157 if is_cond post then BINOP_CONV fix_if_post_conv post 158 else fix_post_conv post 211 val (_,pre,_,post) 339 val post = th |> concl |> rand value [all...] |
H A D | straightlineScript.sml | 39 ``(c_post ==> SPEC model (assert p) code (assert post)) ==> 40 TRIPLE (assert,model) (pre,p) code (pre /\ c_post,post)``,
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_finalScript.sml | 41 fun SPEC_WEAKEN_RULE th post = let 42 val th = SPEC post (MATCH_MP progTheory.SPEC_WEAKEN th) 218 val post = ``SEP_EXISTS r3 dg g dm m dh h. aR 3w r3 * aSTRING r3 (sexp2string t1) value 222 val post = subst_SPEC_PC th post value 223 val (th,goal) = SPEC_WEAKEN_RULE th post 279 val post = ``SEP_EXISTS r3 dg g dm m dh h. pR 3w r3 * pSTRING r3 (sexp2string t1) value 283 val post = subst_SPEC_PC th post value 284 val (th,goal) = SPEC_WEAKEN_RULE th post 340 val post = ``xSTACK (esp-4w) [edi] * xR EDI edi * xR ESP (esp - 0x4w) * xPC (p + 0x1w)`` value 361 val post = ``xSTACK esp [w] * xR EDI w * xR ESP esp * xPC (p + 0x3w)`` value 382 val post = ``xSTACK esp [w] * xR EDI w * xR ESP (esp+4w) * xPC (p + 0x1w)`` value 399 val post = ``(let (eax,ecx,edi,esi,ebp,dh,h,df,f,dm,m,dg,g) = value 406 val post = subst_SPEC_PC th post value 429 val post = ``SEP_EXISTS edi dg g dm m dh h. xR EDI edi * xSTRING edi (sexp2string t1) value 433 val post = subst_SPEC_PC th post value 513 val post = subst_SPEC_PC th post value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | prog_ppcLib.sml | 67 val post = list_mk_star (map snd pre_post) ``:ppc_set -> bool`` value 80 val post = subst ss post value 82 in (pre,post) end; 167 val (pre,post) = ppc_pre_post g 168 val tm = ``SPEC PPC_MODEL pre {(p,c)} post`` 170 mk_var("post",type_of post) |-> post,
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sml | 934 As such, arm_CONFIG is not automatically introduced in the post-condition. 935 This is achieved with some post-processing. 1096 arm_spec_hex "E4921004"; (* LDR post imm *) 1097 arm_spec_hex "E4121004"; (* LDR post -imm *) 1098 arm_spec_hex "E6921002"; (* LDR post reg *) 1099 arm_spec_hex "E6121002"; (* LDR post -reg *) 1100 arm_spec_hex "E6121003"; (* LDR post -reg *) 1101 arm_spec_hex "E6921103"; (* LDR post reg *) 1110 arm_spec_hex "E6D21102"; (* LDRB reg post *) 1113 arm_spec_hex "E09210F3"; (* LDRSH reg post *) [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SolverSpec.sml | 14 executing it as a system command; calls 'post' (which is supposed to parse 19 (post : 'a -> string -> result) : Abbrev.goal -> result = 33 (* call 'post' to determine the result *) 34 val result = post x outfile
|
H A D | Z3.sml | 26 fun mk_Z3_fun name pre cmd_stem post goal = 29 SolverSpec.make_solver pre (file ^ cmd_stem) post goal
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | prog_x86Lib.sml | 85 val post = list_mk_star (map snd pre_post) ``:x86_set -> bool`` value 102 val post = subst ss post value 104 val post = mk_star (post,mk_comb(``xPC``,new_eip)) value 106 in (pre,post) end; 217 val (pre,post) = x86_pre_post g s 218 val tm = ``SPEC X86_MODEL pre {(eip,(c,w))} post`` 220 mk_var("post",type_of post) | [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | session.scala | 32 def post(a: A) 205 phase_changed.post(new_phase) 261 commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) 384 raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) 495 statistics.post(Session.Statistics(props)) 519 raw_output_messages.post(output) 535 raw_output_messages.post(output) 540 syslog_messages.post(output) 543 all_messages.post(output) 546 all_messages.post(inpu [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | session.scala | 32 def post(a: A) 205 phase_changed.post(new_phase) 261 commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) 384 raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) 495 statistics.post(Session.Statistics(props)) 519 raw_output_messages.post(output) 535 raw_output_messages.post(output) 540 syslog_messages.post(output) 543 all_messages.post(output) 546 all_messages.post(inpu [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | annotatedIR.sml | 57 | printtree(CALL(fname,pre,body,post,info),d) = 61 let val ir' = SC (pre, SC (body, post, info), info) 334 | rm_dummy_inst (CALL (fname,pre,body,post,info)) = 335 CALL (fname, rm_dummy_inst pre, rm_dummy_inst body, rm_dummy_inst post,info) 403 | get_annt (CALL(fname,pre,body,post,info)) = info 423 | apply_to_info (CALL(fname,pre,body,post,info)) f = CALL(fname, pre, body, post, f info) 441 | get_modified_regs (CALL(fname,pre,body,post,info)) = 478 | (CALL (fname,pre,body,post,info)) => 479 CALL(fname, pre, body, post, replace_in [all...] |
H A D | funCall.sml | 125 | visit (CALL(fname,pre,body,post,info)) = 126 CALL(fname, pre, body, post, adjust_info info) 149 (* Pre-call and post-call processing in compilance with the ARM Procedure Call standard *) 529 fun extract (CALL(fname, pre, body, post, outer_info)) = 530 (fname, pre, body, post, outer_info) 531 val (fname, pre, body, post, outer_info) = extract s2 535 fun convert_fcall (CALL(fname, pre, body, post, outer_info)) = 594 val post' = BLK ( 598 CALL(fname, pre' , body', post', outer_info)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Systeml.sig | 13 second is the name of the post-initialisation script to run. *)
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/examples/ |
H A D | verification.sml | 72 (``!post. wp (While (\s. T) Skip) post = Zero``, 89 (``!post. wlp (While (\s. T) Skip) post = Magic``,
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceSyntax.sml | 150 val (f,pre,prog,post) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 169 val (f,pre,prog,post) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 172 (p1, pL, f, pre, post) 177 val (f,pre,prog,post) = dest_VAR_RES_COND_HOARE_TRIPLE tt; 188 (p1', c_opt, f, pre, post, thm_fun)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | annotatedIR.sml | 47 | printtree(CALL(fname,pre,body,post,info),d) = 51 let val ir' = SC (pre, SC (body, post, info), info) 317 | rm_dummy_inst (CALL (fname,pre,body,post,info)) = 318 CALL (fname, rm_dummy_inst pre, rm_dummy_inst body, rm_dummy_inst post, info) 386 | get_annt (CALL(fname,pre,body,post,info)) = info 406 | apply_to_info (CALL(fname,pre,body,post,info)) f = CALL(fname, pre, body, post, f info) 423 | get_modified_regs (CALL(fname,pre,body,post,info)) = 453 | (CALL (fname,pre,body,post,info)) => 454 CALL(fname, pre, body, post, inf [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | annotatedIR.sml | 47 | printtree(CALL(fname,pre,body,post,info),d) = 51 let val ir' = SC (pre, SC (body, post, info), info) 317 | rm_dummy_inst (CALL (fname,pre,body,post,info)) = 318 CALL (fname, rm_dummy_inst pre, rm_dummy_inst body, rm_dummy_inst post, info) 386 | get_annt (CALL(fname,pre,body,post,info)) = info 406 | apply_to_info (CALL(fname,pre,body,post,info)) f = CALL(fname, pre, body, post, f info) 423 | get_modified_regs (CALL(fname,pre,body,post,info)) = 453 | (CALL (fname,pre,body,post,info)) => 454 CALL(fname, pre, body, post, inf [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_stepLib.sml | 1720 ("LoadWord (imm,post)", "FTFF_FFT________________"), 1723 ("LoadByte (imm,post)", "FTFF_TFT________________"), 1726 ("LoadWord (reg,post)", "FTTF_FFT_______________F"), 1729 ("LoadByte (reg,post)", "FTTF_TFT_______________F"), 1733 ("LoadHalf (reg,post)", "FFFF_FFT________FFFFT_TT"), 1734 ("LoadSignedByte (reg,post)", "FFFF_FFT________FFFFTTFT"), 1739 ("LoadHalf (imm,post)", "FFFF_TFT____________T_TT"), 1740 ("LoadSignedByte (imm,post)", "FFFF_TFT____________TTFT"), 1747 ("StoreWord (imm,post)", "FTFF_FFF________________"), 1750 ("StoreByte (imm,post)", "FTFF_TFF_______________ [all...] |