Let C be a line, or sequence of lines, in a computer program, and let P and Q be logical predicates such that if P is true before C is executed then Q will necessarily be true after C is executed. Then the following expression
is an expression in Hoare logic, also known as a Hoare triple. Note that if C does not terminate, then there is no "after", so Q can be any statement at all.
See also:
Search Encyclopedia

Featured Article
