Searched refs:post (Results 1 - 25 of 109) sorted by relevance

12345

/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DtripleScript.sml12 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 DtripleLib.sml68 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 DwpTools.sig14 (* The main tactics for reducing Leq pre (wlp prog post) *)
H A DwpScript.sml1046 ``!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 DtemporalScript.sml29 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 DstraightlineLib.sml43 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 Dstack_analysisLib.sml29 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 Dgraph_specsLib.sml118 (* 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 DstraightlineScript.sml39 ``(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 Dlisp_finalScript.sml41 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 Dprog_ppcLib.sml67 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 Darm_progLib.sml934 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 DSolverSpec.sml14 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 DZ3.sml26 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 Dprog_x86Lib.sml85 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 Dsession.scala32 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 Dsession.scala32 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 DannotatedIR.sml57 | 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 DfunCall.sml125 | 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 DSysteml.sig13 second is the name of the post-initialisation script to run. *)
/seL4-l4v-10.1.1/HOL4/examples/pgcl/examples/
H A Dverification.sml72 (``!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 Dvars_as_resourceSyntax.sml150 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 DannotatedIR.sml47 | 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 DannotatedIR.sml47 | 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 Darm_stepLib.sml1720 ("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...]

Completed in 172 milliseconds

12345