| 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 |