I assume you read http://en.wikipedia.org/wiki/Hoare_logic http://en.wikipedia.org/wiki/Hoare_logic ? Basically, the (relevant) state of the computation is rep

I assume you read http://en.wikipedia.org/wiki/Hoare_logic http://en.wikipedia.org/wiki/Hoare_logic ? Basically, the (relevant) state of the computation is represented as a set of logical propositions which are true before a statement, and a set of logical propositions which are true after the statement. For each kind of statement the language supports (`if` statements, `while` statements, etc.) there are natural ways to reason about those triples. Do you understand the "While rule" on the link above? I can explain it in natural language, but I'd rather not expend the effort if it's not something you've already seen.