ホーア論理
事前条件(precondition) P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件(postcondition) Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して部分的に正当(partially correct)であると言い、
P { S } Q
と記述する。ホーアによる元々の記法は上記のものであるが、一般的にはプログラム S の部分正当性は、
{ P } S { Q }
と記述されることが多い。
事前条件 P が成り立つときに、プログラム S を実行すると、その実行が必ず終了するならば、プログラム S は、事前条件 P に関して停止する(terminate)と言う。
プログラム S が部分的に正当かつ停止するものであるとき、すなわち、プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当(correct)であるという。