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

Hoare 論理によるプログラム検証入門

プログラム検証：
最初の例

蓮尾 一郎
東京大学理学部情報科学科 講師

http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro

12

While ループのある本当に？

プログラム

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

証明してみよう！

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*10

プログラム検証 program veriﬁcation
プログラムや計算機システムの正しさは重要．
銀行，自動車，ロケット，セキュリティ，...
34

Ariane 5 打ち上げ失敗 (1996)

プログラム検証：「意味論的」証明
5

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

主張：

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

計算するプログラム

6

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

実行後の k の値は N!

困難：
ループが何度回るかわからないk * (n!) = N!

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

7

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

!
!
!
!
!
!
!

kn1

N

N

N-1

N*(N-1)

N-2

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

N-3

...

...

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

08

正しさの証明

正しさの証明

補題１：

補題１：

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

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

n := N; ループの前
k := 1;
while (n > 0) {k := k*n;n := n-1;}
ループの後 ☃

kold，nold と knew，nnew と書くと，（仮定）（示したいこと）

kold * (nold !) = N!

knew * (nnew !) = N!

ループ不変量：いま，knew * (nnew !)= (kold * nold) * ( (nold - 1)! )[knew，nnewの定義より]= N!

[仮定より]= kold * (nold !)よって成立．



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

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

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



10

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

補題１：

ループの後 ☃

すなわち，で成り立てば☃でも成り立つ．

9

正しさの証明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! はループに入る前で成立．

プログラムの正しさの証明：... Hoare logic!

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

Hoare 論理

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”

13

プログラム

{ n=2 } n:=n+1 { n=3 }例：

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

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

プログラム意味論

メモリ状態の性質を記述するための assertion
language
Hoare triple を導くための導出規則 （ルール）
機械的な，文字列の書き換え
15

1614

「意味論」とは？

メモリ状態

プログラムの「意味」は何か
n := N;k := 1;
while (n > 0) {k := k*n;n := n-1;}

正確な答え：「実行した際の MacBook のメモ
リ状態の変化」" 細かすぎて「使えない」

変数と値の対応の表のこと．
x y

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

213 

数学的には： 関数
σ : Var −→ Z

1718

プログラムの意味

プログラムの意味

メモリ状態の変換としてメモリ状態の変換として

つまり，関数 MSt −→ MSt ∪ {⊥}x は変数，a は「数の表現」（たとえば y+1）

つまり，関数 MSt −→ MSt ∪ {⊥}�→ ：「変形する」「移す」
��σ �−→ σ x �→ �a�σ�x := a� :プログラム x:=a の「意味」

�→�→..
.

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

メモリ状態，
たとえば

x
 y

�→
�→..
.

x の値を，a を σ のもとで計算し213 た値（たとえば�y + 1�σ = 14�P1 ; P2 � :P1 ，P2 はプログラム

σ�−→

��
�P2 � �P1 �σ

まず P1 によって変換

次に P2 によって変換とか）にアップデート

1920

プログラムの意味

プログラムの意味

メモリ状態の変換としてメモリ状態の変換として

つまり，関数 MSt −→ MSt ∪ {⊥}つまり，関数 MSt −→ MSt ∪ {⊥}�while b P � :�if b then P1 else P2 � :��P1 �σ if �b�σ is trueσ �−→
�P2 �σ if �b�σ is falseσ, �P �σ,21プログラムの意味論：「停止しない」つまり，関数 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 � :σ�−→�ポイント：
数学的に厳密な定義...

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

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

（ x > 0 とか）

��−→ ??

��n
ある時点で b が偽になれば，つまり �b� �P � σ = falseb は「真偽表現」

メモリ状態の変換としてσ状態変換の繰り返し �P �n σを考える：

P1 ，P2 はプログラムまとめ「停止しない」要素還元的（大きなプログラムの意味は，その部品の意味から決まる） 23

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

22

Hoare 論理の「材料」（思い出そう）

プログラム意味論

プログラム ＝ メモリ状態の変換
メモリ状態の性質を記述するためのassertion language
Hoare triple を導くための導出規則
24

Assertion Language

Assertion

Language

