Mercurial > hg > Papers > 2015 > atton-thesis

changeset 85:bcd56a757a1a presen_final

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix presentation
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 19 Feb 2015 14:14:52 +0900
parents 751e83a23d82
children 70dcf08c8095
files presentation/slide.html presentation/slide.md
diffstat 2 files changed, 22 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.html	Thu Feb 19 09:07:23 2015 +0900
+++ b/presentation/slide.html	Thu Feb 19 14:14:52 2015 +0900
@@ -31,12 +31,12 @@
 <div class="slide" id="2"><div>
 		<section>
 			<header>
-				<h1 id="section">研究目的</h1>
+				<h1 id="section">研究目的 : プログラムの変更の形式化</h1>
 			</header>
 			<!-- === begin markdown block ===
 
       generated by markdown 1.1.1 on Ruby 2.2.0 (2014-12-25) [x86_64-darwin13]
-                on 2015-02-19 09:06:34 +0900 with Markdown engine kramdown (1.4.2)
+                on 2015-02-19 14:14:41 +0900 with Markdown engine kramdown (1.4.2)
                   using options {}
   -->
 
@@ -58,7 +58,7 @@
 <div class="slide" id="3"><div>
 		<section>
 			<header>
-				<h1 id="section-1">研究目標</h1>
+				<h1 id="monad-">研究目的 : Monad を用いた変更の形式化</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -79,13 +79,13 @@
 <div class="slide" id="4"><div>
 		<section>
 			<header>
-				<h1 id="section-2">プログラムの変更の形式化</h1>
+				<h1 id="section-1">プログラムの変更の形式化</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
 <ul>
   <li>形式手法とはソフトウェアの検証に数学や論理学を用いる手法</li>
-  <li>論理と対応する lambda 計算を用いたプログラムの解析などがある</li>
+  <li>論理と対応する lambda 計算を用いたプログラムの形式化などがある</li>
   <li>Moggi らによれば圏論のMonad は関数とメタ計算を含む関数との対応</li>
   <li>メタ計算として変更を定義することで形式的な定義を与える</li>
   <li>「過去の変更を全て保存する」メタ計算 Delta Monad を提案する</li>
@@ -99,7 +99,7 @@
 <div class="slide" id="5"><div>
 		<section>
 			<header>
-				<h1 id="section-3">プログラムの定義</h1>
+				<h1 id="section-2">プログラムの定義</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -194,7 +194,7 @@
 			<!-- _S9SLIDE_ -->
 
 <ul>
-  <li>関数の適用をメタ計算を行なう中置関数 <code>&gt;&gt;=</code> として定義</li>
+  <li>関数の適用時にメタ計算を行なう中置関数 <code>&gt;&gt;=</code> として定義</li>
   <li>return はメタ計算に値を対応させる関数</li>
 </ul>
 
@@ -273,7 +273,7 @@
 <div class="slide" id="13"><div>
 		<section>
 			<header>
-				<h1 id="section-4">異なるバージョンを同時に実行する</h1>
+				<h1 id="section-3">異なるバージョンを同時に実行する</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -294,7 +294,7 @@
 <div class="slide" id="14"><div>
 		<section>
 			<header>
-				<h1 id="monad-">他の Monad との組み合せ</h1>
+				<h1 id="monad--1">他の Monad との組み合せ</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -302,6 +302,7 @@
   <li>Delta Monad 以外にもメタ計算は Monad として提供されている</li>
   <li>例外機構、ロギング、入出力など</li>
   <li>他の Monad と組み合せることにより変更に対する計算が定義できる</li>
+  <li>Delta Monad が他の Monad と組み合わせ可能であることは証明した</li>
 </ul>
 
 
@@ -320,7 +321,7 @@
   <li>ログを取る Writer Monad と組み合せた numberCount の実行結果</li>
 </ul>
 
-<pre><code>*Main&gt; numberCountM 1000
+<pre><code>*Main&gt; numberCountM 10
 DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
                            "[2,3,5,7]",
                            "4"]))
@@ -337,7 +338,7 @@
 <div class="slide" id="16"><div>
 		<section>
 			<header>
