Mercurial > hg > Papers > 2015 > atton-sigse
changeset 52:780eab85e724
Update slides. Add links, add lectures
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 21 Jan 2015 20:26:55 +0900 |
| parents | 6972867ea8f4 |
| children | 65391f6321a8 |
| files | slide/slide.html slide/slide.md |
| diffstat | 2 files changed, 149 insertions(+), 46 deletions(-) [+] |
line wrap: on
line diff
--- a/slide/slide.html Wed Jan 21 17:26:23 2015 +0900 +++ b/slide/slide.html Wed Jan 21 20:26:55 2015 +0900 @@ -36,7 +36,7 @@ <!-- === begin markdown block === generated by markdown 1.1.1 on Ruby 2.2.0 (2014-12-25) [x86_64-darwin13] - on 2015-01-21 17:26:16 +0900 with Markdown engine kramdown (1.4.2) + on 2015-01-21 20:24:29 +0900 with Markdown engine kramdown (1.4.2) using options {} --> @@ -46,6 +46,7 @@ <li>大学ではどんなことをやっているか(講義, イベント, 研究)</li> <li>講義などでつまづくポイント</li> <li>つまづきの解決策</li> + <li>どのような講義をするべきか?</li> </ul> @@ -56,13 +57,26 @@ <div class="slide" id="3"><div> <section> <header> - <h1 id="section">講義で紹介する形式手法</h1> + <h1 id="section">講義で使用している形式手法</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>model checking 的なアプローチ</li> - <li>証明的なアプローチ</li> + <li>仕様記述 + <ul> + <li>UML</li> + </ul> + </li> + <li>model checking 的なアプローチ + <ul> + <li>Java Path Finder</li> + </ul> + </li> + <li>証明的なアプローチ + <ul> + <li>Haskell, Agda</li> + </ul> + </li> </ul> @@ -73,12 +87,30 @@ <div class="slide" id="4"><div> <section> <header> + <h1 id="section-1">仕様記述</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>モデリングと設計 の講義</li> + <li>iOS Application を作成する</li> + <li>ユースケース図やクラス図を使って仕様を考える</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="5"><div> + <section> + <header> <h1 id="model-checking-">model checking 的なアプローチ</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>Operationg System の講義</li> + <li><a href="http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/os/index.html">Operationg System</a> の講義</li> <li>Process/Thread Scheduling を考えた時に</li> <li>Dead Lock を起こすような Scheduling を実際に書いて実行させる</li> <li>Java Path Finder で Thread の実行順序を網羅的に実行する</li> @@ -89,15 +121,15 @@ </section> </div></div> -<div class="slide" id="5"><div> +<div class="slide" id="6"><div> <section> <header> - <h1 id="section-1">証明的なアプローチ</h1> + <h1 id="section-2">証明的なアプローチ</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>ソフトウェア工学 の講義</li> + <li><a href="http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/index.html">ソフトウェア工学</a> の講義</li> <li>集合, 論理, 関数, 自然演繹による証明</li> <li>型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明</li> <li>Haskell : 自然演繹と lambda calculus</li> @@ -110,7 +142,7 @@ </section> </div></div> -<div class="slide" id="6"><div> +<div class="slide" id="7"><div> <section> <header> <h1 id="agda-">Agda による証明を解説した例</h1> @@ -119,29 +151,9 @@ <ul> <li>Open Source Conference</li> - <li>ソフトウェア工学で学んだ Agda の使い方を発表</li> + <li>ソフトウェア工学で学んだ Agda を <a href="http://ie.u-ryukyu.ac.jp/~e115763/slides/events/osc2014/slide.html">Agda 入門</a>として発表</li> <li>Agda で SystemT の Nat の加法の交換法則を解説</li> - <li>ほとんどが定義の解説に時間を取られてしまう</li> -</ul> - - - - </section> -</div></div> - -<div class="slide" id="7"><div> - <section> - <header> - <h1 id="section-2">圏によるプログラムの形式化</h1> - </header> - <!-- _S9SLIDE_ --> - -<ul> - <li>プログラムの変更を Monad で表す</li> - <li>プログラムの変更時に変更前のプログラムも残したまま変更する</li> - <li>全てのバージョンのプログラムを同時に実行できる</li> - <li>デバッグやテストと組み合せることでバグ</li> - <li>実行系と検証系を同時に走らせることもできる</li> + <li>定義の解説にほとんどの時間を取られてしまう</li> </ul> @@ -152,15 +164,16 @@ <div class="slide" id="8"><div> <section> <header> - <h1 id="section-3">学習コスト</h1> + <h1 id="section-3">圏によるプログラムの形式化</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>論理, 自然演繹 -> Haskell -> Agda</li> - <li>それぞれのステップに壁がある</li> - <li>自然演繹では解けるけれど lambda term で書き直す</li> - <li>Haskell では定義できるけれど Agda で証明できない</li> + <li>プログラムの変更を Monad で表す</li> + <li>プログラムの変更時に変更前のプログラムも残したまま変更する</li> + <li>全てのバージョンのプログラムを同時に実行できる</li> + <li>デバッグやテストと組み合せることでバグを見付けたい</li> + <li>実行系と検証系を同時に走らせることもできる</li> </ul> @@ -171,7 +184,27 @@ <div class="slide" id="9"><div> <section> <header> - <h1 id="section-4">つまづくポイント</h1> + <h1 id="section-4">学習コスト</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>論理, 自然演繹 -> Haskell -> Agda</li> + <li>それぞれのステップに壁がある</li> + <li>論理とプログラム間で変換できないなど</li> + <li>自然演繹では解けるけれど lambda term で書き直す</li> + <li>Haskell では定義できるけれど Agda で証明できない</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="10"><div> + <section> + <header> + <h1 id="section-5">つまづくポイント</h1> </header> <!-- _S9SLIDE_ --> @@ -191,10 +224,10 @@ </section> </div></div> -<div class="slide" id="10"><div> +<div class="slide" id="11"><div> <section> <header> - <h1 id="section-5">つまづきをどう解決するか</h1> + <h1 id="section-6">つまづきをどう解決するか</h1> </header> <!-- _S9SLIDE_ --> @@ -203,12 +236,59 @@ <li>論理とプログラムの対応を見えるようにする <ul> <li>Agda は対話的に項を書き換えることができる</li> - <li>どこでつまづいても情報が手に入るようにしたい</li> + <li>どこでつまづいても情報が手に入るようにしたい + <ul> + <li>論理側でも、プログラム側でも、どのステップでも</li> + </ul> + </li> <li>対話的に情報を引き出す手段そのものを学ぶ</li> </ul> </li> </ul> + + + </section> +</div></div> + +<div class="slide" id="12"><div> + <section> + <header> + <h1 id="section-7">他に講義に取りいれるもの?</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>仕様記述</li> + <li>他の証明支援系 + <ul> + <li>Coq, …</li> + </ul> + </li> + <li>他の理論 + <ul> + <li>Hoare Logic, Computational Tree Logic, …</li> + </ul> + </li> + <li>どのようなカリキュラムが良いか?</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="13"><div> + <section> + <header> + <h1 id="delta-">Delta の詳細</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>TODO…</li> +</ul> + <style> .slide.cover H2 { margin-top:72px;
--- a/slide/slide.md Wed Jan 21 17:26:23 2015 +0900 +++ b/slide/slide.md Wed Jan 21 20:26:55 2015 +0900 @@ -7,19 +7,29 @@ * 大学ではどんなことをやっているか(講義, イベント, 研究) * 講義などでつまづくポイント * つまづきの解決策 +* どのような講義をするべきか? -# 講義で紹介する形式手法 +# 講義で使用している形式手法 +* 仕様記述 + * UML * model checking 的なアプローチ + * Java Path Finder * 証明的なアプローチ + * Haskell, Agda + +# 仕様記述 +* モデリングと設計 の講義 +* iOS Application を作成する +* ユースケース図やクラス図を使って仕様を考える # model checking 的なアプローチ -* Operationg System の講義 +* [Operationg System](http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/os/index.html) の講義 * Process/Thread Scheduling を考えた時に * Dead Lock を起こすような Scheduling を実際に書いて実行させる * Java Path Finder で Thread の実行順序を網羅的に実行する # 証明的なアプローチ -* ソフトウェア工学 の講義 +* [ソフトウェア工学](http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/index.html) の講義 * 集合, 論理, 関数, 自然演繹による証明 * 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明 * Haskell : 自然演繹と lambda calculus @@ -28,20 +38,21 @@ # Agda による証明を解説した例 * Open Source Conference -* ソフトウェア工学で学んだ Agda の使い方を発表 +* ソフトウェア工学で学んだ Agda を [Agda 入門](http://ie.u-ryukyu.ac.jp/~e115763/slides/events/osc2014/slide.html)として発表 * Agda で SystemT の Nat の加法の交換法則を解説 -* ほとんどが定義の解説に時間を取られてしまう +* 定義の解説にほとんどの時間を取られてしまう # 圏によるプログラムの形式化 * プログラムの変更を Monad で表す * プログラムの変更時に変更前のプログラムも残したまま変更する * 全てのバージョンのプログラムを同時に実行できる -* デバッグやテストと組み合せることでバグ +* デバッグやテストと組み合せることでバグを見付けたい * 実行系と検証系を同時に走らせることもできる # 学習コスト * 論理, 自然演繹 -> Haskell -> Agda * それぞれのステップに壁がある +* 論理とプログラム間で変換できないなど * 自然演繹では解けるけれど lambda term で書き直す * Haskell では定義できるけれど Agda で証明できない @@ -57,8 +68,20 @@ * 論理とプログラムの対応を見えるようにする * Agda は対話的に項を書き換えることができる * どこでつまづいても情報が手に入るようにしたい + * 論理側でも、プログラム側でも、どのステップでも * 対話的に情報を引き出す手段そのものを学ぶ +# 他に講義に取りいれるもの? +* 仕様記述 +* 他の証明支援系 + * Coq, ... +* 他の理論 + * Hoare Logic, Computational Tree Logic, ... +* どのようなカリキュラムが良いか? + +# Delta の詳細 +* TODO... + <style> .slide.cover H2 { margin-top:72px;