Hoare 論理によるプログラム検証入門
蓮尾 一郎
東京大学理学部情報科学科 講師
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro

1
Friday, July 1, 2011

（本当は）
情報科学科の宣伝

Hoare 論理によるプログラム検証入門
蓮尾 一郎
東京大学理学部情報科学科 講師
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro

1
Friday, July 1, 2011

プログラム検証：
最初の例
2
Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

3
Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;
}

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

Friday, July 1, 2011

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

ループ脱出！
( n>0 でない )Friday, July 1, 2011

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

03

While ループのあるプログラム
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}
N の階乗 N! を計算するプログラム
ループ脱出！
( n>0 でない )Friday, July 1, 2011

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

0
3

本当に？

4
Friday, July 1, 2011

本当に？
証明してみよう！

4
Friday, July 1, 2011

本当に？
証明してみよう！
数学的に厳密に4
Friday, July 1, 2011

本当に？
証明してみよう！
数学的に厳密にいろんなプログラムに使えるような，「スジのよい」方法で．できれば自動化

4
Friday, July 1, 2011

本当に？
証明してみよう！
数学的に厳密にいろんなプログラムに使えるような，「スジのよい」方法で．できれば自動化

4
Friday, July 1, 2011

本当に？
証明してみよう！
数学的に厳密にいろんなプログラムに使えるような，「スジのよい」方法で．できれば自動化プログラム検証 program veriﬁcation

4
Friday, July 1, 2011

本当に？
証明してみよう！
数学的に厳密にいろんなプログラムに使えるような，「スジのよい」方法で．できれば自動化プログラム検証 program veriﬁcation
プログラムや計算機システムの正しさは重要．
銀行，自動車，ロケット，セキュリティ，...
4
Friday, July 1, 2011

5
Friday, July 1, 2011

Ariane 5 打ち上げ失敗 (1996)

5
Friday, July 1, 2011

Ariane 5 打ち上げ失敗 (1996)

5
Friday, July 1, 2011

Ariane 5 打ち上げ失敗 (1996)

5
Friday, July 1, 2011

Ariane 5 打ち上げ失敗 (1996)

5
Friday, July 1, 2011

プログラム検証：「意味論的」証明
6
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}
N の階乗 N! を計算するプログラム
7
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

主張：
実行後の k の値は N!

N の階乗 N! を計算するプログラム
7
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

主張：
実行後の k の値は N!

困難：
ループが何度回るかわからない

N の階乗 N! を計算するプログラム
7
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

主張：

N の階乗 N! をアイデア：

計算するプログラム

ループの前後で保存される性質

実行後の k の値は N!

困難：
ループが何度回るかわからない（ループ不変量）に注目
7
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

8
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

k * (n!) = N!
8
Friday, July 1, 2011

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目
k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔
✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔
✔
✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔
✔
✔
✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N!
Friday, July 1, 2011

アイデア：
ループの前後で保存される性質（ループ不変量）に注目

✔
✔
✔
✔
✔
✔
✔

k

n

1

N

N

N-1

N*(N-1)

N-2

N*(N-1)*(N-2)

N-3

...

...

N*(N-1)*...*2

1

N*(N-1)*...*2*1

08

正しさの証明
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

ループ不変量：k * (n!) = N!
9
Friday, July 1, 2011

正しさの証明
補題１：
n := N; ループの前☺
k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N! は確かにループ不変量．
すなわち，☺で成り立てば☃でも成り立つ．

ループの後 ☃

ループ不変量：k * (n!) = N!
9
Friday, July 1, 2011

正しさの証明
補題１：
k * (n!) = N! は確かにループ不変量．

n := N; ループの前☺
すなわち，☺で成り立てば☃でも成り立つ．
k := 1;
while (n > 0) {k := k*n;証明：
n := n-1;
ループの前と後の k, n の値をそれぞれ}
ループの後 ☃

ループ不変量：k * (n!) = N!

kold，nold と knew，nnew と書くと，（仮定☺）

kold * (nold !) = N!

（示したいこと）

knew * (nnew !) = N!

いま，knew * (nnew !)= (kold * nold) * ( (nold - 1)! )[knew，nnewの定義より]= kold * (nold !)= N!
よって成立．
Friday, July 1, 2011

[仮定☺より]☐9

正しさの証明
補題１：
n := N; ループの前☺
k := 1;
while (n > 0) {k := k*n;n := n-1;}

k * (n!) = N! は確かにループ不変量．
すなわち，☺で成り立てば☃でも成り立つ．

ループの後 ☃

ループ不変量：k * (n!) = N!
10
Friday, July 1, 2011

正しさの証明
補題１：
n := N; ループの前☺
k := 1;
while (n > 0) {k := k*n;n := n-1;}
ループの後 ☃k * (n!) = N! は確かにループ不変量．
すなわち，☺で成り立てば☃でも成り立つ．

補題２：k * (n!) = N! はループに入る前☺で成立．

ループ不変量：k * (n!) = N!
10
Friday, July 1, 2011

正しさの証明
補題１：
n := N; ループの前☺
k := 1;
while (n > 0) {k := k*n;n := n-1;}
ループの後 ☃k * (n!) = N! は確かにループ不変量．
すなわち，☺で成り立てば☃でも成り立つ．

