Hoare logic

Hoare logic(Q1375924) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. The key idea is that this logic enables rule composition that can capture errors at the primitive level.