WBLogic.persistent_pred

WBLogic.oneshot

WBLogic.program_logic.ghost_stacks

WBLogic.program_logic.weakestpre

• Derived rules

WBLogic.program_logic.lifting

WBLogic.program_logic.adequacy

WBLogic.program_logic.lib.sts

WBLogic.heap_lang.primitive_laws

WBLogic.heap_lang.derived_laws

• Rules for allocation
• Rules for accessing array elements

WBLogic.heap_lang.proofmode

WBLogic.heap_lang.adequacy

WBLogic.heap_lang_examples.awkward

WBLogic.heap_lang_examples.very_awkward

WBLogic.heap_lang_examples.sts.very_awkward

WBLogic.F_mu_ref.base

WBLogic.F_mu_ref.lang

WBLogic.F_mu_ref.wp_rules

WBLogic.F_mu_ref.typing

WBLogic.F_mu_ref.unary.logrel

WBLogic.F_mu_ref.unary.fundamental

WBLogic.F_mu_ref.unary.soundness

WBLogic.F_mu_ref.unary.examples.very_awkward

WBLogic.F_mu_ref.binary.rules

WBLogic.F_mu_ref.binary.logrel

WBLogic.F_mu_ref.binary.fundamental

WBLogic.F_mu_ref.binary.context_refinement

WBLogic.F_mu_ref.binary.soundness

WBLogic.F_mu_ref.binary.examples.fact

WBLogic.F_mu_ref.binary.examples.very_awkward

WBLogic.heap_lang_trace.lang

WBLogic.heap_lang_trace.tactics

WBLogic.heap_lang_trace.notation

WBLogic.heap_lang_trace.class_instances

• Instances of the Atomic class
• Instances of the PureExec class

WBLogic.heap_lang_trace.trace_resources

WBLogic.heap_lang_trace.primitive_laws

WBLogic.heap_lang_trace.derived_laws

• Rules for allocation
• Rules for accessing array elements

WBLogic.heap_lang_trace.proofmode

WBLogic.heap_lang_trace.adequacy

WBLogic.heap_lang_trace_examples.very_awkward

• • Proof that the very awkward example specification guarantees

WBLogic.heap_lang_trace_examples.sequential_trace_alt