補題２：k * (n!) = N! はループに入る前☺で成立．

ループ不変量：証明：

k * (n!) = N!

n = N，k = 1 より明らか．

☐

10
Friday, July 1, 2011

正しさの証明
補題１：
n := N; ループの前☺
k := 1;
while (n > 0) {k := k*n;n := n-1;}
ループの後 ☃k * (n!) = N! は確かにループ不変量．
すなわち，☺で成り立てば☃でも成り立つ．

補題２：k * (n!) = N! はループに入る前☺で成立．

ループ不変量：プログラムの正しさの証明：

k * (n!) = N!

補題１，２より， k * (n!) = N! はループの実行前，実行中，実行後全てで成立．ループの実行後は n=0 なので，k = N! でなければならない． ☐Friday, July 1, 201111

証明の本質をとらえて，
「機械化」

12
Friday, July 1, 2011

証明の本質をとらえて，「機械化」
本質的な議論は単純？

12Friday, July 1, 2011

証明の本質をとらえて，「機械化」
本質的な議論は単純？
代入による値の書き換え

12
Friday, July 1, 2011

証明の本質をとらえて，「機械化」
本質的な議論は単純？
代入による値の書き換え
ループ不変量12
Friday, July 1, 2011

証明の本質をとらえて，「機械化」
本質的な議論は単純？
代入による値の書き換え
ループ不変量12
Friday, July 1, 2011

証明の本質をとらえて，「機械化」
本質的な議論は単純？
代入による値の書き換え
ループ不変量... Hoare logic!

12
Friday, July 1, 2011

Hoare 論理：
プログラムの正しさを証明する「機械」

13
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests

14
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系

14
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}14
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}
実行前に成り立つ性質“precondition”

プログラム

実行後に成り立つ性質“postcondition”
14

Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}
実行前に成り立つ性質“precondition”

プログラム{ n=2 } n:=n+1 { n=3 }例：

実行後に成り立つ性質“postcondition”
14

Friday, July 1, 2011

Hoare 論理の「材料」
プログラム意味論
プログラム ＝ メモリ状態の変換

メモリ状態の性質を記述するための assertion
language

Hoare triple を導くための導出規則 （ルール）
機械的な，文字列の書き換え
15
Friday, July 1, 2011

プログラム意味論

16
Friday, July 1, 2011

「意味論」とは？
プログラムの「意味」は何か
正確な答え：「実行した際の MacBook のメモ
リ状態の変化」➜ 細かすぎて「使えない」

n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

ここではメモリ状態を用いる
プログラミング言語による（宣言型言語だからメモリ状態を使う．たとえば関数型言語ならば関数として意味をつける）
17
Friday, July 1, 2011

メモリ状態
変数と値の対応の表のこと．


x
 y


�→
�
→
..
.



2
13 


数学的には： 関数
σ : Var −→ Z
Friday, July 1, 201118

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :

σ

�−→

�

σ x �→ �a�σ�

x は変数，a は「数の表現」（たとえば y+1）
Friday, July 1, 201119

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :プログラム x:=a の
「意味」

σ

�−→

�

σ x �→ �a�σ�

x は変数，a は「数の表現」（たとえば y+1）
Friday, July 1, 201119

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :プログラム x:=a の「意味」

x は変数，a は「数の表現」（たとえば y+1）
Friday, July 1, 2011σ�−→

メモリ状態，たとえば�

σ x �→ �a�σ

�



x →
�
2
 y →

�
13


..
.

19

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :プログラム x:=a の「意味」

x は変数，a は「数の表現」（たとえば y+1）
Friday, July 1, 2011

�→ ：「変形する」「移す」
��σ �−→ σ x �→ �a�σ

メモリ状態，
たとえば





x →
�
2
 y →

�
13


..
.

19

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :プログラム x:=a の「意味」

x は変数，a は「数の表現」（たとえば y+1）
Friday, July 1, 2011

�→ ：「変形する」「移す」
��σ �−→ σ x �→ �a�σ

アップデートされたメモリ状態．

メモリ状態，
たとえば

x の値を，a を σ のもとで計算し



x →
�
2
 y →

�
13


..
.

た値（たとえば�y + 1�σ = 14とか）にアップデート

19

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�P1 ; P2 � :

σ

�−→

�
�
�P2 � �P1 �σ

P1 ，P2 はプログラム

20
Friday, July 1, 2011

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�P1 ; P2 � :

σ

�−→

�
�
�P2 � �P1 �σ

まず P1 によって変換

P1 ，P2 はプログラム

20
Friday, July 1, 2011

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�P1 ; P2 � :P1 ，P2 はプログラム

σ

�−→

�
�
�P2 � �P1 �σ

まず P1 によって変換

次に P2 によって変換

20
Friday, July 1, 2011

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�if b then P1 else P2 � :�
�P1 �σ if �b�σ is trueσ �−→
�P2 �σ if �b�σ is false

P1 ，P2 はプログラムb は「真偽表現」（ x > 0 とか）21
Friday, July 1, 2011

プログラムの意味
MSt −→ MSt ∪ {⊥}�while b P � :σ�−→ ??

22
Friday, July 1, 2011

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�while b P � :σ�−→ ??