Assertion: メモリ状態の性質を記述する「論理式」．例：
x=5y≤3z. ( x = 2 * zy=3*z)

本当ならば，言語（文法）をはっきり定めることが望ましい．たとえば：AExp �Fml �aA::=::=x | n | a1 + a2 | a1 − a2 | a1 ∗ a2
true | false | A1 ∧ A2 | ¬A | a1 < a2 |∀x ∈ N. A
where x ∈ Var

とくに，証明の形式化・自動化のためには必須
25

ここではやらない（時間がないから）

26

Hoare 論理

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}27

実行前に成り立つ性質“precondition”

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

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

28

Hoare Triple の意味論

実行前に成り立つ性質“precondition” を表す
assertion

実行後に成り立つ性質“postcondition” を表す assertion{A} P {B}Partial Correctness{A} P {B}
「 {A} P {B} が真」であるとは，
assertion A をみたす任意のメモリ状態σについて，プログラムメモリ状態 [| P |]σ が assertion B をみたすことをいう．

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

「" P が停止しないときに関しては，何も保証してくれな
い （“partial correctness”）
29

そもそも「P が停止するか？」はとても難しい問題．
決定不能！（判定してくれるプログラムは存在しない）

30

Hoare 論理の導出規則

真な 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 }停止しないのでだったらどうする？
はすべての assertion をみたす」と約束．

（この規則では仮定はなし）{ A[a/x] } x:=a { A }assertion A において，変数 x を aに書き換えたもの(Assign)
規則の名前（assignment = 「値の割り当て」）

結論 { A[a/x] } x:=a { A } は，右から左に読むとよい．

postcondition が何であっても，この Hoare triple は
真「x:=a の後に A が成り立つためには，実行前には A[a/x] が成り立たてばよい」
31

32

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

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

Hoare 論理の導出規則(Assign)
規則の名前（assignment = 「値の割り当て」）

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

例：

規則は上から下に{ y=2 } x:=y { x=2 }{ k*((n-1)!)=N!

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

n≥0 }（上が成り立てば下が成り立つ）

証明を探すときは逆（下が成り立つためには，どんな上が成り立てばいい？）{ x-1=2 } x:=x-1 { x=2 }Hoare triple は右から左に（postcondition が成り立つためには．．．）
33

Hoare 論理の導出規則

34

さっきの例，くわしく！！
(Assign)(Assign)

規則の読み方：「上の仮定が成立していれば，下の結論も成立」(SeqComp){ A } P1 { C }{ x-1=2 } x:=y { y-1=2 }{ C } P2 { B }{ A } P1; P2 { B }(SeqComp){ 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)

規則の名前（sequential composition =「逐次合成」）{ 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 }{ x-1=2 } y:=x { y-1=2 }(Assign){ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } y:=x; y:=y-1 { y=2 }(Assign)(Assign)(Assign)(SeqComp){ x-1=2 } x:=y { y-1=2 }35{ y-1=2 } y:=y-1 { y=2 }{ x-1=2 } x:=y; y:=y-1 { y=2 }考えの流れ(SeqComp)Step 4:「x-1=2 であるためのprecondition，わかった！」36

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

例：{

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

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

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

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

{k*(n!)=N!

n≥0(SeqComp)n≥0}¬ (x>0)} x:=x { x≥0 }{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }(If)b } P1 { A }

¬b }

38

Hoare 論理の導出規則

A はループ不変量！