-				<h1 id="delta-">Delta による信頼性向上手法</h1>
+				<h1 id="delta-">Delta による信頼性向上</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -360,14 +361,14 @@
 <div class="slide" id="17"><div>
 		<section>
 			<header>
-				<h1 id="section-5">まとめと課題</h1>
+				<h1 id="section-4">まとめと課題</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
 <ul>
   <li>メタ計算によってプログラムの変更を定義できた</li>
   <li>メタ計算により信頼性の向上手法を提案できた</li>
-  <li>Monad であることを Agda によって示した</li>
+  <li>Delta Monad が Monad 則を満たすことを Agda によって示した</li>
   <li>プログラムの変更を全て Delta Monad で記述できるか?</li>
   <li>形式的な視点からプログラムの変更とは?
     <ul>
--- a/presentation/slide.md	Thu Feb 19 09:07:23 2015 +0900
+++ b/presentation/slide.md	Thu Feb 19 14:14:52 2015 +0900
@@ -3,14 +3,14 @@
 profile : 琉球大学工学部 <br> 情報工学科 <br> 並列信頼研究室(河野研)
 lang: Japanese
 
-# 研究目的
+# 研究目的 : プログラムの変更の形式化
 * プログラムの信頼性を向上させる
 * 信頼性とはプログラムが正しく動く保証である
 * プログラムの信頼性はバグなどの原因で低下する
 * 信頼性が低下するきっかけにプログラムの変更がある
 * プログラムの変更を形式化することで信頼性を保証する
 
-# 研究目標
+# 研究目的 : Monad を用いた変更の形式化
 * Monad を用いてプログラムの変更を形式化する
 * プログラムにおける Monad はメタ計算を表現するために用いる
 * メタ計算とは計算を実現するための計算である
@@ -20,7 +20,7 @@
 
 # プログラムの変更の形式化
 * 形式手法とはソフトウェアの検証に数学や論理学を用いる手法
-* 論理と対応する lambda 計算を用いたプログラムの解析などがある
+* 論理と対応する lambda 計算を用いたプログラムの形式化などがある
 * Moggi らによれば圏論のMonad は関数とメタ計算を含む関数との対応
 * メタ計算として変更を定義することで形式的な定義を与える
 * 「過去の変更を全て保存する」メタ計算 Delta Monad を提案する
@@ -64,7 +64,7 @@
     * 関数適用 : バージョンごとに関数適用する
 
 # Haskell における Monad の instance 定義
-* 関数の適用をメタ計算を行なう中置関数 ``>>=`` として定義
+* 関数の適用時にメタ計算を行なう中置関数 ``>>=`` として定義
 * return はメタ計算に値を対応させる関数
 
 ```
@@ -118,12 +118,13 @@
 * Delta Monad 以外にもメタ計算は Monad として提供されている
 * 例外機構、ロギング、入出力など
 * 他の Monad と組み合せることにより変更に対する計算が定義できる
+* Delta Monad が他の Monad と組み合わせ可能であることは証明した
 
 # Writer Monad と組み合せる
 * ログを取る Writer Monad と組み合せた numberCount の実行結果
 
 ```
-*Main> numberCountM 1000
+*Main> numberCountM 10
 DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
                            "[2,3,5,7]",
                            "4"]))
@@ -132,7 +133,7 @@
                            "5"]))))
 ```
 
-# Delta による信頼性向上手法
+# Delta による信頼性向上
 * 各トレースの比較によるデバッグ
 * 異なるバージョンの同時実行によるバージョン間互換
 * 正常系と開発版を同時に実行できる
@@ -142,7 +143,7 @@
 # まとめと課題
 * メタ計算によってプログラムの変更を定義できた
 * メタ計算により信頼性の向上手法を提案できた
-* Monad であることを Agda によって示した
+* Delta Monad が Monad 則を満たすことを Agda によって示した
 * プログラムの変更を全て Delta Monad で記述できるか?
 * 形式的な視点からプログラムの変更とは?
     * 同時実行は product, repository は colimit?