Hoare Logic Coq definitions crib sheet

Notation
Definition
Name of definition (if any)

state -> Prop assertion

total_map nat
state
P ->> Q forall st, P st -> Q st assert_implies
P <<->> Q P ->> Q /\ Q ->> P
{{ P }}  c  {{ Q }} forall st st', c / st \\ st' -> P st -> Q st' hoare_triple
P [ X |-> a ] fun (st:state) => P (t_update st X (aeval st a)) assn_sub

Web Accessibility