Hoare logicとは - わかりやすく解説 Weblio辞書

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

ホーア論理

(Hoare logic から転送)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/21 02:23 UTC 版)

ナビゲーションに移動検索に移動

この記事の正確性に疑問が呈されています。問題箇所に信頼できる情報源を示して、記事の改善にご協力ください。議論はノートを参照してください。（2016年4月）
疑問点：トリプルの定義からすでに通常の定義と異なっている。例もおかしい

ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。

プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法^[1]を基に、計算機科学者のアントニー・ホーアによって提案された^[2]。

概要

ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に関する規則、ポインタに関する規則などがある。

定義

部分的正当性（partial correctness）

事前条件（precondition） P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件（postcondition） Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して部分的に正当（partially correct）であると言い^[3]、

P { S } Q

と記述する^[4]。ホーアによる元々の記法は上記のものであるが、一般的にはプログラム S の部分正当性は、

{ P } S { Q }

と記述されることが多い^[5]^[6]。

正当性（correctness）

事前条件 P が成り立つときに、プログラム S を実行すると、その実行が必ず終了するならば、プログラム S は、事前条件 P に関して停止する（terminate）と言う^[7]。

プログラム S が部分的に正当かつ停止するものであるとき、すなわち、プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという^[8]。

部分的正当性の証明体系

(A1) 代入文の公理

{ Q[e/x] } x:＝e { Q }

ここで、事前条件の Q[e/x] は置換であり、式 Q の中に出現するすべての x を式 e で置き換えた式を表す。一方で事後条件の Q は代入文実行後（置換ではなく代入を行ったあとの）x の値について式 Q が成り立つことを表す^[9]。

したがって、この公理は、

{ Q[e/x] }：式 Q 中の全ての x を e に置換するとき式 Q が成り立つのであれば、
x:=e：（置換で成り立つならば、ほぼ同じような代入操作でも変わらないはずのため）式 Q 中の x の値を代入 x:=e で変更することで、
{ Q }：（置換の場合は成り立っているのであるから x の値が e に変更されたのであれば当然に）代入文実行後の式 Q は成り立つ、

というように読む^[10]。

(A2) 空文の公理

空文（skip文）は、プログラムの状態を変化させないが、これを表すのが空文の公理である。skip以前に真であったことはそのまま真となる。

{ P } skip { P }

(R1) 複合文の規則

一般に順序的プログラムは機能ごとに分解することができるが、その逆として分解した手続きは複合文として合成することができる。以下の複合文の規則は分解したプログラムが中間条件 R を介することで元の機能に合成されることを表している^[11]。

{ P } `S1` { R } , { R } `S2` { Q }
{ P } `S1 ; S2` { Q }

(R2) if文の規則

{ P ∧ B } `S1` { Q } , { P ∧ ¬B } `S2` { Q }
{ P } `If B Then S1 else S2 End` { Q }

{ P ∧ B } `S1` { Q } , P ∧ ¬B => Q
{ P } `If B Then S1 End` { Q }

(R3) while文の規則

{ P ∧ B } `S1` { P }
{ P } `While B Do S1 End` { P ∧ ¬B }

ここで、P はループ不変条件である^[12]。

(R4) 帰結の規則

P => P₁ , { P₁ } `S` { Q₁ } , Q₁ => Q
{ P } `S` { Q }

例

例 1
$\{x+1=43\}\!$	$\ y:=x+1\ \!$	$\{y=43\}\!$	（代入の公理）
			$(x+1=43\Leftrightarrow x=42)$
$\{x=42\}\!$	$\ y:=x+1\ \!$	$\{y=43\land x=42\}\!$	（結果規則）
例 2
$\{x+1\leq N\}\!$	$\ x:=x+1\ \!$	$\{x\leq N\}\ \!$	（代入の公理）
			（ $x<N\implies x+1\leq N$ ここで x と N は整数型）
$\{x<N\}\!$	$\ x:=x+1\ \!$	$\{x\leq N\}\ \!$	（結果規則）

脚注