22
Friday, July 1, 2011

プログラムの意味
メモリ状態の変換として
つまり，関数 MSt −→ MSt ∪ {⊥}�while b P � :σ�−→ ??

状態変換の繰り返し �P �n σを考える：

σ, �P �σ,�P �(�P �σ),�P �(�P �(�P �σ)),

...

�
�
n
ある時点で b が偽になれば，つまり �b� �P � σ = false

なら，そうなるような最初の n に対する �P �n σ
を返す

b がずっと真であれば，（未定義，非停止）
22

Friday, July 1, 2011

プログラムの意味「停止しない」メモリ状態の変換として

つまり，関数 MSt −→ MSt ∪ {⊥}�while b P � :σ�−→ ??

状態変換の繰り返し �P �n σを考える：

σ, �P �σ,�P �(�P �σ),�P �(�P �(�P �σ)),

...

�
�
n
ある時点で b が偽になれば，つまり �b� �P � σ = false

なら，そうなるような最初の n に対する �P �n σ
を返す

b がずっと真であれば，（未定義，非停止）
22

Friday, July 1, 2011

プログラムの意味論：
まとめ「停止しない」メモリ状態の変換として

つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :

�P1 ; P2 � :

σ

�−→

σ

�−→

�

σ x �→ �a�σ��
�P2 � �P1 �σ�if b then P1 else P2 � :�
�P1 �σ if �b�σ is trueσ �−→
�P2 �σ if �b�σ is false�while b P � :Friday, July 1, 2011

σ

�−→

�

...
23

プログラムの意味論：
まとめ「停止しない」メモリ状態の変換として

つまり，関数 MSt −→ MSt ∪ {⊥}�x := a� :

�P1 ; P2 � :

σ

�−→

σ

�−→

�

σ x �→ �a�σ��
�P2 � �P1 �σ�if b then P1 else P2 � :�
�P1 �σ if �b�σ is trueσ �−→
�P2 �σ if �b�σ is false�while b P � :Friday, July 1, 2011

σ

�−→

�

ポイント：
数学的に厳密な定義...

要素還元的（大きなプログラムの意味は，その部品の意味から決まる） 23

Hoare 論理の「材料」（思い出そう）
プログラム意味論
プログラム ＝ メモリ状態の変換

メモリ状態の性質を記述するためのassertion language

Hoare triple を導くための導出規則
24
Friday, July 1, 2011

Assertion
Language
25
Friday, July 1, 2011

Assertion Language
Assertion: メモリ状態の性質を記述する「論理式」．例：
x=5

y≤3

z. ( x = 2 * z

y=3*z)

26
Friday, July 1, 2011

Assertion Language
Assertion: メモリ状態の性質を記述する「論理式」．例：
x=5

y≤3

z. ( x = 2 * z

y=3*z)

26
Friday, July 1, 2011

Assertion Language
Assertion: メモリ状態の性質を記述する「論理式」．例：
x=5

y≤3

z. ( x = 2 * z

y=3*z)

本当ならば，言語（文法）をはっきり定めることが望ましい．たとえば：AExp �
Fml �

a
A

::=
::=

x | n | a1 + a2 | a1 − a2 | a1 ∗ a2
true | false | A1 ∧ A2 | ¬A | a1 < a2 |∀x ∈ N. A
where x ∈ Var

とくに，証明の形式化・自動化のためには必須
ここではやらない（時間がないから）26
Friday, July 1, 2011

Hoare 論理の導出規則
27
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests

28
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系

28
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}28
Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}
実行前に成り立つ性質“precondition”

プログラム

実行後に成り立つ性質“postcondition”
28

Friday, July 1, 2011

Hoare 論理
Sir Antony Hoare(1934.1.11-)[Hoare, 1969]

Microsoft Research, Cambridge“Program logic” “Floyd-Hoare logic” とも呼ばれる．
関連： Dynamic logic, Kleene algebra with tests
Hoare triple を導いていく体系{A} P {B}
実行前に成り立つ性質“precondition”

プログラム{ n=2 } n:=n+1 { n=3 }例：

実行後に成り立つ性質“postcondition”
28

Friday, July 1, 2011

Hoare Triple の意味論

29
Friday, July 1, 2011

Hoare Triple の意味論
{A} P {B}29
Friday, July 1, 2011

Hoare Triple の意味論
実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}プログラム

29
Friday, July 1, 2011

Hoare Triple の意味論
実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}プログラム

「 {A} P {B} が真」であるとは，

29
Friday, July 1, 2011

Hoare Triple の意味論
実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}プログラム

「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σ
について，

29
Friday, July 1, 2011

Hoare Triple の意味論
実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}プログラム

「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，メモリ状態 [| P |]σ が assertion B をみたすことをいう．
Friday, July 1, 201129

Hoare Triple の意味論
実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}プログラム

「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，実行後のメモリ状態
メモリ状態 [| P |]σ が assertion B をみたすことをいう．
Friday, July 1, 201129

Partial Correctness{A} P {B}
「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，
メモリ状態 [| P |]σ が assertion B をみたすことをいう．

「

はすべての assertion をみたす」と約束．
➜ P が停止しないときに関しては，何も保証してくれな
い （“partial correctness”）
そもそも「P が停止するか？」はとても難しい問題．
決定不能！（判定してくれるプログラムは存在しない）

