2018.5.42

We redefine Hoare triples ``$\{P\}~c~\{Q\}${P} c {Q}’’ to mean that, whenever $c$c is started in a state satisfying $P$P, and terminates with result $r$r, then KaTeX parse error: Undefined control sequence: \norm at position 3: r=\̲n̲o̲r̲m̲{\sigma} (and hence KaTeX parse error: Undefined control sequence: \err at position 7: r\not=\̲e̲r̲r̲) where the state $\sigma$σ satisfies $Q$Q.