Hoare Logic

A logic for verifying the correctness of programs. Separation Logic combines a form of Bunched Logic with Hoare triples.

Hoare Triples

A Hoare triple consists of a precondition P, a command (program) C, and a postcondition Q:

{P} C {Q}

Q. What is the meaning of a Hoare triple {P} C {Q}?

A. When the precondition P is met, executing C will establish Q

Q. What does a Hoare triple consist of?

A. A precondition, command (program), and a postcondition