Friday, July 1, 201130

Partial Correctness{A} P {B}
「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，
メモリ状態 [| P |]σ が assertion B をみたすことをいう．

「

だったらどうする？
はすべての assertion をみたす」と約束．

➜ P が停止しないときに関しては，何も保証してくれな
い （“partial correctness”）
そもそも「P が停止するか？」はとても難しい問題．
決定不能！（判定してくれるプログラムは存在しない）
Friday, July 1, 201130

Partial Correctness{A} P {B}
「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，
メモリ状態 [| P |]σ が assertion B をみたすことをいう．

「

だったらどうする？
はすべての assertion をみたす」と約束．

➜ P が停止しないときに関しては，何も保証してくれな
い （“partial correctness”）
そもそも「P が停止するか？」はとても難しい問題．
決定不能！（判定してくれるプログラムは存在しない）
Friday, July 1, 201130

真な Hoare Triple の例{ x=2 } x:=x+1 { x=3 }{ x=2 } x:=x+1; y:=x { y=3 }{ } if x>0 then x:=x-1 else x:=0 { x≥0 }{ x>0 } while x>0 {y:=x} { x=x+1 }31
Friday, July 1, 2011

真な Hoare Triple の例{ x=2 } x:=x+1 { x=3 }{ x=2 } x:=x+1; y:=x { y=3 }{ } if x>0 then x:=x-1 else x:=0 { x≥0 }{ x>0 } while x>0 {y:=x} { x=x+1 }停止しないので

31
Friday, July 1, 2011

真な Hoare Triple の例{ x=2 } x:=x+1 { x=3 }{ x=2 } x:=x+1; y:=x { y=3 }{ } if x>0 then x:=x-1 else x:=0 { x≥0 }{ x>0 } while x>0 {y:=x} { x=x+1 }停止しないのでpostcondition が何であっても，この Hoare triple は真
31

Friday, July 1, 2011

Hoare 論理の導出規則{ A[a/x] } x:=a { A }(Assign)結論 { A[a/x] } x:=a { A } は，右から左に読むとよい．
「x:=a の後に A が成り立つためには，実行
前には A[a/x] が成り立たないといけない」
32
Friday, July 1, 2011

Hoare 論理の導出規則{ A[a/x] } x:=a { A }(Assign)

規則の名前（assignment = 「値の割り当て」）

結論 { A[a/x] } x:=a { A } は，右から左に読むとよい．
「x:=a の後に A が成り立つためには，実行
前には A[a/x] が成り立たないといけない」
32
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A[a/x] } x:=a { A }（この規則では仮定はなし）(Assign)

規則の名前（assignment = 「値の割り当て」）

結論 { A[a/x] } x:=a { A } は，右から左に読むとよい．
「x:=a の後に A が成り立つためには，実行
前には A[a/x] が成り立たないといけない」
32
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A[a/x] } x:=a { A }（この規則では仮定はなし）

assertion A において，変数 x を aに書き換えたもの(Assign)

規則の名前（assignment = 「値の割り当て」）

結論 { A[a/x] } x:=a { A } は，右から左に読むとよい．
「x:=a の後に A が成り立つためには，実行
前には A[a/x] が成り立たないといけない」
32
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A[a/x] } x:=a { A }（この規則では仮定はなし）

assertion A において，変数 x を aに書き換えたもの(Assign)

規則の名前（assignment = 「値の割り当て」）例：{ y=2 } x:=y { x=2 }{ k*((n-1)!)=N!

{ x-1=2 } x:=x-1 { x=2 }n-1≥0 } n:=n-1 { k*(n!)=N!

n≥0 }
33

Friday, July 1, 2011

Hoare 論理の導出規則{ A } P1 { C }{ C } P2 { B }{ A } P1; P2 { B }(SeqComp)（もう一回言っておく）次のように読む．
規則は上から下に（上が成り立てば下が成り立つ）

証明を探すときは逆（下が成り立つためには，どんな上が成り立てばいい？）
Hoare triple は右から左に（postcondition が成り立つためには．．．）
34
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A } P1 { C }{ C } P2 { B }{ A } P1; P2 { B }(SeqComp)（もう一回言っておく）次のように読む．
規則は上から下に（上が成り立てば下が成り立つ）

証明を探すときは逆（下が成り立つためには，どんな上が成り立てばいい？）
Hoare triple は右から左に（postcondition が成り立つためには．．．）
34
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A } P1 { C }{ C } P2 { B }(SeqComp){ A } P1; P2 { B }規則の名前（sequential composition =「逐次合成」）（もう一回言っておく）次のように読む．
規則は上から下に（上が成り立てば下が成り立つ）

証明を探すときは逆（下が成り立つためには，どんな上が成り立てばいい？）
Hoare triple は右から左に（postcondition が成り立つためには．．．）
34
Friday, July 1, 2011

Hoare 論理の導出規則
規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ A } P1 { C }{ C } P2 { B }{ A } P1; P2 { B }(SeqComp)

規則の名前（sequential composition =「逐次合成」）

例：(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp){ x-1=2 } x:=y; y:=y-1 { y=2 }35
Friday, July 1, 2011

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

