Speaking of reasoning, I believe a Hoare proof of correctness for a flowchart is * a choice of a precondition and postcondition, Pre(B) and Post(B), for every

Speaking of reasoning, I believe a Hoare proof of correctness for a flowchart is * a choice of a precondition and postcondition, Pre(B) and Post(B), for every basic block B * for every basic block B, a proof that {Pre(B)} B {Post(B)} * for every arrow a : B1 -> B2, a proof that Post(B1) /\ Cond => Pre(B2) where Cond is the condition for the arrow to be taken