Mercurial > hg > Papers > 2015 > atton-sigse
view slide/slide.md @ 49:fc10d834c3c9
Add slide for winter workshop
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 Jan 2015 16:59:03 +0900 |
parents | |
children | ba3003b56804 |
line wrap: on
line source
title: 形式手法を広めるには author: 河野真治 <br> 比嘉健太 profile: 琉球大学工学部情報工学科 lang: Japanese # Agenda * 大学ではどんなことをやっているか(講義, イベント, 研究) * 講義などを通して思う教育カリキュラムに必要なもの * 改善案 # 講義で紹介する形式手法 * UML (いれる?) * model checking 的なアプローチ * 証明的なアプローチ # UML (いれる?) * モデリングと設計 * iOS Application を作成する * UML で class をモデリングする # model checking 的なアプローチ * Operationg System の講義 * Process/Thread Scheduling を考えた時に * Dead Lock を起こすような Scheduling を実際に書いて実行させる * Java Path Finder で Thread の実行順序を網羅的に実行する # 証明的なアプローチ * ソフトウェア工学 の講義 * 集合, 論理, 関数, 自然演繹による証明 * 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明 * Haskell : 自然演繹と lambda calculus * Agda : Data type に対する証明 (Product, Sum, List, Functor, Monad ...) * Agda : SystemT を使った自然数に対する演算の証明 # Agda による証明を解説した例 * Open Source Conference * ソフトウェア工学で学んだ Agda の使い方を発表 * Agda で SystemT の Nat の加法の交換法則を解説 * ほとんどが定義の解説に時間を取られてしまう # 圏によるプログラムの形式化 * プログラムの変更を Monad で表す * プログラムの変更時に変更前のプログラムも残したまま変更する * 全てのバージョンのプログラムを同時に実行できる * デバッグやテストと組み合せることでバグ * 実行系と検証系を同時に走らせることもできる # 学習コスト * 論理, 自然演繹 -> Haskell -> Agda * それぞれのステップに壁がある * 自然演繹では解けるけれど lambda term で書き直す * Haskell では定義できるけれど Agda で証明できない # つまづくポイント * Haskell -> Agda の壁を考える * コードを書いてる人なら型を合わせることは分かる * 型によって証明を書くことに繋げるには? * プログラムと論理の対応を把握してもらう必要がある * どうしたら把握してもらえるか? # つまづきをどう解決するか * 書き続ける * 論理とプログラムの対応を見えるようにする * Agda は対話的に項を書き換えることができる * どこでつまづいても情報が手に入るようにしたい * 対話的に情報を引き出す手段を知る <style> .slide.cover H2 { font-size:72px; } .slide.cover H3#author { margin-top:72px; font-size:42px; } </style> <!-- vim: set filetype=markdown.slide: -->