本文へスキップ

ホアとは?

ほあ

チャールズ・アントニー・リチャード・ホアは、クイックソートの発明プログラム検証のホア論理で知られるイギリスの計算機科学者です。

チャールズ・アントニー・リチャード・ホア(Charles Antony Richard Hoare、通称C.A.R. Hoare、1934年生まれ)は、イギリスの計算機科学者で、オックスフォード大学やマイクロソフトリサーチで長年活躍しました。

ホアの最も広く知られた業績の一つは、1959〜60年ごろに考案したクイックソートアルゴリズムです。ピボット基準配列を分割して再帰的にソートする手法で、平均計算量O(n log n)を持ち、今日でも実用上最も使われるソートアルゴリズムの一つです。

また、プログラムの正しさを論理的に証明するための枠組み「ホア論理(Hoare Logic)」を1969年に提案したことでも知られます。事前条件・事後条件・不変条件を用いてプログラムの振る舞いを仕様化する手法であり、形式検証・ソフトウェア工学の理論的基盤となっています。さらに、並行プロセスの記述言語CSP(Communicating Sequential Processes)を考案し、並行プログラミングの理論にも貢献しました。

1980年にチューリング賞を受賞し、アルゴリズム・プログラム検証・並行計算の三分野を横断した功績が評価されています。

使い方・例文

プログラミングの授業でソートアルゴリズムを学ぶ際、最も教科書的な高速ソート法としてホアが考案したクイックソートが最初に取り上げられます。

この用語をシェア

𝕏 でポスト LINE

最終更新:

関連用語