1.アルゴリズムの基本概念

(A)アルゴリズムに関する用語（教科書やプリントにある分は省略）

(1)アルゴリズム

　もとは算用数字を用いた筆算のこと。計算や問題を解決するための手順、方式。特にコンピューターのプログラムに適用可能な手続きをいうことが多い。
　情報処理の手順そのものの事をさす。講義ではフローチャートで表していた。

(2)プログラム

　コンピューターに、情報処理を行うための動作手順を指定するもの。

2.アルゴリズムの正当性検証

　正当性には部分正当性（弱正当性）と停止性があり、両方が成立して初めて正当であるといえる。

部分正当性・・・仮に停止するなら、正しい。
停止性・・・必ず停止する。

(A)フローチャートプログラムについて

(1)変数

　入力変数、作業変数。結果変数がある。
　プリントの例1では、入力変数がx、作業変数がy₁ y₂ y₃、結果変数がz。

(2)ステートメント

　スタートステートメント・割当ステートメント・テストステートメント・停止ステートメントがある。
　プリントの例1では、
　スタートステートメント・・・STARTから(y₁,y₂,y₃)←(0,0,1)まで。
　割当ステートメント・・・y₂←y₂+y₃など。
　テストステートメント・・・y₂>xの部分。
　停止ステートメント・・・z←y₁の部分。

(3)データ述語φ(x)

　入力変数xが満たすべき条件の事。例えば、例1のプログラムにx="本日は晴天なり"というデータを入れることは意味が無い。

(4)結果の述語Ψ(x,z)

　アルゴリズムが終わったあとに、入力変数xと出力変数zが満たすべき性質。
　例1の場合、z=(x^0.5を越えない最大の整数値)

(B)正当性の検証

(1)停止性の検証

　そのアルゴリズムがデータ述語を満たす全ての入力xに対して停止するかの検証。

(2)弱正当性の検証

　全ての入力に対してそのアルゴリズムが停止すると仮定して、全ての入力（φ(x)が真であるもの）に対して結果が正しい（Ψ(x,z)が真）かどうかの検証。

〜プリントの例1で検証してみる〜

　入力条件（データ述語） x>0
　結果の述語 z²<=x<=(z+1)²
(1)弱正当性の検証

step1.ループを切る
α STARTから(y₁,y₂,y₃)←(0,0,1)まで。
β y₂←y₂+y₃から(y₁,y₃)←(y₁+1,y₃+2)まで。
γ y₂←y₂+y₃からHALTまで。

step2.検証条件を作る

　基本的に次のような形になる。
その道に入る前の状態∧その道が通過される条件→その道を通った後の状態
　ループがあるときは、
n回目のループで成立している状態∧その道が通過される条件→n+1回目のループで成立されるべき状態
　その道を通った後の状態やn+1回目のループで成立されるべき状態は発見的に構成する。今回の例では
P:y₁²<=x∧y₂=(y₁+1)²∧y₃=2y₁+1
α x>0→(0²<x∧1=(0+1)²∧1=2*0+1)
β (y₁²<=x∧y₂=(y₁+1)²∧y₃=2y₁+1∧y₂<=x)→((y₁+1)²<=x∧y₂+y₃+2=(y₁+2)²∧y₃+2=2(y₁+1)+1
γ (y₁²<=x∧y₂=(y₁+1)²∧y₃=2y₁+1∧y₂>=x)→y₁²<=x<(y₁+1)²

めも〜〜何でこうなるのかって言うのは次回先生がやってくれるんだろうなぁ