逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法)

Slides:



Advertisements
Similar presentations
5.制御構造と配列 場合分け( If Then Else , Select Case ) 繰返し( Do While ) 繰返しその2( For Next )
Advertisements

ベイズの定理と ベイズ統計学 東京工業大学大学院 社会理工学研究科 前川眞一. 2 Coffe or Tea 珈琲と紅茶のどちらが好きかと聞いた場合、 Star Trek のファンの 60% が紅茶を好む。 Star Wars のファンの 95% が珈琲を好む。 ある人が紅茶を好むと分かったとき、その人が.
だい六か – クリスマスとお正月 ぶんぽう. て form review ► Group 1 Verbs ► Have two or more ひらがな in the verb stem AND ► The final sound of the verb stem is from the い row.
て -form - Making て -form from ます -form -. With て -form, You can say... ~てもいいですか? (= May I do…) ~てください。 (= Please do…) ~ています。 (= am/is/are doing…) Connecting.
第 5 章 2 次元モデル Chapter 5 2-dimensional model. Contents 1.2 次元モデル 2-dimensional model 2. 弱形式 Weak form 3.FEM 近似 FEM approximation 4. まとめ Summary.
VE 01 え form What is え form? え? You can do that many things with え form?
白井 良明 立命館大学情報理工学部 知能情報学科
ロジスティクス工学 第6章 動的ロットサイズ決定モデル 東京商船大学 久保 幹雄
ループで実行する文が一つならこれでもOK
アルゴリズムイントロダクション第2章 主にソートに関して
データ構造とアルゴリズム論 第5章 整列(ソート)のアルゴリズム
TRIVIA QUIZ Choose a group name! Write this on your answer sheet
All Rights Reserved, Copyright (C) Donovan School of English
The authors have no actual or potential declaration to make.
Verb てform + から、 After.
てフォーム Conjoining sentences (Verb)
プログラムの正当性(2) 正当性証明の基本原理
第10回 ソート(1):単純なソートアルゴリズム
Solid State Transformer (SST)
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
Semantics with Applications
Let’s learn how to say where the zoo animals have come from in Japanese! Listen and repeat.
岩井 儀雄 コンピュータ基礎演習  ー探索、整列ー 岩井 儀雄
Let’s learn how to say where the zoo animals have come from in Japanese! Listen and repeat.
最短経路.
大域的データフロー解析 流れグラフ 開始ブロック 基本ブロックをnodeとし、 基本ブロック間の制御関係をedgeとするグラフを、
ストップウォッチの カード ストップウォッチの カード
カタカナ  4 When you want to own a car in the big cities in Japan, you need to prove you have a place to park your car. Unless you have a parking space on.
ロジスティクス工学 第7章 配送計画モデル 東京商船大学 久保 幹雄
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
第25章 単一始点最短路 3節 Bellman-Fordのアルゴリズム
帰納変数 iが基本帰納変数 変数iに対して、 i := i±c という形の代入が一つのみ jがiに対する帰納変数
アルゴリズムとプログラミング (Algorithms and Programming)
CHANGING VERBS TO “Potential form” easy ですよ!.
アルゴリズムとデータ構造 補足資料5-2 「サンプルプログラムsetop.c」
にほんご JPN101 Oct. 5, 2009 (Monday).
Term paper, Report (1st, first)
Structured programming
情報工学概論 (アルゴリズムとデータ構造)
Volleyball club ZAURUS
Where is Wumpus Propositional logic (cont…) Reasoning where is wumpus
プログラミング言語論 第4回 文の翻訳 C言語の文 表明 Hoare論理
クイズやゲーム形式で紹介した実例です。いずれも過去のインターン作です。
2019年4月8日星期一 I. EPL 84, (2008) 2019年4月8日星期一.
Structural operational semantics
データ構造とアルゴリズム論 第5章 整列(ソート)のアルゴリズム
2009/10/23 整列アルゴリズム (1) 第4講: 平成21年10月23日 (金) 4限 E252教室 コンピュータアルゴリズム.
プログラムの正当性(2) 正当性証明の基本原理
プログラミング言語論 第7回 文の翻訳 C言語の文 表明 Hoare論理
再帰的手続き.
2019/4/22 Warm-up ※Warm-up 1~3には、小学校外国語活動「アルファベットを探そう」(H26年度、神埼小学校におけるSTの授業実践)で、5年生が撮影した写真を使用しています(授業者より使用許諾済)。
データ構造とアルゴリズム論 第5章 整列(ソート)のアルゴリズム
Term paper, report (2nd, final)
プログラムの基本構造と 構造化チャート(PAD)
情報工学科 3年生対象 専門科目 システムプログラミング 第4回 シェルスクリプト 情報工学科 篠埜 功.
モデル検査(5) CTLモデル検査アルゴリズム
知能ソフトウェア特論 Intelligent Software
知能ソフトウェア特論 Intelligent Software
Conflict of Interest disclosure slide A potential conflict of interest exists when there is involvement between the speaker/presenter with any for-profit.
Create the Future Appreciate the difference
復習 if ~ 選択制御文(条件分岐) カッコが必要 true 条件 false 真(true)なら この中が aを2倍する 実行される
プログラミング言語論 第4回 文の翻訳 C言語の文 表明 Hoare論理
プログラミング言語論 第4回 文の翻訳 C言語の文 表明 Hoare論理
Term paper, report (2nd, final)
~sumii/class/proenb2009/ml6/
2017年度 有限幾何学 期末試験 注意:ループと多重辺がないグラフのみを扱う. 問1 次の定理と,その証明の概略を読み,各問に答えよ.
日本膵臓学会 CO I 開示 発表者名(全員記載): ○○ ○○ 、 ○○ ○○ 、・・・ (◎発表責任者)
場合分け(If Then Else,Select Case) 繰返し(Do While) 繰返しその2(For Next)
アノテーションガイドラインの管理を行う アノテーションシステムの提案
HYSPRIT Chiba campaign (daily)
Presentation transcript:

逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法) 表現系工学特論 逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法)

1.正当性アサーション(復習) precondition loop invariant potential function post condition

2.正当性の証明(復習) 部分正当性 もし実行が停止すれば,その時点で事後条件が成り立つ. 停止性 必ず実行が停止する. 部分正当性      もし実行が停止すれば,その時点で事後条件が成り立つ. 停止性      必ず実行が停止する. partial correctness termination

3.帰納的アサーション法(Floyd法)による部分正当性の証明 Put at least one assertions in each loop. (2) For each path starting from and ending at prove the following statement: ■ is true at if when the control has reached then

3.帰納的アサーション法(Floyd法)による部分正当性の証明 プログラムのループの少なくとも1カ所に   必ずアサーションを書く. (2) アサーション を書いた位置 からアサーション に到達するすべての経路ごとに 次のことを証明する. ■位置 が真のとき, に到達した時点で は真である で その経路に沿ってプログラムを実行して 位置  ただし,経路の途中で他のアサーションが書かれた位置を 通過しないものについてのみでよい.  経路がループのとき,i = j でもよい.

■例題 挿入ソート

挿入ソート(Java版) //loop invariant: A[0]..A[i-1] are sorted; // 1≦i≦n for(i=1; i!=n; i++) { w=A[i];   //insert w into (or append w to) A[0]..A[i-1] // to make A[0]..A[i] sorted. //loop invariant: A[0]..A[j],A[j+2]..A[i] are sorted; // (try to place w at A[j+1]) // w<A[j+2] if j<i-1; // 1≦i≦n-1; -1≦j≦i-1 for(j=i-1; j>=0 && w<A[j]; j--) { A[j+1]=A[j]; } A[j+1]=w; }

経路ごとの証明(1/7) #1 #2 (0)→(1) (1)→(4) (1)→(2) (2)→(3) #1 (2)→(3) #2 (3)→(1) (2)→(2) #1 #2

経路ごとの証明(2/7):(0)→(1) ,(1)→(4) (0)→(1): I = 1より自明. (1)→(4): I = nより自明.

経路ごとの証明(3/7):(1)→(2) 2 3 5 4 6 7 8 9 J sorted W I I ≠ n W = A[I] J = I - 1

経路ごとの証明(4/7):(2)→#1→ (3)の証明 sorted J = -1 J I 1 2 3 5 6 7 8 9 1 < A[0] = W

経路ごとの証明(5/7):(2)→#2→ (3)の証明 sorted J ≧ 0 J I #2 2 3 4 5 6 7 8 9 ≦ 4 < A[J] ≦ W A[J+1] = W

経路ごとの証明(6/7):(3)→(1)の証明 2 3 4 6 7 8 9 5 sorted I sorted 2 3 4 6 7 8 9

演習問題 経路ごとの証明(7/7): (2)→(2)の証明 演習問題 経路ごとの証明(7/7): (2)→(2)の証明 2 3 5 4 6 7 8 9 J sorted < I J ≧ 0 > W < A[J] sorted 2 3 6 7 8 9 J 5 4 < I A[J+1] = A[J]