Searched refs:guard (Results 1 - 25 of 75) sorted by relevance

123

/seL4-l4v-master/HOL4/examples/simple_complexity/loop/
H A DloopScript.sml41 loop_count_def |- !modify guard R. WF R ==> (!x. ~guard x ==> R (modify x) x) ==>
42 !x. loop_count guard modify x =
43 if guard x then 0 else SUC (loop_count guard modify (modify x))
44 loop_count_thm |- !modify guard R. WF R /\ (!x. ~guard x ==> R (modify x) x) ==>
45 !x. loop_count guard modify x =
46 if guard x then 0 else SUC (loop_count guard modif
[all...]
H A DloopListScript.sml474 Let guard = (\x. x = []),
477 and !x. ~guard x ==> (R (TL x) x) by LENGTH_TL_LT
478 Base: LENGTH [] = loop_count guard TL []
479 Note guard [] by notation
482 = loop_count guard modify [] by loop_count_0, guard []
483 Step: LENGTH x = loop_count guard TL x ==>
484 !h. LENGTH (h::x) = loop_count guard TL (h::x)
485 Note ~guard (h::x) by notation
488 = SUC (loop_count guard T
[all...]
H A DloopMultiplyScript.sml415 > loop_count_thm |> SPEC_ALL |> INST_TYPE [alpha |-> ``:num``] |> Q.INST [`modify` |-> `\x. b * x`, `guard` |-> `\x. x = 0 \/ m <= x`];
638 Let guard = (\x. x = 0 \/ m <= x),
641 The goal is: mop b m x = loop_count guard modify x
644 and !x. ~guard x ==> R (modify x) x by m - (b * x) < m - x, 1 < b, x <> 0
645 If guard x,
646 Then m <= x by guard x
649 = loop_count guard modify 0 by loop_count_0, guard x
650 If ~guard x,
651 Then ~(m <= x), or x < m by ~guard
[all...]
H A DloopIncreaseScript.sml387 > loop_count_thm |> SPEC_ALL |> INST_TYPE [alpha |-> ``:num``] |> Q.INST [`modify` |-> `\x. x + b`, `guard` |-> `\x. m <= x`];
564 Let guard = (\x. m <= x),
567 The goal is: bop b m x = loop_count guard modify x
570 and !x. ~guard x ==> R (modify x) x by m - (x + b) < m - x, 0 < b
571 If guard x,
572 Then m <= x by guard x
575 = loop_count guard modify 0 by loop_count_0, guard x
576 If ~guard x,
577 Then ~(m <= x), or x < m by ~guard
[all...]
H A DloopDecreaseScript.sml535 Let guard = (\x. x = 0),
538 The goal is: hop b x = loop_count guard modify x
541 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b
542 If guard x,
543 Then x = 0 by guard x
546 = loop_count guard modify 0 by loop_count_0, guard x
547 If ~guard x,
548 Then x <> 0 by ~guard x
551 = SUC (loop_count guard modif
[all...]
H A DloopDivideScript.sml643 Let guard = (\x. x = 0),
646 The goal is: pop b x = loop_count guard modify x
649 and !x. ~guard x ==> R (modify x) x by x DIV b < x, 1 < b
650 If guard x,
651 Then x = 0 by guard x
654 = loop_count guard modify 0 by loop_count_0, guard x
655 If ~guard x,
656 Then x <> 0 by ~guard x
659 = SUC (loop_count guard modif
[all...]
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/
H A Dstd_logicScript.sml22 Hoare (��s. P s ��� guard x s) p Q ���
23 Hoare (��s. P s ��� ~guard x s) q Q ���
27 (���s0. Hoare (��s. P s ��� guard x s ��� s = s0) p (��s. P s ��� R s s0)) ��� WF R ���
28 Hoare P (While x p) (��s. P s ��� ~guard x s))
H A Dstd_logic_completenessScript.sml13 (���s. P s ��� Inv s) ��� (���s. Inv s ��� ��guard x s ��� Q s) ���
14 (���s0. Hoare (��s. Inv s ��� guard x s ��� s = s0) p (��s. Inv s ��� m s < ((m s0):num))) ���
20 \\ qexists_tac �����s. Inv s ��� ��guard x s��� \\ fs []
27 NRC (��s t. guard f s ��� terminates s c t) k0 m t0 ���
28 NRC (��s t. guard f s ��� terminates s c t) k1 m t1 ���
29 ��guard f t0 ��� ��guard f t1 ���
74 \\ qexists_tac �����s. @n. ���t. NRC (��s t. guard f s ��� terminates s c t) n s t ��� ��guard f t���
90 \\ ������n. NRC (��s t. guard
[all...]
H A Ddiv_logicScript.sml33 Pohjola (��s. P s ��� guard x s) p D ���
34 Pohjola (��s. P s ��� ~guard x s) q D ���
41 guard x s ��� H 0 s ��� ignores_output H ���
44 (��s. H (i+1) s ��� output_of s = ev i ��� guard x s)) ���
50 (���s. P s ��� guard x s) ��� WF R ���
H A Dwhile_langScript.sml42 guard x ((s,out):state) = (x s ��� 0)
63 step (If x p q, s) ((if guard x s then p else q), s))
H A Ddiv_logic_completenessScript.sml17 guard f s ���
22 guard f s ���
52 ���ts. ts 0 = s ��� ���i. guard f (ts i) ��� terminates (ts i) c (ts (i+1)) ���
59 \\ qsuff_tac ������i. ���t. NRC (��x y. terminates x c y) i s t ��� guard f t ���
H A Ddiv_logic_soundnessScript.sml117 \\ ������i. ���t k. NRC (��s1 s2. terminates s1 p s2 ��� guard x s2) i s t ���
160 \\ qpat_x_assum ���guard x _��� mp_tac \\ simp []
179 \\ ������i. ���t. NRC (��s1 s2. terminates s1 p s2 ��� guard x s2) i s t ���
186 qhdtm_x_assum ���guard��� mp_tac >>
H A Dwhile_lang_lemmasScript.sml76 exec s (if guard x s then p else q) s1 ���
80 ~guard x s ���
84 guard x s ���
146 terminates s (if guard x s then p else q) t
311 ���n. NRC (��s t. guard f s ��� terminates s c t) n m t ��� ��guard f t
465 diverges s (If f p q) l = diverges s (if guard f s then p else q) l
/seL4-l4v-master/HOL4/examples/computability/register/
H A DrmRecursiveFuncsScript.sml85 loopguard guard step = <|
87 tf := (��s. if s=(npair 0 2) then (Dec guard (SOME step.q0) NONE)
90 In := [guard] ++ step.In;
110 (0,2) guard
112 Pr guard [i1...in]
161 guard s = <|
171 (* Assumption: ((guard, count), (accumulator, inputs))*)
203 (* TODO: new guard and count functions *)
204 (* Assumption: ((guard, count), (accumulator, inputs))*)
207 Pr_unary base step guard count
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dcond_cleanLib.sml16 val (guard,next1,next2) = dest_IF next value
17 in (guard,dest_ASM next1, dest_ASM next2) end
24 val (guard,asm1,asm2) = dest_IMPL_INST_IF_ASM_ASM th value
64 val (guard,_,(s2,u2,j2)) = dest_IMPL_INST_IF_ASM_ASM th value
68 val assum = negate_guard guard
75 val (guard,_,(s2,u2,j2)) = dest_IMPL_INST_IF_ASM_ASM th value
83 val (guard,(s1,u1,j1),_) = dest_IMPL_INST_IF_ASM_ASM th value
87 val assum = guard
94 val (guard,(s1,u1,j1),_) = dest_IMPL_INST_IF_ASM_ASM th value
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/
H A DtailrecScript.sml14 TAILREC_PRE f1 guard precondition (x:'a) ���
15 (!k. (!m. m < k ==> guard (FUNPOW f1 m x)) ���precondition (FUNPOW f1 k x)) ���
16 ���n. ~guard (FUNPOW f1 n x)`;
73 ``!step guard side.
74 (?R. WF R /\ !x. guard x ==> R (step x) x) /\ (!x. side x) ==>
75 !x. TAILREC_PRE step guard side x = T``,
/seL4-l4v-master/seL4/libsel4/include/sel4/
H A Ddeprecated.h117 typedef seL4_Word seL4_CapData_t SEL4_DEPRECATED("Badge and guard data are just seL4_Word type");
124 static inline SEL4_DEPRECATED("Use seL4_CNode_CapData_new().words[0]") seL4_Word seL4_CapData_Guard_new(seL4_Word guard, argument
127 return seL4_CNode_CapData_new(guard, bits).words[0];
/seL4-l4v-master/HOL4/src/monad/
H A Dmonadsyntax.sig30 guard : term option }
H A Dmonadsyntax.sml23 guard : term option }
29 fun toSexp {bind,ignorebind,unit,fail,choice,guard} =
33 Option (Option.map Term guard)]
42 fail = determOpt failopt, guard = determOpt guardopt,
407 val {bind,ignorebind,unit,fail,choice,guard} = getMI fname s
415 Option.app (fn g => ovl("assert", g)) guard
420 val {bind,ignorebind,unit,fail,choice,guard} = getMI fname s
428 Option.app (rmovl "assert") guard
504 guard = SOME (prim_mk_const {Name = "OPTION_GUARD", Thy = "option"}),
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dantiquote.scala26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dantiquote.scala26 "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
/seL4-l4v-master/seL4/src/kernel/
H A Dcspace.c129 word_t radixBits, guardBits, levelBits, guard; local
156 guard = (capptr >> ((n_bits - guardBits) & MASK(wordRadix))) & MASK(guardBits);
157 if (unlikely(guardBits > n_bits || guard != capGuard)) {
/seL4-l4v-master/HOL4/examples/STE/
H A DConversion.sml66 fun TrajForm (guard:term, n:string, value:term, START, END) =
69 ``((Is_1 ^node) WHEN (^value/\ ^guard))
71 ((Is_0 ^node) WHEN ~(^value /\ ^guard))``;
/seL4-l4v-master/HOL4/src/monad/more_monads/
H A DreaderMonadScript.sml88 ignorebind = NONE, choice = NONE, guard = NONE, fail = NONE
/seL4-l4v-master/seL4/manual/parts/
H A Dcspace.tex83 the original and a different guard (see
89 capability has the same badge and guard as the original.
330 also carries a \emph{guard} value, explained in
341 then compares that \obj{CNode}'s \emph{guard} value against the most
360 all levels, various guard and radix sizes and internal CNode
369 \item a top level CNode object with a 12-bit guard set to 0x000 and
427 \item[Cap A.] The first CNode has a 4-bit guard set to 0x0, and an
434 \item[Cap B.] Again, the first CNode has a 4-bit guard set to 0x0, and
436 It also has a 4-bit guard of 0x0 and Cap B resides at index
442 of the second CNode. The third CNode has no guard an
[all...]

Completed in 209 milliseconds

123