考えの流れ

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

考えの流れ

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

考えの流れ

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

考えの流れ

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

さっきの例，くわしく！！
(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 1:「実行後に y=2 になってほしんだけど．．．」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 2:「y:=y-1 の前には y-1=2であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }(SeqComp)

Step 3:「さらに x:=y の前には
x-1=2 であればいいぞ」{ x-1=2 } x:=y; y:=y-1 { y=2 }(Assign)(Assign){ x-1=2 } x:=y { y-1=2 }{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }Friday, July 1, 2011

考えの流れ

(SeqComp)

Step 4:「x-1=2 であるためのprecondition，わかった！」36

Hoare 論理の導出規則{ A } P1 { C }規則の読み方：「上の仮定が成立していれば，下の結論も成立」{ C } P2 { B }(SeqComp){ A } P1; P2 { B }規則の名前（sequential composition =「逐次合成」）

例：{

k*n*((n-1)!)=N!
n-1≥0{
Friday, July 1, 2011}

k:=k*n{k*n*((n-1)!)=N!
n-1≥0

} {
{
}

k*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

}

k:=k*n;n:=n-1}n:=n-1{k*(n!)=N!

n≥0(SeqComp)}

k*(n!)=N!
n≥037

Hoare 論理の導出規則{ A b } P1 { B }{ A ¬b } P2 { B }{ A } if b then P1 else P2 { B }

(If)

例：
{ x≥0

x>0 } x:=x-1 { x≥0 }{ x≥0¬ (x>0)} x:=x { x≥0 }(If){ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }38
Friday, July 1, 2011

Hoare 論理の導出規則{Ab } P1 { A }{ A } while b P1 { A¬b }(While)例：{ x≥0x>0} x:=x-1 { x≥0 }{ x≥0 } while x>0 ( x:=x-1 ) { x≥0(While)¬(x>0) }39

Friday, July 1, 2011

Hoare 論理の導出規則
A はループ不変量！

{Ab } P1 { A }{ A } while b P1 { A¬b }(While)例：{ x≥0x>0} x:=x-1 { x≥0 }{ x≥0 } while x>0 ( x:=x-1 ) { x≥0(While)¬(x>0) }39

Friday, July 1, 2011

Hoare 論理の導出規則
A はループ不変量！

{Ab } P1 { A }{ A } while b P1 { A¬b }(While)ループを脱出した ➜b は成立しないはず

例：
{ x≥0

x>0} x:=x-1 { x≥0 }{ x≥0 } while x>0 ( x:=x-1 ) { x≥0(While)¬(x>0) }39

Friday, July 1, 2011

Hoare 論理の導出規則
A はループ不変量！

{Ab } P1 { A }{ A } while b P1 { A¬b }(While)ループを脱出した ➜b は成立しないはず例：{{
Friday, July 1, 2011

k*(n!)=N!
n>0

k*(n!) = N!

}}

k:=k*n;n:=n-1
while (n>0)
k:=k*n;n:=n-1{{k*(n!)=N!

k*(n!)=N!
n=0}}(While)40

Hoare 論理の導出規則
A Aʼ

{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}

例：
x>0

( x≥0

x>0 )

{ x≥0

x>0} x:=x-1 { x≥0 }(Conseq){ x>0 } x:=x-1 { x≥0 }41
Friday, July 1, 2011

Hoare 論理の導出規則
A Aʼ

{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}
規則の名前（consequence =「（論理的）帰結」）

例：
x>0

( x≥0

x>0 )

{ x≥0

x>0} x:=x-1 { x≥0 }(Conseq){ x>0 } x:=x-1 { x≥0 }41
Friday, July 1, 2011

Hoare 論理の導出規則
A Aʼ

{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}
規則の名前（consequence =「（論理的）帰結」）

仮定： 「A が成り立てば，必ず Aʼ も
成り立つ」

例：
x>0

( x≥0

x>0 )

{ x≥0

x>0} x:=x-1 { x≥0 }(Conseq){ x>0 } x:=x-1 { x≥0 }41
Friday, July 1, 2011

Hoare 論理の導出規則{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}

A Aʼ

規則の名前
（consequence =「（論理的）帰結」）

仮定： 「A が成り立てば，必ず Aʼ も成り立つ」

k*(n!)=N!
n>0

k*(n!)=N!

{

k*n*((n-1)!)=N!
n-1≥0{
Friday, July 1, 2011

k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n>0

}

}

k:=k*n;n:=n-1k:=k*n;n:=n-1{k*(n!)=N!
n≥0

{

n≥0

}

k*(n!)=N!

k*(n!)=N!

}(Conseq)
42

Hoare 論理の導出規則（まとめ）{ A[a/x] } x:=a { A }{ A } P1 { C }(Assign){ C } P2 { B }{ A } P1; P2 { B }{ A b } P1 { B }(SeqComp){ A ¬b } P2 { B }{ A } if b then P1 else P2 { B }{Ab } P1 { A }{ A } while b P1 { A

¬b }

(If)

(While)43

Friday, July 1, 2011

Hoare 論理の導出規則（まとめ，つづき）
A Aʼ

{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}44
Friday, July 1, 2011

Hoare 論理における導出
45Friday, July 1, 2011

