ホーア論理

ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。