{ A } while b P1 { A{ x≥0x>0 } x:=x-1 { x≥0 }37

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

{A(While)b } P1 { A }{ A } while b P1 { A

ループを脱出した "¬b }(While)

ループを脱出した "b は成立しないはず

b は成立しないはず

例：

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

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ʼ

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

A Aʼ

規則の名前
（consequence =仮定： 「A が成り立てば，必ず Aʼ も成り立つ」成り立つ」「（論理的）帰結」）

( x≥0

規則の名前
（consequence =仮定： 「A が成り立てば，必ず Aʼ も

例：x>0{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}「（論理的）帰結」）

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

n-1≥0

41

Hoare 論理の導出規則（まとめ）{ A } P1 { C }{ A b } P1 { B }(Assign)n-1≥0

k*(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)
42A Aʼ

{ Aʼ } P { Bʼ } Bʼ B(Conseq){A } P {B}(SeqComp){ A ¬b } P2 { B }{ A } if b then P1 else P2 { B }{A{k*n*((n-1)!)=N!

Hoare 論理の導出規則（まとめ，つづき）{ C } P2 { B }{ A } P1; P2 { B }{k*n*((n-1)!)=N!

{ x>0 } x:=x-1 { x≥0 }{ A[a/x] } x:=a { A }k*(n!)=N!

b } P1 { A }{ A } while b P1 { A¬b }(If)(While)4344

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

Hoare 論理に{おける導出

k=1

n=N}

while (n>0){k:=k*n;n:=n-1「意味論的立場」

Hoare 論理の導出規則を繰り返し使って，仮定なしの「導出木」（「証明木」）が作れればOK！

assertion A をみたす任意のメモリ状態σについて，メモリ状態 [| P |]σ が assertion B をみたすことをいう

．
直接の証明

記号操作，証明「検索」" 自動化！

「数学の証明」，頭を使う．
" 自動化できない！

Hoare 論理の導出}「構文論的立場」「 {A} P {B} が真」であるとは，

45

k = N!

46

Hoare 論理の導出木！！
（導出木，証明木）

x≥0(Assign)x>0{ x-1≥0 } x:=x-1 { x≥0 }x-1≥0{x≥0x>0(Conseq)} x:=x-1 { x≥0 }x≥0¬ (x>0)x≥0(Assign){ x≥0 } x:=x { x≥0 }x≥0{ ¬ (x>0) } x:=x { x≥0 }{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }(Conseq)x≥0(Assign)x>0{ x-1≥0 } x:=x-1 { x≥0 }

x-1≥0

{(If)

x≥0x>0(Conseq)} x:=x-1 { x≥0 }x≥0¬ (x>0)x≥0(Assign){ x≥0 } x:=x { x≥0 }x≥0{ ¬ (x>0) } x:=x { x≥0 }{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }47(Conseq)

(If)

48

Hoare 論理の導出

健全性，完全性

たとえば，次の Hoare triple を証明したい．

{k=1n=N}

while (n>0)
k:=k*n;n:=n-1「意味論的立場」「 {A} P {B} が真」であるとは，assertion A をみたす任意のメモリ状態σについて，メモリ状態 [| P |]σ が assertion B をみたすことをいう

．
直接の証明

「数学の証明」，頭を使う．
" 自動化できない！

{k = N!

意味論と構文論のせめぎあい！！
（導出規則＝構文論＝「機械」）}

健全性 soundness: 導出規則で導かれる Hoare triple は，すべて真「ウソは言わない」「構文論的立場」「証明能力が高すぎない」

Hoare 論理の導出規則を繰り返し使って，仮定なしの「導出木」（「証明木」）
が作れればOK！

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

記号操作，証明「検索」" 自動化！
49

50

健全性，完全性
Hoare 論理は健全性を満たす．

例： 階乗の計算

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

52

はじめの例

Hoare 論理による証明

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

目標： 次の Hoare triple の導出

実行後の k の値は N!

{

この証明を，Hoare 論理を使っk=1

while (n>0)

}

n=N

{

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

k = N!

}てシステマティックに！

（構文論的・機械的な，記号書きN の階乗 N! を換えによる証明）

計算するプログラム

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

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

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

k=1

n=N

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

k:=k*nn-1≥0

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

n:=n-1n-1≥0{

k*(n!)=N!

{{n≥0n>0}k*(n!) = N!

n≥0

k=1

n=N}

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

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

k*(n!)=N!

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

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

n:=n-1{n≥0(SeqComp)}}{}(Assign){k*n*((n-1)!)=N!
n-1≥0k*(n!)=N!
n≥0n>0

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

(Conseq)(While)k*(n!)=N!

n≥0

k=N!

k = N!

}

n-1≥0

k=1

¬(n>0)(Conseq)55

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

Hoare 論理による証明(Assign)k*(n!)=N!

}n≥0k*(n!)=N!

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

54

n=N

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

k:=k*nn-1≥0

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

n:=n-1n-1≥0{

k*(n!)=N!

{{n≥0n>0}k*(n!) = N!

n≥0

k=1

n=N}

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

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

k*(n!)=N!

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

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

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

n≥0(SeqComp)}n≥0

k*(n!)=N!

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

ループ不変量！

}}{(Assign)(Conseq)(While)k*(n!)=N!

n≥0

k=N!

k = N!

}}¬(n>0)(Conseq)

56

大問題

参考文献

（気づいた？）
ループ不変量の見つけ方 (invariant discovery)

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

Hoare 論理のルールを見ても，書いてない！
理論的には述語論理で書き下せる．
（While ループの意味論をなぞる．cf. 相対完全性）

K. Suenaga and I. Hasuo. Programming with Inﬁnitesimals: A
While-Language for Hybrid System Modeling. Proc. ICALP
2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag

が，とても複雑な式" その後の検証がうまく回らない．（Aʼ A の真偽判定などで検証器落ちる）

I. Hasuo and K. Suenaga. Exercises in Nonstandard Static
Analysis of Hybrid Systems. To appear in Proc. CAV 2012.

プログラム検証の研究の大部分が，invariant discovery の研究
さまざまな heuristics: (non-)linear arithmetic,abstract interpretation, CEGAR, ...
57

58

プログラム自動検証器のデモ

Hoare 論理 ＋ 超準解析

離散的なプログラムだけでなく，自己紹介

連続的な物理量も含むハイブリッドシステムの検証
応用： 物理情報システム（車，飛行機，家電，...）
末永幸平先生（京大）との共同研究
59

60

研究テーマ

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

抽象数学をつかって，情報科学の新パラダイムに斬り込む

京都大学数理解析研究所 助教（2007-2011)東京大学理学部情報科学科 講師（2011-）