Hoare 論理の導出
たとえば，次の Hoare triple を証明したい．

{

k=1

n=N

}

while (n>0)

「意味論的立場」「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，
メモリ状態 [| P |]σ が assertion B をみたすことを
いう

．
直接の証明

「数学の証明」，
頭を使う．
➜ 自動化できない！
Friday, July 1, 2011

k:=k*n;n:=n-1{

k = N!

}「構文論的立場」
Hoare 論理の導出規則を繰り返し使って，仮定なしの「導出木」（「証明木」）
が作れればOK！
記号操作，証明「検索」➜ 自動化！
46

Hoare 論理の導出

x≥0(Assign)x>0{ x-1≥0 } x:=x-1 { x≥0 }x-1≥0(Conseq)

{

x≥0
x>0

} x:=x-1 { x≥0 }x≥0¬ (x>0)x≥0(Assign){ x≥0 } x:=x { x≥0 }x≥0(Conseq){ ¬ (x>0) } x:=x { x≥0 }(If){ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }47
Friday, July 1, 2011

Hoare 論理の導出木！！
（導出木，証明木）
x≥0(Assign)x>0{ x-1≥0 } x:=x-1 { x≥0 }x-1≥0(Conseq)

{

x≥0
x>0

} x:=x-1 { x≥0 }x≥0¬ (x>0)x≥0(Assign){ x≥0 } x:=x { x≥0 }x≥0(Conseq){ ¬ (x>0) } x:=x { x≥0 }(If){ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }48
Friday, July 1, 2011

Hoare 論理の導出
たとえば，次の Hoare triple を証明したい．

{

k=1

n=N

}

while (n>0)

「意味論的立場」「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，
メモリ状態 [| P |]σ が assertion B をみたすことを
いう

．
直接の証明

「数学の証明」，
頭を使う．
➜ 自動化できない！
Friday, July 1, 2011

k:=k*n;n:=n-1{

k = N!

}「構文論的立場」
Hoare 論理の導出規則を繰り返し使って，仮定なしの「導出木」（「証明木」）
が作れればOK！
記号操作，証明「検索」➜ 自動化！
49

健全性，完全性
意味論と構文論のせめぎあい！！
（導出規則＝構文論＝「機械」）
健全性 soundness: 導出規則で導かれる Hoare triple は，すべて真「ウソは言わない」「証明能力が高すぎない」
この性質は必須．（ウソをつかれると困る）
完全性 completeness: 真であるHoare triple は，すべて導出規則で導ける「真なことはすべて言ってくれる」「証明能力が十分高い」
これは成り立たない場合も多い（仕方ない．不完全性定理）

50
Friday, July 1, 2011

健全性，完全性
Hoare 論理は健全性を満たす．
相対完全性 relative completeness を満たす．
相対完全性 ＝ 「条件付き」完全性
条件付きでない，フルの完全性は，
Gödel の不完全性定理により排除される．
51
Friday, July 1, 2011

例： 階乗の計算

52
Friday, July 1, 2011

はじめの例n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

主張：
実行後の k の値は N!

N の階乗 N! を計算するプログラム
53
Friday, July 1, 2011

はじめの例n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

主張：
実行後の k の値は N!

この証明を，Hoare 論理を使ってシステマティックに！

N の階乗 N! を（構文論的・機械的な，記号書き計算するプログラム

換えによる証明）

53
Friday, July 1, 2011

Hoare 論理による証明
目標： 次の Hoare triple の導出

{

k=1

n=N

}

while (n>0)
k:=k*n;n:=n-1{

k = N!

}

54
Friday, July 1, 2011

Hoare 論理による証明(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

k*n*((n-1)!)=N!
n-1≥0

} {
} {
{
}
{
k:=k*nk*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

k*n*((n-1)!)=N!
n-1≥0

{
k=1

(Assign)k*(n!)=N!
n≥0n>0

k:=k*n;k*(n!)=N!

n:=n-1

n≥0

n≥0

{
{

Friday, July 1, 2011n≥0
(SeqComp)}(Conseq)}

k*(n!) = N!

n≥0

k=1

{

}

{

k:=k*n;n:=n-1k*(n!)=N!
n≥0

}

n=N

k*(n!) = N!

}n:=n-1k*(n!)=N!

n=N}

while (n>0)
k:=k*n;n:=n-1}{k*(n!)=N!

while (n>0)
k:=k*n;n:=n-1n≥0¬(n>0)}{(While)k*(n!)=N!

n≥0
k=N!

k = N!

}¬(n>0)(Conseq)

55

Hoare 論理による証明(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

k*n*((n-1)!)=N!
n-1≥0

} {
} {
{
}
{
k:=k*nk*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

k*n*((n-1)!)=N!
n-1≥0

{
k=1

(Assign)k*(n!)=N!
n≥0n>0

k:=k*n;k*(n!)=N!

n:=n-1

n≥0

n≥0

{
{

Friday, July 1, 2011n≥0
(SeqComp)}(Conseq)}

k*(n!) = N!

n≥0

k=1

{

}

{

k:=k*n;n:=n-1k*(n!)=N!
n≥0

}

n=N

k*(n!) = N!

}n:=n-1k*(n!)=N!

n=N}

while (n>0)
k:=k*n;n:=n-1}{k*(n!)=N!

while (n>0)
k:=k*n;n:=n-1n≥0¬(n>0)}{(While)k*(n!)=N!

n≥0
k=N!

k = N!

}¬(n>0)(Conseq)56