^ Floyd(1967)
^ Hoare(1969)
このような経緯から、フロイド−ホーア論理（Floyd-Hoare Logic）とも呼ばれる。荒木・張(2002) p.23
^ 荒木・張(2002) p.7
^ これをホーアの三つ組（Hoare triple）と呼ぶこともある。
^ これは、ホーアの共同研究者であったニクラウス・ヴィルトが開発したプログラミング言語のPascalのコメント記法に由来していると考えられる。系統的(1986)
^ 部分的正当性に関するホーア論理では、プログラムの完了を示すことができない。もしプログラム S が完了しなければ事後条件の Q は意味を成さない。そのような事情から事後条件 Q を偽の値である false とすることで完了しないプログラムを
{ P } S { false }
と表すこともある。
^ 荒木・張(2002) p.7
^ 荒木・張(2002) p.7
^ 荒木・張(2002) p.7
^
正しい Triple の例:
- $\{x+1=43\}\ y:=x+1\ \{y=43\}\!$
- $\{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!$
ホーアが提案した代入の公理は、複数の（変項の）名前が（メモリ上の）同じ格納値を参照している場合に「正しくない」。例えば、以下の例で x と y が同じ値を参照している場合
$\{A\}\ x:=2\ \{y=3\}$
この Triple は真ではない。なぜなら、 x に 2 を代入した後では y が 3 となるような事後状態は存在しないからである。
^ 例えば、次の2つの代入を考えてみよう。
$\{x+1=43\}\ y:=x+1\ \{y=43\}$

$\{y=43\}\ z:=y\ \{z=43\}$
合成規則を適用すると、これらは次のようになる:
$\{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}$
^ なお、完全正当性のための While 規則としては以下のようになる。
${\frac {<\;{\textrm {is\ well-founded,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P]\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ [\neg B\wedge P]}}\!$
この規則では、ループ不変条件が保持されるだけでなく、ループが終了することを証明するためにループ変化条件（英語版） t を加えている。t は整礎関係 (well-founded relation) の観点でループの反復ごとに厳密に減少していく値である。なお不変条件 P が与えられたとき、条件 B は t がその範囲の極小元でないことを暗に示さなければならず、さもなくば事前条件は偽となる。関係 "<" は整礎なので、ループの各ステップで有限鎖（英語版）の元が減少していくことでカウントされる。また、ここで波括弧ではなく角括弧が使われているのは完全正当性を示すためであり、部分正当性のみならず完了も示す（これは、完全正当性の数ある記法の1つである）。

参考文献

Robert D. Tennent: "Specifying Software" (ホーア論理を紹介している最近の教科書) ISBN 0-521-00401-2
荒木啓二郎, 張漢明『プログラム仕様記述論』オーム社〈IT Text〉、2002年。
林晋『プログラム検証論』共立出版〈情報数学講座〉、1995年。
木村泉, 米澤明憲『算法表現論』岩波書店〈岩波講座情報科学〉、1982年。
R. W. Floyd (1967), “Assigning meanings to programs”, Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19: 19–31
C. A. R. Hoare (1969), “An axiomatic basis for computer programming”, Communications of the ACM 12(10): 576-580,583, doi:10.1145/363235.363259
N. Wirth『系統的プログラミング入門』野下浩平, 筧捷彦, 武市正人訳、近代科学社、1986年、第２版補訂。
ロバート B. アンダスン『演習プログラムの証明』有澤誠訳、近代科学社〈ソフトウェア工学ライブラリ〉、1980年。

KeY-Hoare - KeY という定理証明機上に構築された半自動検証システムで、ホーア論理を散りいれている。
j-Algo-modul Hoare calculus — アルゴリズム視覚化プログラム j-Algo におけるホーア論理視覚化モジュール

Weblio日本語例文用例辞書

索引トップ用語の索引ランキング

「Hoare logic」の例文・使い方・用例・文例

【学術名】 logic, music, rhetoric.

Weblio日本語例文用例辞書はプログラムで機械的に例文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。

>> 「Hoare logic」を含む用語の索引
Hoare logicのページへのリンク


	All text is available under the terms of the GNU Free Documentation License. この記事は、ウィキペディアのホーア論理 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。
TANAKA Corpus	Tanaka Corpusのコンテンツは、特に明示されている場合を除いて、次のライセンスに従います： Creative Commons Attribution (CC-BY) 2.0 France.
京大-NICT 日英中基本文データ	この対訳データはCreative Commons Attribution 3.0 Unportedでライセンスされています。
	Copyright © 1995-2025 Hamajima Shoten, Publishers. All rights reserved.
	Copyright © Benesse Holdings, Inc. All rights reserved.
	Copyright (c) 1995-2025 Kenkyusha Co., Ltd. All rights reserved.
	日本語ワードネット1.1版 (C) 情報通信研究機構, 2009-2010 License All rights reserved. WordNet 3.0 Copyright 2006 by Princeton University. All rights reserved. License
	Copyright (C) 1994- Nichigai Associates, Inc., All rights reserved. 「斎藤和英大辞典」斎藤秀三郎著、日外アソシエーツ辞書編集部編
	This page uses the JMdict dictionary files. These files are the property of the Electronic Dictionary Research and Development Group, and are used in conformance with the Group's licence.

Hoare logicとは？わかりやすく解説

ホーア論理

目次

概要