HoareCore

📁 Source: MRiscX/Hoare/HoareCore.lean

Statistics

Metric	Count
Definitions Assertion, And, Not, hoare_triple_up, hoare_triple_up_1, weak	6
Theorems	0
Total	6

Assertion

Definitions

Name	Category	Theorems
And 📖	CompOp	—
Not 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Assertion 📖	CompOp	—
hoare_triple_up 📖	MathDef	9 math math: S_LOOP, BL_TO_WL, WL_TO_BL, BL_SUBSET, S_COND, POST_WEAK, S_SEQ', PRE_STR, S_SEQ
hoare_triple_up_1 📖	MathDef	28 math math: specification_AddRegister, specification_JumpNeqZero_false, specification_Jump', specification_AddImmediate, specification_JumpNeq_true, specification_LoadWordImmediate, specification_LoadWordReg, specification_XOR, specification_JumpLe_true, specification_LoadImmediate, specification_XorImmediate, specification_JumpEq_true, specification_Increment, specification_JumpGt_true, specification_JumpNeq_false, specification_StoreWordImmediate, specification_Decrement, specification_CopyRegister, specification_LoadAddress, specification_JumpEqZero_true, specification_JumpEqZero_false, specification_SubRegister, specification_JumpNeqZero_true, specification_JumpGt_false, specification_Jump, specification_JumpEq_false, specification_JumpLe_false, specification_SubImmediate
weak 📖	MathDef	2 math math: weak_with_less_BL_weakens, weak_L_w_with_L_from_L_b

---

← Back to Index