最初にやった数学的証明の「形式化」（エッセンスは同じ）

Hoare 論理による証明(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

k*n*((n-1)!)=N!
n-1≥0

} {
} {
{
}
{
k:=k*nk*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

k*n*((n-1)!)=N!
n-1≥0

{
k=1

(Assign)k*(n!)=N!
n≥0n>0

k:=k*n;k*(n!)=N!

n:=n-1

n≥0

n≥0

{
{

Friday, July 1, 2011n≥0
(SeqComp)}(Conseq)}

k*(n!) = N!

n≥0

k=1

{

}

{

k:=k*n;n:=n-1k*(n!)=N!
n≥0

}

n=N

k*(n!) = N!

}n:=n-1k*(n!)=N!

n=N}

while (n>0)
k:=k*n;n:=n-1}{k*(n!)=N!

while (n>0)
k:=k*n;n:=n-1n≥0¬(n>0)}{(While)k*(n!)=N!

n≥0
k=N!

k = N!

}¬(n>0)(Conseq)56

最初にやった数学的証明の「形式化」（エッセンスは同じ）

Hoare 論理による証明(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

k*n*((n-1)!)=N!
n-1≥0

} {
} {
{
}
{
k:=k*nk*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

k*n*((n-1)!)=N!
n-1≥0

{
k=1

(Assign)k*(n!)=N!
n≥0n>0

k:=k*n;k*(n!)=N!

n:=n-1

n≥0

n≥0

{
{

Friday, July 1, 2011n≥0
(SeqComp)}(Conseq)}

k*(n!) = N!

n≥0

k=1

{

}

{

k:=k*n;n:=n-1k*(n!)=N!
n≥0

ループ不変量！

}n=N

k*(n!) = N!

}n:=n-1k*(n!)=N!

n=N}

while (n>0)
k:=k*n;n:=n-1}{k*(n!)=N!

while (n>0)
k:=k*n;n:=n-1n≥0¬(n>0)}{(While)k*(n!)=N!

n≥0
k=N!

k = N!

}¬(n>0)(Conseq)56

（頭を使わずに，規則を見てパターンマッチングでできるぞ．．．）

最初にやった数学的証明の「形式化」（エッセンスは同じ）

Hoare 論理による証明(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

k*n*((n-1)!)=N!
n-1≥0

} {
} {
{
}
{
k:=k*nk*((n-1)!)=N!

k*((n-1)!)=N!

n-1≥0

n-1≥0

k*n*((n-1)!)=N!
n-1≥0

{
k=1

(Assign)k*(n!)=N!
n≥0n>0

k:=k*n;k*(n!)=N!

n:=n-1

n≥0

n≥0

{
{

Friday, July 1, 2011n≥0
(SeqComp)}(Conseq)}

k*(n!) = N!

n≥0

k=1

{

}

{

k:=k*n;n:=n-1k*(n!)=N!
n≥0

ループ不変量！

}n=N

k*(n!) = N!

}n:=n-1k*(n!)=N!

n=N}

while (n>0)
k:=k*n;n:=n-1}{k*(n!)=N!

while (n>0)
k:=k*n;n:=n-1n≥0¬(n>0)}{(While)k*(n!)=N!

n≥0
k=N!

k = N!

}¬(n>0)(Conseq)

56

参考文献

G. Winskel, The Formal Semantics ofProgramming Languages: An Introduction.
The MIT Press, ISBN 0-262-23169-7

57
Friday, July 1, 2011

自己紹介

58
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）

59
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）
京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）

59
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）
京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）
専門分野： 数学と計算機科学を行ったり来たり
理学部情報科学科での立ち位置：

59
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）
京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）
専門分野： 数学と計算機科学を行ったり来たり
理学部情報科学科での立ち位置：
応用 vs. 理論

59
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）
京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）
専門分野： 数学と計算機科学を行ったり来たり
理学部情報科学科での立ち位置：
応用 vs. 理論
速度 vs. 正しさ

59
Friday, July 1, 2011

蓮尾 一郎 （はすお・いちろう）
BSc（東大数学，2002）
MSc（東工大情報，2004）
PhD（U. Nijmegen, 2008）
京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）
専門分野： 数学と計算機科学を行ったり来たり
理学部情報科学科での立ち位置：
応用 vs. 理論
速度 vs. 正しさ
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro
59
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学

60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学

既存の手法
60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学

数学的な定式化「数学的本質」
を見極める

既存の手法
60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的

数学的な定式化「数学的本質」
を見極める

既存の手法
60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法

新たな手法
60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法

新たな手法

非決定的システム
60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的Kleisli 圏での余代数

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法

新たな手法

非決定的システム
60
Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的Kleisli 圏での余代数

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム

新たな手法
確率的システム60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
抽象的，一般的Kleisli 圏での余代数

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算新たな手法
確率的システム60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
Kleisli 圏での余代数

抽象的，一般的

Geometry of Interaction

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算新たな手法
確率的システム60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
Kleisli 圏での余代数