特に： 圏論，数理論理学，代数学，幾何学

専門分野： 数学と計算機科学を行ったり来たり
理学部情報科学科での立ち位置：

Kleisli 圏での余代数

応用 vs. 理論

Hoare 論理 ＋ 超準解析

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

速度 vs. 正しさ

Geometry of Interaction

パラメータを変えて具体化を見極める

既存の手法

http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro

非決定的システム
ふつうの計算抽象的，一般的

新たな手法

離散的システム

確率的システム

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

61

62

メッセージ

お待ちかね：

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

レポート課題そもそもコンピュータは数学（数学基礎論）から生まれた

63

64

レポート課題

レポート課題

1. 次の４つの Hoare triple について，真であるかどうか判定せよ．（証明・反例があればなおよい）

2. 次の2つのHoare triple に対して，Hoare 論理の導出木を与えよ．ただし x,n,m は整数(int)型の変数とする．

{ 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 }{ x≥0 } if x>0 then x:=x-1 else x:=x { x≥0 }ヒント： 38 ページのルールの適用（まだ仮定が残ってる！）を完成させる．

y:=0; x:=X;{ X!0 }

while (x>100) {y:=y+1;
x:=x-100}{0"x<100 ∧100*y + x = X{ m (m≥0}

気持ち： X セントを「y ドル x セント」に変換するプログラム 65n=2*m) } while (n>0) { n:=n-2} { n=0 }「n は負でない偶数」
66

レポート課題レポート課題

3. [Hoare 論理とは関係ない算数の問題]
２つの正の整数 m, n （ただし m > n）について，4. 正の整数X, Y の最大公約数を計算するための，次のプ
ログラム P を考える（ユークリッドの互除法）．
ヒント：

x:=X; y:=Y;
while (x#y) {if x!ythen x:=x-yelse y:=y-x}

GCD(m, n) = GCD(m - n, n)であることを示せ．ただし，GCD(m, n) は
m と n の最大公約数を表す．

• 55ページを参考に．
• レポート課題の問題３を使う．

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

次の Hoare triple の，Hoare 論理における導出木を与えよ．
67{ X>0Y>0 } P { x=y=GCD(X,Y) }68

念のため全問解かなくても大丈夫だが，たくさん解いたほうがよい（当たり前）
コピーはダメ！
東北大学 小林直樹先生のページを参照
http://www.kb.ecei.tohoku.ac.jp/~koba/report.html

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