抽象的，一般的

Geometry of Interaction

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算新たな手法
確率的システム
量子計算
60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
Kleisli 圏での余代数

抽象的，一般的

Geometry of Interaction

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算離散的システム

新たな手法
確率的システム
量子計算
60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
Kleisli 圏での余代数

抽象的，一般的

Geometry of Interaction
Hoare 論理 ＋ 超準解析

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算離散的システム

新たな手法
確率的システム
量子計算
60

Friday, July 1, 2011

研究テーマ
抽象数学をつかって，情報科学の新パラダイ
ムに斬り込む特に： 圏論，数理論理学，代数学，幾何学
Kleisli 圏での余代数

抽象的，一般的

Geometry of Interaction
Hoare 論理 ＋ 超準解析

数学的な定式化「数学的本質」

パラメータを変

を見極める

えて具体化

既存の手法
非決定的システム
ふつうの計算離散的システム

新たな手法
確率的システム

ハイブリッドシステム
量子計算
60

Friday, July 1, 2011

メッセージ
情報科学と数学のインタラクション，おもしろいよ！

61
Friday, July 1, 2011

メッセージ
情報科学と数学のインタラクション，おもしろいよ！
そもそもコンピュータは数学（数学基礎論）から生まれた

61
Friday, July 1, 2011

お待ちかね：
レポート課題62
Friday, July 1, 2011

レポート課題
1. 次の４つの Hoare triple について，真であるかど
うか判定せよ．（証明・反例があればなおよい）{ x=3 } x:=y { y=3 }{ y=2 } x:=y+1; y:=x { x=3 }{ } if x≥0 then x:=x-1 else x:=0 { x≥0 }
y:=0; x:=X;{ X≥0 }

while (x>100) {y:=y+1;{

0≤x<100 ∧100*y + x = X}

x:=x-100}
Friday, July 1, 201163

レポート課題
1. 次の４つの Hoare triple について，真であるかど
うか判定せよ．（証明・反例があればなおよい）{ x=3 } x:=y { y=3 }{ y=2 } x:=y+1; y:=x { x=3 }{ } if x≥0 then x:=x-1 else x:=0 { x≥0 }
y:=0; x:=X;{ X≥0 }

while (x>100) {y:=y+1;
x:=x-100}

Friday, July 1, 2011{0≤x<100 ∧100*y + x = X}

気持ち： X セントを「y ドル x セント」に変換するプログラム 63

レポート課題
2. 次の2つのHoare triple に対して，
Hoare 論理の導出木を与えよ．ただし x,
n,m は整数(int)型の変数とする．
{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }{ m (m≥0n=2*m) } while (n>0) { n:=n-2} { n=0 }64
Friday, July 1, 2011

レポート課題
2. 次の2つのHoare triple に対して，
Hoare 論理の導出木を与えよ．ただし x,
n,m は整数(int)型の変数とする．
{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }ヒント： 38 ページのルールの適用（まだ仮定が残ってる！）
を完成させる．

{ m (m≥0n=2*m) } while (n>0) { n:=n-2} { n=0 }64
Friday, July 1, 2011

レポート課題
2. 次の2つのHoare triple に対して，
Hoare 論理の導出木を与えよ．ただし x,
n,m は整数(int)型の変数とする．
{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }ヒント： 38 ページのルールの適用（まだ仮定が残ってる！）
を完成させる．

{ m (m≥0n=2*m) } while (n>0) { n:=n-2} { n=0 }「n は負でない偶数」
64
Friday, July 1, 2011

レポート課題
3. [Hoare 論理とは関係ない算数の問題]
２つの正の整数 m, n （ただし m > n）について，GCD(m, n) = GCD(m - n, n)であることを示せ．ただし，GCD(m, n) は
m と n の最大公約数を表す．

65
Friday, July 1, 2011

レポート課題
4. 正の整数X, Y の最大公約数を計算するための，次のプ
ログラム P を考える（ユークリッドの互除法）．

x:=X; y:=Y;
while (x≠y) {if x≥ythen x:=x-yelse y:=y-x}
次の Hoare triple の，Hoare 論理における導出木を与
えよ．

{ X>0
Friday, July 1, 2011Y>0 } P { x=y=GCD(X,Y) }66

レポート課題
4. 正の整数X, Y の最大公約数を計算するための，次のプ
ログラム P を考える（ユークリッドの互除法）．
ヒント：

x:=X; y:=Y;
while (x≠y) {if x≥ythen x:=x-yelse y:=y-x}• 55ページを参考に．
• レポート課題の問題３を使う．

• ループ不変量は，
x>0 y>0
GCD(x,y)=GCD(X,Y)

次の Hoare triple の，Hoare 論理における導出木を与
えよ．

{ X>0
Friday, July 1, 2011Y>0 } P { x=y=GCD(X,Y) }

66

念のため
全問解かなくても大丈夫だが，たくさん解いたほうがよい（当たり前）

コピーはダメ！
東北大学 小林直樹先生のページを参照
http://www.kb.ecei.tohoku.ac.jp/~koba/report.html

盗作と判断された場合には，深刻な結果に至る場
合があります．
たとえば，法学部では一発退学
67
Friday, July 1, 2011