Mercurial > hg > Papers > 2020 > ryokka-master
changeset 14:19ab6b8055ea
fix slide
author | ryokka |
---|---|
date | Wed, 12 Feb 2020 05:02:27 +0900 |
parents | e8655e0264b8 |
children | 36fb80fdcc3e |
files | paper/master_paper.pdf paper/master_paper.tex slide/Makefile slide/master-slide.html slide/master-slide.md slide/slide.html slide/slide.md slide/slide.mm slide/slide.pdf.html |
diffstat | 9 files changed, 3010 insertions(+), 780 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/master_paper.tex Tue Feb 11 02:31:26 2020 +0900 +++ b/paper/master_paper.tex Wed Feb 12 05:02:27 2020 +0900 @@ -19,7 +19,7 @@ \usepackage{type1cm} \usepackage[usenames]{color} \usepackage{ulem} -\usepackage{lstlinebgrd} +%% \usepackage{lstlinebgrd} \jtitle{Continuation based C での Hoare Logic を用いた仕様記述と検証} %% \etitle{Hoare Logic based Specification and Verification in Continuation based C}
--- a/slide/Makefile Tue Feb 11 02:31:26 2020 +0900 +++ b/slide/Makefile Wed Feb 12 05:02:27 2020 +0900 @@ -5,7 +5,7 @@ .PHONY : all clean remake all: - slideshow build $(TARGET).md -t s6cr --h2 + slideshow build $(TARGET).md -t s6cr open $(TARGET).html clean:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/master-slide.html Wed Feb 12 05:02:27 2020 +0900 @@ -0,0 +1,524 @@ +<!DOCTYPE html> + +<html lang="en"> + +<head> + <meta charset="utf-8"> + <meta http-equiv="X-UA-Compatible" content="IE=edge"> + <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=no"> + <meta name="apple-mobile-web-app-capable" content="yes"> + <meta name="apple-mobile-web-app-status-bar-style" content="black"> + <meta name="mobile-web-app-capable" content="yes"> + <title> + Continuation Based C の Hoare Logic を用いた仕様記述と検証 - CodiMD + </title> + <link rel="icon" type="image/png" href="http://hackmd.cr.ie.u-ryukyu.ac.jp/favicon.png"> + <link rel="apple-touch-icon" href="http://hackmd.cr.ie.u-ryukyu.ac.jp/apple-touch-icon.png"> + + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.4.0/css/bootstrap.min.css" integrity="sha256-H0KfTigpUV+0/5tn2HXC0CPwhhDhWgSawJdnFd0CGCo=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fork-awesome/1.1.3/css/fork-awesome.min.css" integrity="sha256-ZhApazu+kejqTYhMF+1DzNKjIzP7KXu6AzyXcC1gMus=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/ionicons/2.0.1/css/ionicons.min.css" integrity="sha256-3iu9jgsy9TpTwXKb7bNQzqWekRX7pPK+2OLj3R922fo=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/prism/1.5.1/themes/prism.min.css" integrity="sha256-vtR0hSWRc3Tb26iuN2oZHt3KRUomwTufNIf5/4oeCyg=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/styles/github-gist.min.css" integrity="sha256-tAflq+ymku3Khs+I/WcAneIlafYgDiOQ9stIHH985Wo=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/emojify.js/1.1.0/css/basic/emojify.min.css" integrity="sha256-UOrvMOsSDSrW6szVLe8ZDZezBxh5IoIfgTwdNDgTjiU=" crossorigin="anonymous" /> + <style> + @import url(https://fonts.googleapis.com/css?family=Source+Sans+Pro:400,400italic,600,600italic,300italic,300|Source+Serif+Pro|Source+Code+Pro:400,300,500&subset=latin,latin-ext);.markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;font-size:16px;line-height:1.5;word-wrap:break-word}.markdown-body:after,.markdown-body:before{display:table;content:""}.markdown-body:after{clear:both}.markdown-body>:first-child{margin-top:0!important}.markdown-body>:last-child{margin-bottom:0!important}.markdown-body a:not([href]){color:inherit;text-decoration:none}.markdown-body .absent{color:#c00}.markdown-body .anchor{float:left;padding-right:4px;margin-left:-20px;line-height:1}.markdown-body .anchor:focus{outline:none}.markdown-body blockquote,.markdown-body dl,.markdown-body ol,.markdown-body p,.markdown-body pre,.markdown-body table,.markdown-body ul{margin-top:0;margin-bottom:16px}.markdown-body hr{height:.25em;padding:0;margin:24px 0;background-color:#e7e7e7;border:0}.markdown-body blockquote{padding:0 1em;color:#777;border-left:.25em solid #ddd}.night .markdown-body blockquote{color:#bcbcbc}.markdown-body blockquote>:first-child{margin-top:0}.markdown-body blockquote>:last-child{margin-bottom:0}.markdown-body .loweralpha{list-style-type:lower-alpha}.markdown-body h1,.markdown-body h2,.markdown-body h3,.markdown-body h4,.markdown-body h5,.markdown-body h6{margin-top:24px;margin-bottom:16px;font-weight:600;line-height:1.25}.night .markdown-body h1,.night .markdown-body h2,.night .markdown-body h3,.night .markdown-body h4,.night .markdown-body h5,.night .markdown-body h6{color:#ddd}.markdown-body h1 .fa-link,.markdown-body h2 .fa-link,.markdown-body h3 .fa-link,.markdown-body h4 .fa-link,.markdown-body h5 .fa-link,.markdown-body h6 .fa-link{color:#000;vertical-align:middle;visibility:hidden;font-size:16px}.night .markdown-body h1 .fa-link,.night .markdown-body h2 .fa-link,.night .markdown-body h3 .fa-link,.night .markdown-body h4 .fa-link,.night .markdown-body h5 .fa-link,.night .markdown-body h6 .fa-link{color:#fff}.markdown-body h1:hover .anchor,.markdown-body h2:hover .anchor,.markdown-body h3:hover .anchor,.markdown-body h4:hover .anchor,.markdown-body h5:hover .anchor,.markdown-body h6:hover .anchor{text-decoration:none}.markdown-body h1:hover .anchor .fa-link,.markdown-body h2:hover .anchor .fa-link,.markdown-body h3:hover .anchor .fa-link,.markdown-body h4:hover .anchor .fa-link,.markdown-body h5:hover .anchor .fa-link,.markdown-body h6:hover .anchor .fa-link{visibility:visible}.markdown-body h1 code,.markdown-body h1 tt,.markdown-body h2 code,.markdown-body h2 tt,.markdown-body h3 code,.markdown-body h3 tt,.markdown-body h4 code,.markdown-body h4 tt,.markdown-body h5 code,.markdown-body h5 tt,.markdown-body h6 code,.markdown-body h6 tt{font-size:inherit}.markdown-body h1{font-size:2em}.markdown-body h1,.markdown-body h2{padding-bottom:.3em;border-bottom:1px solid #eee}.markdown-body h2{font-size:1.5em}.markdown-body h3{font-size:1.25em}.markdown-body h4{font-size:1em}.markdown-body h5{font-size:.875em}.markdown-body h6{font-size:.85em;color:#777}.markdown-body ol,.markdown-body ul{padding-left:2em}.markdown-body ol.no-list,.markdown-body ul.no-list{padding:0;list-style-type:none}.markdown-body ol ol,.markdown-body ol ul,.markdown-body ul ol,.markdown-body ul ul{margin-top:0;margin-bottom:0}.markdown-body li>p{margin-top:16px}.markdown-body li+li{margin-top:.25em}.markdown-body dl{padding:0}.markdown-body dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:700}.markdown-body dl dd{padding:0 16px;margin-bottom:16px}.markdown-body table{display:block;width:100%;overflow:auto;word-break:normal;word-break:keep-all}.markdown-body table th{font-weight:700}.markdown-body table td,.markdown-body table th{padding:6px 13px;border:1px solid #ddd}.markdown-body table tr{background-color:#fff;border-top:1px solid #ccc}.night .markdown-body table tr{background-color:#5f5f5f}.markdown-body table tr:nth-child(2n){background-color:#f8f8f8}.night .markdown-body table tr:nth-child(2n){background-color:#4f4f4f}.markdown-body img{max-width:100%;box-sizing:content-box;background-color:#fff}.markdown-body img[align=right]{padding-left:20px}.markdown-body img[align=left]{padding-right:20px}.markdown-body .emoji{max-width:none;vertical-align:text-top;background-color:transparent}.markdown-body span.frame{display:block;overflow:hidden}.markdown-body span.frame>span{display:block;float:left;width:auto;padding:7px;margin:13px 0 0;overflow:hidden;border:1px solid #ddd}.markdown-body span.frame span img{display:block;float:left}.markdown-body span.frame span span{display:block;padding:5px 0 0;clear:both;color:#333}.markdown-body span.align-center{display:block;overflow:hidden;clear:both}.markdown-body span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}.markdown-body span.align-center span img{margin:0 auto;text-align:center}.markdown-body span.align-right{display:block;overflow:hidden;clear:both}.markdown-body span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}.markdown-body span.align-right span img{margin:0;text-align:right}.markdown-body span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}.markdown-body span.float-left span{margin:13px 0 0}.markdown-body span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}.markdown-body span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}.markdown-body code,.markdown-body tt{padding:.2em 0;margin:0;font-size:85%;background-color:rgba(0,0,0,.04);border-radius:3px}.night .markdown-body code,.night .markdown-body tt{color:#eee;background-color:hsla(0,0%,90.2%,.36)}.markdown-body code:after,.markdown-body code:before,.markdown-body tt:after,.markdown-body tt:before{letter-spacing:-.2em;content:"\A0"}.markdown-body code br,.markdown-body tt br{display:none}.markdown-body del code{text-decoration:inherit}.markdown-body pre{word-wrap:normal}.markdown-body pre>code{padding:0;margin:0;font-size:100%;word-break:normal;white-space:pre;background:transparent;border:0}.markdown-body .highlight{margin-bottom:16px}.markdown-body .highlight pre{margin-bottom:0;word-break:normal}.markdown-body .highlight pre,.markdown-body pre{padding:16px;overflow:auto;font-size:85%;line-height:1.45;background-color:#f7f7f7;border-radius:3px}.markdown-body pre code,.markdown-body pre tt{display:inline;max-width:auto;padding:0;margin:0;overflow:visible;line-height:inherit;word-wrap:normal;background-color:transparent;border:0}.markdown-body pre code:after,.markdown-body pre code:before,.markdown-body pre tt:after,.markdown-body pre tt:before{content:normal}.markdown-body .csv-data td,.markdown-body .csv-data th{padding:5px;overflow:hidden;font-size:12px;line-height:1;text-align:left;white-space:nowrap}.markdown-body .csv-data .blob-line-num{padding:10px 8px 9px;text-align:right;background:#fff;border:0}.markdown-body .csv-data tr{border-top:0}.markdown-body .csv-data th{font-weight:700;background:#f8f8f8;border-top:0}.markdown-body kbd{display:inline-block;padding:3px 5px;font-size:11px;line-height:10px;color:#555;vertical-align:middle;background-color:#fcfcfc;border:1px solid;border-color:#ccc #ccc #bbb;border-radius:3px;box-shadow:inset 0 -1px 0 #bbb}.news .alert .markdown-body blockquote{padding:0 0 0 40px;border:0}.activity-tab .news .alert .commits,.activity-tab .news .markdown-body blockquote{padding-left:0}.task-list-item{list-style-type:none}.task-list-item label{font-weight:400}.task-list-item.enabled label{cursor:pointer}.task-list-item+.task-list-item{margin-top:3px}.task-list-item-checkbox{float:left;margin:.31em 0 .2em -1.3em!important;vertical-align:middle;cursor:default!important}.markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;padding-top:40px;padding-bottom:40px;max-width:758px;overflow:visible!important}.markdown-body pre{border:inherit!important}.night .markdown-body pre{filter:invert(100%)}.markdown-body code{color:inherit!important}.markdown-body pre code .wrapper{display:-webkit-inline-flex;display:-moz-inline-flex;display:-ms-inline-flex;display:-o-inline-flex;display:inline-flex}.markdown-body pre code .gutter{float:left;overflow:hidden;-webkit-user-select:none;user-select:none}.markdown-body pre code .gutter.linenumber{text-align:right;position:relative;display:inline-block;cursor:default;z-index:4;padding:0 8px 0 0;min-width:20px;box-sizing:content-box;color:#afafaf!important;border-right:3px solid #6ce26c!important}.markdown-body pre code .gutter.linenumber>span:before{content:attr(data-linenumber)}.markdown-body pre code .code{float:left;margin:0 0 0 16px}.markdown-body .gist .line-numbers{border-left:none;border-top:none;border-bottom:none}.markdown-body .gist .line-data{border:none}.markdown-body .gist table{border-spacing:0;border-collapse:inherit!important}.night .markdown-body .gist table tr:nth-child(2n){background-color:#ddd}.markdown-body code[data-gist-id]{background:none;padding:0;filter:invert(100%)}.markdown-body code[data-gist-id]:after,.markdown-body code[data-gist-id]:before{content:""}.markdown-body code[data-gist-id] .blob-num{border:unset}.markdown-body code[data-gist-id] table{overflow:unset;margin-bottom:unset}.markdown-body code[data-gist-id] table tr{background:unset}.markdown-body[dir=rtl] pre{direction:ltr}.markdown-body[dir=rtl] code{direction:ltr;unicode-bidi:embed}.markdown-body .alert>p{margin-bottom:0}.markdown-body pre.abc,.markdown-body pre.flow-chart,.markdown-body pre.graphviz,.markdown-body pre.mermaid,.markdown-body pre.sequence-diagram{text-align:center;background-color:inherit;border-radius:0;white-space:inherit}.night .markdown-body pre.graphviz .graph>polygon{fill:#333}.night .markdown-body pre.mermaid .sectionTitle,.night .markdown-body pre.mermaid .titleText,.night .markdown-body pre.mermaid text{fill:#fff}.markdown-body pre.abc>code,.markdown-body pre.flow-chart>code,.markdown-body pre.graphviz>code,.markdown-body pre.mermaid>code,.markdown-body pre.sequence-diagram>code{text-align:left}.markdown-body pre.abc>svg,.markdown-body pre.flow-chart>svg,.markdown-body pre.graphviz>svg,.markdown-body pre.mermaid>svg,.markdown-body pre.sequence-diagram>svg{max-width:100%;height:100%}.night .markdown-body .abc path{fill:#eee}.night .markdown-body .abc path.note_selected{fill:##4DD0E1}.night tspan{fill:#fefefe}.night pre rect{fill:transparent}.night pre.flow-chart path,.night pre.flow-chart rect{stroke:#fff}.markdown-body pre>code.wrap{white-space:pre-wrap;white-space:-moz-pre-wrap;white-space:-pre-wrap;white-space:-o-pre-wrap;word-wrap:break-word}.markdown-body .alert>p,.markdown-body .alert>ul{margin-bottom:0}.markdown-body summary{display:list-item}.markdown-body summary:focus{outline:none}.markdown-body details summary{cursor:pointer}.markdown-body details:not([open])>:not(summary){display:none}.markdown-body figure{margin:1em 40px}.markdown-body img{background-color:transparent}.vimeo,.youtube{cursor:pointer;display:table;text-align:center;background-position:50%;background-repeat:no-repeat;background-size:contain;background-color:#000;overflow:hidden}.vimeo,.youtube{position:relative;width:100%}.youtube{padding-bottom:56.25%}.vimeo img{width:100%;object-fit:contain;z-index:0}.youtube img{object-fit:cover;z-index:0}.vimeo iframe,.youtube iframe,.youtube img{width:100%;height:100%;position:absolute;top:0;left:0}.vimeo iframe,.youtube iframe{vertical-align:middle;z-index:1}.vimeo .icon,.youtube .icon{position:absolute;height:auto;width:auto;top:50%;left:50%;transform:translate(-50%,-50%);color:#fff;opacity:.3;-webkit-transition:opacity .2s;transition:opacity .2s;z-index:0}.vimeo:hover .icon,.youtube:hover .icon{opacity:.6;-webkit-transition:opacity .2s;transition:opacity .2s}.slideshare .inner,.speakerdeck .inner{position:relative;width:100%}.slideshare .inner iframe,.speakerdeck .inner iframe{position:absolute;top:0;bottom:0;left:0;right:0;width:100%;height:100%}.MJX_Assistive_MathML{display:none}.ui-infobar{position:relative;z-index:2;max-width:758px;margin-top:25px;margin-bottom:-25px;color:#777}.toc .invisable-node{list-style-type:none}.ui-toc{position:fixed;bottom:20px;z-index:10000}.ui-toc-label{opacity:.3;background-color:#ccc;border:none}.ui-toc-label,.ui-toc .open .ui-toc-label{-webkit-transition:opacity .2s;transition:opacity .2s}.ui-toc .open .ui-toc-label{opacity:1;color:#fff}.ui-toc-label:focus{opacity:.3;background-color:#ccc;color:#000}.ui-toc-label:hover{opacity:1;background-color:#ccc;-webkit-transition:opacity .2s;transition:opacity .2s}.ui-toc-dropdown{margin-top:23px;margin-bottom:20px;padding-left:10px;padding-right:10px;max-width:45vw;width:25vw;max-height:70vh;overflow:auto;text-align:inherit}.ui-toc-dropdown>.toc{max-height:calc(70vh - 100px);overflow:auto}.ui-toc-dropdown[dir=rtl] .nav{padding-right:0;letter-spacing:.0029em}.ui-toc-dropdown a{overflow:hidden;text-overflow:ellipsis;white-space:pre}.ui-toc-dropdown .nav>li>a{display:block;padding:4px 20px;font-size:13px;font-weight:500;color:#767676}.ui-toc-dropdown .nav>li:first-child:last-child>ul,.ui-toc-dropdown .toc.expand ul{display:block}.ui-toc-dropdown .nav>li>a:focus,.ui-toc-dropdown .nav>li>a:hover{padding-left:19px;color:#000;text-decoration:none;background-color:transparent;border-left:1px solid #000}.night .ui-toc-dropdown .nav>li>a:focus,.night .ui-toc-dropdown .nav>li>a:hover{color:#fff;border-left-color:#fff}.ui-toc-dropdown[dir=rtl] .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav>li>a:hover{padding-right:19px;border-left:none;border-right:1px solid #000}.ui-toc-dropdown .nav>.active:focus>a,.ui-toc-dropdown .nav>.active:hover>a,.ui-toc-dropdown .nav>.active>a{padding-left:18px;font-weight:700;color:#000;background-color:transparent;border-left:2px solid #000}.night .ui-toc-dropdown .nav>.active:focus>a,.night .ui-toc-dropdown .nav>.active:hover>a,.night .ui-toc-dropdown .nav>.active>a{color:#fff;border-left:2px solid #fff}.ui-toc-dropdown[dir=rtl] .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav>.active>a{padding-right:18px;border-left:none;border-right:2px solid #000}.ui-toc-dropdown .nav .nav{display:none;padding-bottom:10px}.ui-toc-dropdown .nav>.active>ul{display:block}.ui-toc-dropdown .nav .nav>li>a{padding-top:1px;padding-bottom:1px;padding-left:30px;font-size:12px;font-weight:400}.night .ui-toc-dropdown .nav>li>a{color:#aaa}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a{padding-right:30px}.ui-toc-dropdown .nav .nav>li>ul>li>a{padding-top:1px;padding-bottom:1px;padding-left:40px;font-size:12px;font-weight:400}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a{padding-right:40px}.ui-toc-dropdown .nav .nav>li>a:focus,.ui-toc-dropdown .nav .nav>li>a:hover{padding-left:29px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:hover{padding-right:29px}.ui-toc-dropdown .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown .nav .nav>li>ul>li>a:hover{padding-left:39px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:hover{padding-right:39px}.ui-toc-dropdown .nav .nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>a{padding-left:28px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>a{padding-right:28px}.ui-toc-dropdown .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active>a{padding-left:38px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active>a{padding-right:38px}.markdown-body[lang^=ja]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,Hiragino Kaku Gothic Pro,"\30D2\30E9\30AE\30CE\89D2\30B4 Pro W3",Osaka,Meiryo,"\30E1\30A4\30EA\30AA",MS Gothic,"\FF2D\FF33 \30B4\30B7\30C3\30AF",sans-serif,Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol}.ui-toc-dropdown[lang^=ja]{font-family:Source Sans Pro,Helvetica,Arial,Meiryo UI,MS PGothic,"\FF2D\FF33 \FF30\30B4\30B7\30C3\30AF",sans-serif}.markdown-body[lang=zh-tw]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,PingFang TC,Microsoft JhengHei,"\5FAE\8EDF\6B63\9ED1",sans-serif,Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol}.ui-toc-dropdown[lang=zh-tw]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft JhengHei UI,"\5FAE\8EDF\6B63\9ED1UI",sans-serif}.markdown-body[lang=zh-cn]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Roboto,Helvetica Neue,Helvetica,Arial,PingFang SC,Microsoft YaHei,"\5FAE\8F6F\96C5\9ED1",sans-serif,Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol}.ui-toc-dropdown[lang=zh-cn]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft YaHei UI,"\5FAE\8F6F\96C5\9ED1UI",sans-serif}.ui-affix-toc{position:fixed;top:0;max-width:15vw;max-height:70vh;overflow:auto}.back-to-top,.expand-toggle,.go-to-bottom{display:block;padding:4px 10px;margin-top:10px;margin-left:10px;font-size:12px;font-weight:500;color:#999}.back-to-top:focus,.back-to-top:hover,.expand-toggle:focus,.expand-toggle:hover,.go-to-bottom:focus,.go-to-bottom:hover{color:#563d7c;text-decoration:none}.back-to-top,.go-to-bottom{margin-top:0}.ui-user-icon{width:20px;height:20px;display:block;border-radius:3px;margin-top:2px;margin-bottom:2px;margin-right:5px;background-position:50%;background-repeat:no-repeat;background-size:contain}.ui-user-icon.small{width:18px;height:18px;display:inline-block;vertical-align:middle;margin:0 0 .2em}small span{line-height:22px}small .dropdown{display:inline-block}small .dropdown a:focus,small .dropdown a:hover{text-decoration:none}.unselectable{-moz-user-select:none;-khtml-user-select:none;-webkit-user-select:none;-o-user-select:none;user-select:none}.night .navbar{background:#333;border-bottom-color:#333;color:#eee}.night .navbar a{color:#eee}@media print{blockquote,div,img,pre,table{page-break-inside:avoid!important}a[href]:after{font-size:12px!important}}.markdown-body.slides{position:relative;z-index:1;color:#222}.markdown-body.slides:before{content:"";display:block;position:absolute;top:0;left:0;right:0;bottom:0;z-index:-1;background-color:currentColor;box-shadow:0 0 0 50vw}.markdown-body.slides section[data-markdown]{position:relative;margin-bottom:1.5em;background-color:#fff;text-align:center}.markdown-body.slides section[data-markdown] code{text-align:left}.markdown-body.slides section[data-markdown]:before{content:"";display:block;padding-bottom:56.23%}.markdown-body.slides section[data-markdown]>div:first-child{position:absolute;top:50%;left:1em;right:1em;transform:translateY(-50%);max-height:100%;overflow:hidden}.markdown-body.slides section[data-markdown]>ul{display:inline-block}.markdown-body.slides>section>section+section:after{content:"";position:absolute;top:-1.5em;right:1em;height:1.5em;border:3px solid #777}body{font-smoothing:subpixel-antialiased!important;-webkit-font-smoothing:subpixel-antialiased!important;-moz-osx-font-smoothing:auto!important;text-shadow:0 0 1em transparent,1px 1px 1.2px rgba(0,0,0,.004);-webkit-overflow-scrolling:touch;font-family:Source Sans Pro,Helvetica,Arial,sans-serif;letter-spacing:.025em}.focus,:focus{outline:none!important}::-moz-focus-inner{border:0!important}body.modal-open{overflow-y:auto;padding-right:0!important} + </style> + <!-- HTML5 shim and Respond.js for IE8 support of HTML5 elements and media queries --> + <!-- WARNING: Respond.js doesn't work if you view the page via file:// --> + <!--[if lt IE 9]> + <script src="https://cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv.min.js" integrity="sha256-3Jy/GbSLrg0o9y5Z5n1uw0qxZECH7C6OQpVBgNFYa0g=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/respond.js/1.4.2/respond.min.js" integrity="sha256-g6iAfvZp+nDQ2TdTR/VVKJf3bGro4ub5fvWSWVRi2NE=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/es5-shim/4.5.9/es5-shim.min.js" integrity="sha256-8E4Is26QH0bD52WoQpcB+R/tcWQtpzlCojrybUd7Mxo=" crossorigin="anonymous"></script> + <![endif]--> +</head> + +<body> + <div id="doc" class="markdown-body container-fluid"><h1 id="Continuation-Based-C-の-Hoare-Logic-を用いた仕様記述と検証"><a class="anchor hidden-xs" href="#Continuation-Based-C-の-Hoare-Logic-を用いた仕様記述と検証" title="Continuation-Based-C-の-Hoare-Logic-を用いた仕様記述と検証"><i class="fa fa-link"></i></a>Continuation Based C の Hoare Logic を用いた仕様記述と検証</h1><p>琉球大学大学院 : 並列信頼研究室<br> +外間 政尊</p><hr><h2 id="OS-の検証技術としての-Hoare-Logic-の問題点"><a class="anchor hidden-xs" href="#OS-の検証技術としての-Hoare-Logic-の問題点" title="OS-の検証技術としての-Hoare-Logic-の問題点"><i class="fa fa-link"></i></a>OS の検証技術としての Hoare Logic の問題点</h2><ul> +<li> +<p>OS やアプリケーションの信頼性は重要な課題</p> +</li> +<li> +<p>信頼性を上げるために仕様の検証が必要</p> +</li> +<li> +<p>検証にはモデル検査や<strong>定理証明</strong>などが存在する</p> +</li> +<li> +<p>また、仕様検証の手法として <strong>Hoare Logic</strong> がある<br> +-通常の関数でも実行する前に必要な引数があって何らかの出力がある</p> +<ul> +<li>Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ</li> +</ul> +</li> +<li> +<p>Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等)</p> +</li> +</ul><hr><h2 id="Hoare-Logic-をベースにした-Gears-単位での検証"><a class="anchor hidden-xs" href="#Hoare-Logic-をベースにした-Gears-単位での検証" title="Hoare-Logic-をベースにした-Gears-単位での検証"><i class="fa fa-link"></i></a>Hoare Logic をベースにした Gears 単位での検証</h2><ul> +<li>当研究室では 処理の単位を <strong>CodeGear</strong>、データの単位を <strong>DataGear</strong> としてプログラムを記述する手法を提案</li> +<li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む</li> +<li>CodeGear は継続を用いて次の CodeGear に接続される</li> +<li>定理証明支援機の Agda 上で Gears 単位を用いた検証を行う</li> +<li>本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する</li> +</ul><hr><h2 id="Agda"><a class="anchor hidden-xs" href="#Agda" title="Agda"><i class="fa fa-link"></i></a>Agda</h2><p>Agda は関数型言語</p><pre><code class="AGAD hljs"> name : <span class="hljs-built_in">type</span> + name = value +</code></pre><p>関数には型と定義を与える<br> +型は <strong>:</strong> で、 値は <strong>=</strong> で与える<br> +仮定なしに使えるのは Set のみ</p><p>構成要素としては以下の3種類</p><ol> +<li>関数 +<ul> +<li>型は(A : Set かつ B : Set のとき) A → B</li> +<li>値は(x : A かつ y : B) λ x → y</li> +</ul> +</li> +<li>record</li> +<li>data</li> +</ol><hr><h2 id="Agda-の-record-とその例-∧"><a class="anchor hidden-xs" href="#Agda-の-record-とその例-∧" title="Agda-の-record-とその例-∧"><i class="fa fa-link"></i></a>Agda の record とその例 ∧</h2><p>導入は2つのものが同時に存在すること</p><pre><code> A B +------------ + A ∧ B +</code></pre><p>除去は名前を区別する必要がある</p><pre><code> A ∧ B A ∧ B + --------- pi1 --------- pi2 + A B +</code></pre><p>A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B<br> +Agda ではこのような同時に存在する型を <strong>record</strong> で書く</p><pre><code class="AGDA hljs"> record _∧_ (A B : <span class="hljs-keyword">Set</span>) : <span class="hljs-keyword">Set</span> + <span class="hljs-keyword">field</span> + pi1 : A + pi2 : B +</code></pre><p>_∧_ は中間記法、変数が入る位置を _ で示せる<br> +実際の構築は x : A かつ y : B のとき</p><pre><code class="AGDA hljs"><span class="hljs-attribute">createAnd</span> : (A : Set) → (B : Set) → A ∧ B +createAnd x y = record {<span class="hljs-attribute">pi1</span> = x ; <span class="hljs-attribute">pi2</span> = y} +</code></pre><p>のように記述する<br> +C 言語での構造体のようなもの</p><p>A や B に論理式が入ると2つのものが同時に成り立つ証明ができる</p><hr><h2 id="Agda-の-data-とその例-Sum"><a class="anchor hidden-xs" href="#Agda-の-data-とその例-Sum" title="Agda-の-data-とその例-Sum"><i class="fa fa-link"></i></a>Agda の data とその例 Sum</h2><p>導入<br> +一つでも存在すること</p><pre><code> A B + ----------- p1 ---------- p2 + A ∨ B A ∨ B +</code></pre><p>除去<br> +A → C か B → C のとき C</p><pre><code> A B + : : + A ∨ B C C + ------------------------ + C +</code></pre><p>A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B<br> +どちらかが成り立つ型を <strong>data</strong> で書く\</p><pre><code class="AGDA hljs"> data _∨_ (A B : <span class="hljs-keyword">Set</span>) : <span class="hljs-keyword">Set</span> <span class="hljs-keyword">where</span> + p1 : A → A ∨ B + p2 : B → A ∨ B +</code></pre><p>のように記述できる<br> +C 言語での union のようなもの<br> +p1、 p2 は case 文みたいな感じ</p><hr><h2 id="Hoare-Logic"><a class="anchor hidden-xs" href="#Hoare-Logic" title="Hoare-Logic"><i class="fa fa-link"></i></a>Hoare Logic</h2><p>Hoare Logic はプログラム検証の手法<br> +事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ</p><p>これは <strong>{ P } C { Q }</strong> の形で表され、Hoare Triple と呼ばれる</p><p>今回は以下のような while program を検証する</p><p>n = 10 となっているが検証では n は任意の自然数</p><pre><code class="C hljs"> n = 10; + i = 0; + + <span class="hljs-keyword">while</span> (n>0) + { + i++; + n--; + } +</code></pre><hr><h2 id="Agda-での-Hoare-Logic"><a class="anchor hidden-xs" href="#Agda-での-Hoare-Logic" title="Agda-での-Hoare-Logic"><i class="fa fa-link"></i></a>Agda での Hoare Logic</h2><p>Hoare Logic のプログラムは Command で構成される</p><p>Comm 型は data で記述されたコマンドのデータ構造</p><p>実際に実行するには解釈して動かす関数が必要</p><p>Commを使って while program を構築する</p><pre><code class="AGDA hljs"> data Comm : <span class="hljs-keyword">Set</span> <span class="hljs-keyword">where</span> + <span class="hljs-keyword">Skip</span> : Comm + <span class="hljs-keyword">Abort</span> : Comm + PComm : PrimComm → Comm + Seq : Comm → Comm → Comm + <span class="hljs-keyword">If</span> : Cond → Comm → Comm → Comm + <span class="hljs-keyword">While</span> : Cond → Comm → Comm +</code></pre><hr><h2 id="Hoare-Logic-での-while-program"><a class="anchor hidden-xs" href="#Hoare-Logic-での-while-program" title="Hoare-Logic-での-while-program"><i class="fa fa-link"></i></a>Hoare Logic での while program</h2><p>検証する while program の擬似コード</p><pre><code class="C hljs"> n = 10; + i = 0; + + <span class="hljs-keyword">while</span> (n>0) + { + i++; + n--; + } +</code></pre><p>コマンドで構成した while program</p><pre><code class="AGDA hljs"> program : ℕ → Comm + program c1<span class="hljs-number">0</span> = + Se<span class="hljs-string">q ( PComm (λ env → record env {varn = c10})</span>) + $ Se<span class="hljs-string">q ( PComm (λ env → record env {vari = 0})</span>) + $ While (λ env → <span class="hljs-keyword">lt</span> zero (varn env ) ) + (Se<span class="hljs-string">q (PComm (λ env → record env {vari = ((vari env)</span> + <span class="hljs-number">1</span>)} )) + $ PComm (λ env → record env {varn = ((varn env) - <span class="hljs-number">1</span>)} )) +</code></pre><p>これは Hoare Logic のコマンドで以下のような構文木を記述している</p><pre><code> Seq + / \ + PComm Seq + (n=c10) / \ + PComm While + (i=0) | + Cond + (0<n) + | + Seq + / \ + PComm PComm + (i+1) (n-1) +</code></pre><hr><h2 id="Hoare-Logic-での-Command-に対応する仕様"><a class="anchor hidden-xs" href="#Hoare-Logic-での-Command-に対応する仕様" title="Hoare-Logic-での-Command-に対応する仕様"><i class="fa fa-link"></i></a>Hoare Logic での Command に対応する仕様</h2><p>Command に対応する証明がある</p><p><strong>HTProof</strong> は Hoare Triple Proof</p><p><strong>{P} Q {C}</strong> が <strong>Cond → Comm → Cond</strong> に対応している</p><pre><code class="agda hljs"> data HTProof : Cond → Comm → Cond → <span class="hljs-keyword">Set</span> <span class="hljs-keyword">where</span> +</code></pre><p>すべての Command に対応する Proof を載せると長いので<br> +必要なものだけ</p><p><br> +PrimRule は 代入のときに成り立ってほしいルール</p><p>Axiom は Triple を受け取ってすべての Env は事前の Env が正しければ コマンドを実行した後のEnv も正しくなるという命題</p><pre><code class="AGDA hljs"> <span class="hljs-selector-tag">PrimRule</span> : {<span class="hljs-attribute">bPre </span>: Cond} → {<span class="hljs-attribute">pcm </span>: PrimComm} → {<span class="hljs-attribute">bPost </span>: Cond} → + (<span class="hljs-selector-tag">pr</span> : <span class="hljs-selector-tag">Axiom</span> <span class="hljs-selector-tag">bPre</span> <span class="hljs-selector-tag">pcm</span> <span class="hljs-selector-tag">bPost</span>) → + <span class="hljs-selector-tag">HTProof</span> <span class="hljs-selector-tag">bPre</span> (<span class="hljs-selector-tag">PComm</span> <span class="hljs-selector-tag">pcm</span>) <span class="hljs-selector-tag">bPost</span> +</code></pre><p>WekeningRule は 条件を緩める規則</p><p>While コマンドなどで条件が厳しいときに同時に成り立つ異なる条件へ変更必要がある</p><p>Tautology は2つの Cond 型 bPre、 bPre’ を受け取り、 bPre が成り立つとき、 bPre’が成り立つという命題</p><pre><code class="agda hljs"> WeakeningRule : {bPre : Cond} → {bPre<span class="hljs-string">' : Cond} → {cm : Comm} → + {bPost'</span> : Cond} → {bPost : Cond} → + Tautology bPre bPre<span class="hljs-string">' → + HTProof bPre'</span> cm bPost<span class="hljs-string">' → + Tautology bPost'</span> bPost → + HTProof bPre cm bPost +</code></pre><p>SeqRule は Seqcuence が正しい順番で行われることを保証</p><p>cm1、cm2 という2つのCommを受け取ってそれらがcm1、cm2の順で実行される</p><pre><code> SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → + {cm2 : Comm} → {bPost : Cond} → + HTProof bPre cm1 bMid → + HTProof bMid cm2 bPost → + HTProof bPre (Seq cm1 cm2) bPost +</code></pre><p>WhileRule は Comm 型の cm と Cond型の bInv、 bが存在するとき、<br> +事前に</p><pre><code> WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → + HTProof (bInv and b) cm bInv → + HTProof bInv (While b cm) (bInv and neg b) +</code></pre><p>検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある</p><h2 id="Hoare-Logic-での-仕様記述"><a class="anchor hidden-xs" href="#Hoare-Logic-での-仕様記述" title="Hoare-Logic-での-仕様記述"><i class="fa fa-link"></i></a>Hoare Logic での 仕様記述</h2><p>HTProof で記述した仕様</p><p>HTProof が コマンドに対応しているのでほとんど同じ形で書けてる</p><pre><code class="AGDA hljs"> proof1 : (c1<span class="hljs-number">0</span> : ℕ) → HTProof initCond (program c1<span class="hljs-number">0</span> ) (termCond {c1<span class="hljs-number">0</span>}) + proof1 c1<span class="hljs-number">0</span> = + SeqRule {λ e → <span class="hljs-literal">true</span>} ( PrimRule (init-<span class="hljs-keyword">case</span> {c1<span class="hljs-number">0</span>} )) + $ SeqRule {λ e → Equal (varn e) c1<span class="hljs-number">0</span>} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c1<span class="hljs-number">0</span>) ∧ (Equal (vari e) <span class="hljs-number">0</span>)} lemma2 ( + WhileRule {<span class="hljs-number">_</span>} {λ e → Equal ((varn e) + (vari e)) c1<span class="hljs-number">0</span>} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv<span class="hljs-string">'} {_} {whileInv} lemma4 ) lemma5 +</span></code></pre><pre><code class="AGDA hljs"> program : ℕ → Comm + program c1<span class="hljs-number">0</span> = + Se<span class="hljs-string">q ( PComm (λ env → record env {varn = c10})</span>) + $ Se<span class="hljs-string">q ( PComm (λ env → record env {vari = 0})</span>) + $ While (λ env → <span class="hljs-keyword">lt</span> zero (varn env ) ) + (Se<span class="hljs-string">q (PComm (λ env → record env {vari = ((vari env)</span> + <span class="hljs-number">1</span>)} )) + $ PComm (λ env → record env {varn = ((varn env) - <span class="hljs-number">1</span>)} )) +</code></pre><p>proof1 は条件がつながるのに必要な条件を lemma で記述している(lemma は長いので省略)</p><p>部分正当性は示せている</p><p>全体がつながっているが証明にはなっていない</p><hr><h2 id="Hoare-Logic-での健全性の証明"><a class="anchor hidden-xs" href="#Hoare-Logic-での健全性の証明" title="Hoare-Logic-での健全性の証明"><i class="fa fa-link"></i></a>Hoare Logic での健全性の証明</h2><p>実際に正しく動作すること(健全性)を証明する必要がある</p><p>Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す</p><p>PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する</p><pre><code class="AGDA hljs"> PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost + PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +</code></pre><p>Soundness は HTProof に対応した非常に複雑な証明</p><p>HTProof を渡すと Ruleに対応した証明を行う</p><p>proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している</p><pre><code class="AGDA hljs"> proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ <span class="hljs-literal">true</span> + → (SemComm (program c10) input output) + → termCond {c10} output ≡ <span class="hljs-literal">true</span> + proofOfProgram c10 input output ic sem = + PrimSoundness (proof1 c10) input output ic sem +</code></pre><hr><h2 id="Continuation-based-C-について"><a class="anchor hidden-xs" href="#Continuation-based-C-について" title="Continuation-based-C-について"><i class="fa fa-link"></i></a>Continuation based C について</h2><p>Continuation based C (CbC) は当研究室で開発してるプログラミング言語</p><p>CbC では処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong> とする</p><p>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</p><p>Output の DataGear は次の CodeGear の Input として接続される</p><p><img src="/attachment/5e42fdea7b378d004670d2fc" alt="cgdg-small.svg"><br> +<img src="./fig/cgdg-small.svg" alt=""><br> +CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</p><p>Meta CodeGear で信頼性の検証を行う</p><hr><h2 id="Agda-での-CodeGear、-DataGear-の記述"><a class="anchor hidden-xs" href="#Agda-での-CodeGear、-DataGear-の記述" title="Agda-での-CodeGear、-DataGear-の記述"><i class="fa fa-link"></i></a>Agda での CodeGear、 DataGear の記述</h2><ul> +<li>Agda での CodeGear は継続渡しで記述された関数</li> +</ul><pre><code class="AGDA hljs"> <span class="hljs-attribute">whileTest</span> : {<span class="hljs-attribute">t</span> : Set} → (c10 : Nat) + → (Code : Env → t) → t + whileTest c10 next = next (record {<span class="hljs-attribute">varn</span> = c10 + ; <span class="hljs-attribute">vari</span> = <span class="hljs-number">0</span>} ) +</code></pre><ul> +<li>CodeGear の型は継続先を返す関数</li> +<li><strong>(Code : fa → t)</strong> は継続先</li> +<li>引数として継続先の CodeGear を受け取る</li> +</ul><hr><h2 id="CbC-での-Hoare-Logic"><a class="anchor hidden-xs" href="#CbC-での-Hoare-Logic" title="CbC-での-Hoare-Logic"><i class="fa fa-link"></i></a>CbC での Hoare Logic</h2><p>CodeGear、DataGear を用いた Hoare Logic は図のようになる<br> +<img src="/attachment/5e42baee7b378d004670d1f5" alt="hoare-cg-dg.svg"><br> +<img src="./fig/hoare-cg-dg.svg" alt=""><br> +CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる</p><p>下のコードは CodeGear、 DataGear を用いた Hoare Logic ベースの記述例である</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">whileTestPwP</span> : {<span class="hljs-attribute">l</span> : Level} {<span class="hljs-attribute">t</span> : Set l} → (c10 : ℕ) → ((env : Envc ) + → whileTestStateP s1 env → t) → t + whileTestPwP c10 next = next (whileTestP c10 ( λ env → env )) + record { <span class="hljs-attribute">pi1</span> = refl ; <span class="hljs-attribute">pi2</span> = refl } +</code></pre><hr><h2 id="CbC-での-while-program"><a class="anchor hidden-xs" href="#CbC-での-while-program" title="CbC-での-while-program"><i class="fa fa-link"></i></a>CbC での while program</h2><pre><code class="C hljs"> n = 10; + i = 0; + + <span class="hljs-keyword">while</span> (n>0) + { + i++; + n--; + } +</code></pre><p>CbC での while program</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">whileTestPCall</span> : (c10 : ℕ ) → Envc + whileTestPCall c10 = whileTestP<span class="hljs-string">' {_} {_} c10 (λ env → loopP'</span> env (λ env → env)) +</code></pre><ul> +<li>whileTestP’ が n = c10、 i = 0 の代入、 loopP’ が while loop に対応している</li> +<li>CbC での Hoare Logic 上でコマンドは CodeGear そのもの +<ul> +<li>CodeGear は Hoare Logic のコマンドより自由な記述</li> +</ul> +</li> +</ul><hr><h2 id="CbC-での-Hoare-Logic-記述"><a class="anchor hidden-xs" href="#CbC-での-Hoare-Logic-記述" title="CbC-での-Hoare-Logic-記述"><i class="fa fa-link"></i></a>CbC での Hoare Logic 記述</h2><p>CbC での Hoare Logic 記述では CodeGear が条件を受け取る</p><p>whileTestPwP は代入を行う CodeGear</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">whileTestPwP</span> : {<span class="hljs-attribute">l</span> : Level} {<span class="hljs-attribute">t</span> : Set l} → (c10 : ℕ) + → ((env : Envc ) → (vari env ≡ <span class="hljs-number">0</span>) ∧ (varn env ≡ c10 env) → t) → t + whileTestPwP c10 next = + next (whileTestP c10 ( λ env → env )) (record { <span class="hljs-attribute">pi1</span> = refl ; <span class="hljs-attribute">pi2</span> = refl }) +</code></pre><p>loopPwP’ は while loop をするための条件を持ち、ループをする CodeGear</p><p>n と (n ≡ varn env) を受け取り varn でのパターンマッチをしている</p><p>suc n の場合はループを抜けるか判断する CodeGear に継続する</p><p>更に継続先で loopPwP’ を呼ぶことで再帰的にループする</p><pre><code class="AGDA hljs"> loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → (vari env + varn env ≡ c10 env) → + (<span class="hljs-built_in">exit</span> : (env : Envc ) → (vari env ≡ c10 env) → t) → t + loopPwP' zero env refl refl <span class="hljs-built_in">exit</span> = <span class="hljs-built_in">exit</span> env refl + loopPwP' (suc n) env refl refl <span class="hljs-built_in">exit</span> = + whileLoopPwP' (suc n) env refl refl + (λ env x y → loopPwP' n env x y <span class="hljs-built_in">exit</span>) <span class="hljs-built_in">exit</span> +</code></pre><p>whileLoopPwP’ は while loop を抜けるか判断する CodeGear</p><p>loopPwP’から呼ばれている</p><pre><code class="AGDA hljs"> whileLoopPwP<span class="hljs-string">' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → (vari env + varn env ≡ c10 env) + → (next : (env : Envc ) → (pred n ≡ varn env) + → (vari env + varn env ≡ c10 env) → t) + → (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t + whileLoopPwP'</span> zero env refl refl _ <span class="hljs-built_in">exit</span> = <span class="hljs-built_in">exit</span> env refl + whileLoopPwP<span class="hljs-string">' (suc n) env refl refl next _ = + next (record env {varn = pred (varn env) ; vari = suc (vari env)}) + refl (+-suc n (vari env)) +</span></code></pre><p>conv は whileTestPwP の事後条件から while loop のための loop invaliant に変更する</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">conv</span> : (env : Envc ) → (vari env ≡ <span class="hljs-number">0</span>) /\ (varn env ≡ c10 env) + → varn env + vari env ≡ c10 env + conv e record { <span class="hljs-attribute">pi1</span> = refl ; <span class="hljs-attribute">pi2</span> = refl } = +zero +</code></pre><p>whileTestPCallwP’ は先程までの Hoare Logic の記述をつなげたもの</p><p>継続先の CodeGear に渡す条件が</p><pre><code class="AGDA hljs"> whileTestPCallwP' : (c : ℕ ) → <span class="hljs-keyword">Set</span> + whileTestPCallwP<span class="hljs-string">' c = whileTestPwP {_} {_} c ( + λ env s → loopPwP'</span> (varn env) env refl (<span class="hljs-keyword">conv</span> env s) + ( λ env s → <span class="hljs-keyword">vari</span> env ≡ c10 env ) ) +</code></pre><p>whileTestPCallwP’ では Hoare Logic の条件が接続できた</p><hr><h2 id="Hoare-Logic-をベースにした-CbC-での-while-loop"><a class="anchor hidden-xs" href="#Hoare-Logic-をベースにした-CbC-での-while-loop" title="Hoare-Logic-をベースにした-CbC-での-while-loop"><i class="fa fa-link"></i></a>Hoare Logic をベースにした CbC での while loop</h2><p>先程条件を接続した whileTestPCallwP’ を型に入れ、実際に実行してみる</p><pre><code class="AGDA hljs"> whileCallwP : (c : ℕ) → whileTestPCallwP<span class="hljs-string">' c + whileCallwP c = whileTestPwP {_} {_} c (λ env s → + loopPwP'</span> (c10 env) env (sym (pi2 s)) (conv env s) {!!}) +</code></pre><p>loopPwP’は任意の値を取ってループを行う CodeGear であった</p><p>しかし、引数で受け取った任意の自然数で実行するとループが停まらない</p><p>任意の自然数回ループする loopPwP’ が停まることを補助する loopHelper を記述した</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">loopHelper</span> : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) + → (varn env + vari env ≡ c10 env) + → loopPwP<span class="hljs-string">' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) + loopHelper zero env eq refl rewrite eq = refl + loopHelper (suc n) env eq refl rewrite eq = loopHelper n + (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) + refl (+-suc n (vari env)) +</span></code></pre><p>loopHelper を用いて記述した実行は実際に停止した</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">helperCallwP</span> : (c : ℕ) → whileTestPCallwP<span class="hljs-string">' c + helperCallwP c = whileTestPwP {_} {_} c + (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) +</span></code></pre><hr><h2 id="CbC-での-Hoare-Logic-の健全性"><a class="anchor hidden-xs" href="#CbC-での-Hoare-Logic-の健全性" title="CbC-での-Hoare-Logic-の健全性"><i class="fa fa-link"></i></a>CbC での Hoare Logic の健全性</h2><p>implies という data を用いて健全性の証明を行う</p><p>implies の型は A と B の条件を受け取る</p><p>このとき proof として A → B が存在すれば A implies B が証明できる</p><pre><code class="AGDA hljs"> data _implies_ (A B : <span class="hljs-keyword">Set</span> ) : <span class="hljs-keyword">Set</span> (succ Zero) <span class="hljs-keyword">where</span> + proof : ( A → B ) → A implies B +</code></pre><p>代入を行う CodeGear である <strong>whileTestP</strong> を実行したとき、<br> +常に真の命題 <strong>⊤</strong> と代入を終えたときの事後条件である<br> +<strong>(vari env ≡ 0) ∧ (varn env ≡ c10 env)</strong><br> +を implies に入れた型を記述する</p><pre><code class="AGDA hljs"> <span class="hljs-attribute">whileTestPSem</span> : (c : ℕ) → whileTestP c + ( λ env → ⊤ implies (vari env ≡ <span class="hljs-number">0</span>) ∧ (varn env ≡ c10 env) ) + whileTestPSem c = proof ( λ _ → record { <span class="hljs-attribute">pi1</span> = refl ; <span class="hljs-attribute">pi2</span> = refl } ) +</code></pre><p>証明では proof に( ⊤ → (vari env ≡ 0) ∧ (varn env ≡ c10 env) )であると記述できればよく<br> +ここでは λ _ → record { pi1 = refl ; pi2 = refl } がこれに対応する</p><p><strong>whileTestPSemSound</strong> は output ≡ whileTestP c (λ e → e) を受け取ることで whileTestP の実行が終わった結果、つまり停止した CodeGear の実行結果が事後条件を満たしていることを証明している</p><pre><code class="AGDA hljs"> whileTestPSemSound : (c : ℕ ) (output : Envc ) → + output ≡ <span class="hljs-function">whileTestP <span class="hljs-title">c</span> (<span class="hljs-params">λ e → e</span>) + → ⊤ <span class="hljs-title">implies</span> (<span class="hljs-params">(vari output ≡ <span class="hljs-number">0</span></span>) ∧ (<span class="hljs-params">varn output ≡ c</span>)) + whileTestPSemSound c output refl </span>= whileTestPSem c +</code></pre><p>同様に他の CodeGear に対しても健全性の証明が可能</p><p>whileConvPSemSound は制約を緩める conversion の健全性の証明</p><pre><code class="AGDA hljs"><span class="hljs-attribute">whileConvPSemSound</span> : {<span class="hljs-attribute">l</span> : Level} → (input : Envc) → ((vari input ≡ <span class="hljs-number">0</span>) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input) +whileConvPSemSound input = proof λ x → (conversion input x) where + conversion : (env : Envc ) → (vari env ≡ <span class="hljs-number">0</span>) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conversion e record { <span class="hljs-attribute">pi1</span> = refl ; <span class="hljs-attribute">pi2</span> = refl } = +zero +</code></pre><p>whileLoopPSemSound は ループを行う CodeGear の 健全性の証明</p><pre><code class="AGDA hljs">whileLoopPSemSound : {l : Level} → (input output : Envc ) + → (varn input + vari input ≡ c10 input) + → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre +</code></pre><p>loopPPSem を使って証明を行っている</p><pre><code class="AGDA hljs"><span class="hljs-attribute">loopPPSem</span> : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input ) + → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p +</code></pre><hr><h2 id="まとめと今後の課題"><a class="anchor hidden-xs" href="#まとめと今後の課題" title="まとめと今後の課題"><i class="fa fa-link"></i></a>まとめと今後の課題</h2><ul> +<li>CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した</li> +<li>Hoare Logic ベースの検証で停止性を含めて検証できた</li> +<li>Hoare Logic ベースの検証の健全性を証明できた +<ul> +<li>while Program で使用した CodeGear を使って証明できた</li> +</ul> +</li> +<li>今後の課題 +<ul> +<li>BinaryTree の有限ループに対する証明</li> +<li>Hoare Logic で検証されたコードの CbC 変換</li> +<li>並列実行での検証</li> +</ul> +</li> +</ul><hr></div> + <div class="ui-toc dropup unselectable hidden-print" style="display:none;"> + <div class="pull-right dropdown"> + <a id="tocLabel" class="ui-toc-label btn btn-default" data-toggle="dropdown" href="#" role="button" aria-haspopup="true" aria-expanded="false" title="Table of content"> + <i class="fa fa-bars"></i> + </a> + <ul id="ui-toc" class="ui-toc-dropdown dropdown-menu" aria-labelledby="tocLabel"> + <div class="toc"><ul class="nav"> +<li class=""><a href="#Continuation-Based-C-の-Hoare-Logic-を用いた仕様記述と検証" title="Continuation Based C の Hoare Logic を用いた仕様記述と検証">Continuation Based C の Hoare Logic を用いた仕様記述と検証</a><ul class="nav"> +<li><a href="#OS-の検証技術としての-Hoare-Logic-の問題点" title="OS の検証技術としての Hoare Logic の問題点">OS の検証技術としての Hoare Logic の問題点</a></li> +<li><a href="#Hoare-Logic-をベースにした-Gears-単位での検証" title="Hoare Logic をベースにした Gears 単位での検証">Hoare Logic をベースにした Gears 単位での検証</a></li> +<li><a href="#Agda" title="Agda">Agda</a></li> +<li><a href="#Agda-の-record-とその例-∧" title="Agda の record とその例 ∧">Agda の record とその例 ∧</a></li> +<li><a href="#Agda-の-data-とその例-Sum" title="Agda の data とその例 Sum">Agda の data とその例 Sum</a></li> +<li><a href="#Hoare-Logic" title="Hoare Logic">Hoare Logic</a></li> +<li><a href="#Agda-での-Hoare-Logic" title="Agda での Hoare Logic">Agda での Hoare Logic</a></li> +<li><a href="#Hoare-Logic-での-while-program" title="Hoare Logic での while program">Hoare Logic での while program</a></li> +<li><a href="#Hoare-Logic-での-Command-に対応する仕様" title="Hoare Logic での Command に対応する仕様">Hoare Logic での Command に対応する仕様</a></li> +<li><a href="#Hoare-Logic-での-仕様記述" title="Hoare Logic での 仕様記述">Hoare Logic での 仕様記述</a></li> +<li><a href="#Hoare-Logic-での健全性の証明" title="Hoare Logic での健全性の証明">Hoare Logic での健全性の証明</a></li> +<li><a href="#Continuation-based-C-について" title="Continuation based C について">Continuation based C について</a></li> +<li><a href="#Agda-での-CodeGear、-DataGear-の記述" title="Agda での CodeGear、 DataGear の記述">Agda での CodeGear、 DataGear の記述</a></li> +<li><a href="#CbC-での-Hoare-Logic" title="CbC での Hoare Logic">CbC での Hoare Logic</a></li> +<li><a href="#CbC-での-while-program" title="CbC での while program">CbC での while program</a></li> +<li><a href="#CbC-での-Hoare-Logic-記述" title="CbC での Hoare Logic 記述">CbC での Hoare Logic 記述</a></li> +<li><a href="#Hoare-Logic-をベースにした-CbC-での-while-loop" title="Hoare Logic をベースにした CbC での while loop">Hoare Logic をベースにした CbC での while loop</a></li> +<li><a href="#CbC-での-Hoare-Logic-の健全性" title="CbC での Hoare Logic の健全性">CbC での Hoare Logic の健全性</a></li> +<li><a href="#まとめと今後の課題" title="まとめと今後の課題">まとめと今後の課題</a></li> +</ul> +</li> +</ul> +</div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div> + </ul> + </div> + </div> + <div id="ui-toc-affix" class="ui-affix-toc ui-toc-dropdown unselectable hidden-print" data-spy="affix" style="top:17px;display:none;" > + <div class="toc"><ul class="nav"> +<li class=""><a href="#Continuation-Based-C-の-Hoare-Logic-を用いた仕様記述と検証" title="Continuation Based C の Hoare Logic を用いた仕様記述と検証">Continuation Based C の Hoare Logic を用いた仕様記述と検証</a><ul class="nav"> +<li><a href="#OS-の検証技術としての-Hoare-Logic-の問題点" title="OS の検証技術としての Hoare Logic の問題点">OS の検証技術としての Hoare Logic の問題点</a></li> +<li><a href="#Hoare-Logic-をベースにした-Gears-単位での検証" title="Hoare Logic をベースにした Gears 単位での検証">Hoare Logic をベースにした Gears 単位での検証</a></li> +<li><a href="#Agda" title="Agda">Agda</a></li> +<li><a href="#Agda-の-record-とその例-∧" title="Agda の record とその例 ∧">Agda の record とその例 ∧</a></li> +<li><a href="#Agda-の-data-とその例-Sum" title="Agda の data とその例 Sum">Agda の data とその例 Sum</a></li> +<li><a href="#Hoare-Logic" title="Hoare Logic">Hoare Logic</a></li> +<li><a href="#Agda-での-Hoare-Logic" title="Agda での Hoare Logic">Agda での Hoare Logic</a></li> +<li><a href="#Hoare-Logic-での-while-program" title="Hoare Logic での while program">Hoare Logic での while program</a></li> +<li><a href="#Hoare-Logic-での-Command-に対応する仕様" title="Hoare Logic での Command に対応する仕様">Hoare Logic での Command に対応する仕様</a></li> +<li><a href="#Hoare-Logic-での-仕様記述" title="Hoare Logic での 仕様記述">Hoare Logic での 仕様記述</a></li> +<li><a href="#Hoare-Logic-での健全性の証明" title="Hoare Logic での健全性の証明">Hoare Logic での健全性の証明</a></li> +<li><a href="#Continuation-based-C-について" title="Continuation based C について">Continuation based C について</a></li> +<li><a href="#Agda-での-CodeGear、-DataGear-の記述" title="Agda での CodeGear、 DataGear の記述">Agda での CodeGear、 DataGear の記述</a></li> +<li><a href="#CbC-での-Hoare-Logic" title="CbC での Hoare Logic">CbC での Hoare Logic</a></li> +<li><a href="#CbC-での-while-program" title="CbC での while program">CbC での while program</a></li> +<li><a href="#CbC-での-Hoare-Logic-記述" title="CbC での Hoare Logic 記述">CbC での Hoare Logic 記述</a></li> +<li><a href="#Hoare-Logic-をベースにした-CbC-での-while-loop" title="Hoare Logic をベースにした CbC での while loop">Hoare Logic をベースにした CbC での while loop</a></li> +<li><a href="#CbC-での-Hoare-Logic-の健全性" title="CbC での Hoare Logic の健全性">CbC での Hoare Logic の健全性</a></li> +<li><a href="#まとめと今後の課題" title="まとめと今後の課題">まとめと今後の課題</a></li> +</ul> +</li> +</ul> +</div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div> + </div> + <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.1.1/jquery.min.js" integrity="sha256-hVVnYaiADRTO2PzUGmuLJr8BLUSjGIZsDYGmIJLv2b8=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.4.0/js/bootstrap.min.js" integrity="sha256-kJrlY+s09+QoWjpkOrXXwhxeaoDz9FW5SaxF8I0DibQ=" crossorigin="anonymous" defer></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/gist-embed/2.6.0/gist-embed.min.js" integrity="sha256-KyF2D6xPIJUW5sUDSs93vWyZm+1RzIpKCexxElmxl8g=" crossorigin="anonymous" defer></script> + <script> + var markdown = $(".markdown-body"); + //smooth all hash trigger scrolling + function smoothHashScroll() { + var hashElements = $("a[href^='#']").toArray(); + for (var i = 0; i < hashElements.length; i++) { + var element = hashElements[i]; + var $element = $(element); + var hash = element.hash; + if (hash) { + $element.on('click', function (e) { + // store hash + var hash = this.hash; + if ($(hash).length <= 0) return; + // prevent default anchor click behavior + e.preventDefault(); + // animate + $('body, html').stop(true, true).animate({ + scrollTop: $(hash).offset().top + }, 100, "linear", function () { + // when done, add hash to url + // (default click behaviour) + window.location.hash = hash; + }); + }); + } + } + } + + smoothHashScroll(); + var toc = $('.ui-toc'); + var tocAffix = $('.ui-affix-toc'); + var tocDropdown = $('.ui-toc-dropdown'); + //toc + tocDropdown.click(function (e) { + e.stopPropagation(); + }); + + var enoughForAffixToc = true; + + function generateScrollspy() { + $(document.body).scrollspy({ + target: '' + }); + $(document.body).scrollspy('refresh'); + if (enoughForAffixToc) { + toc.hide(); + tocAffix.show(); + } else { + tocAffix.hide(); + toc.show(); + } + $(document.body).scroll(); + } + + function windowResize() { + //toc right + var paddingRight = parseFloat(markdown.css('padding-right')); + var right = ($(window).width() - (markdown.offset().left + markdown.outerWidth() - paddingRight)); + toc.css('right', right + 'px'); + //affix toc left + var newbool; + var rightMargin = (markdown.parent().outerWidth() - markdown.outerWidth()) / 2; + //for ipad or wider device + if (rightMargin >= 133) { + newbool = true; + var affixLeftMargin = (tocAffix.outerWidth() - tocAffix.width()) / 2; + var left = markdown.offset().left + markdown.outerWidth() - affixLeftMargin; + tocAffix.css('left', left + 'px'); + } else { + newbool = false; + } + if (newbool != enoughForAffixToc) { + enoughForAffixToc = newbool; + generateScrollspy(); + } + } + $(window).resize(function () { + windowResize(); + }); + $(document).ready(function () { + windowResize(); + generateScrollspy(); + }); + + //remove hash + function removeHash() { + window.location.hash = ''; + } + + var backtotop = $('.back-to-top'); + var gotobottom = $('.go-to-bottom'); + + backtotop.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + if (scrollToTop) + scrollToTop(); + removeHash(); + }); + gotobottom.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + if (scrollToBottom) + scrollToBottom(); + removeHash(); + }); + + var toggle = $('.expand-toggle'); + var tocExpand = false; + + checkExpandToggle(); + toggle.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + tocExpand = !tocExpand; + checkExpandToggle(); + }) + + function checkExpandToggle () { + var toc = $('.ui-toc-dropdown .toc'); + var toggle = $('.expand-toggle'); + if (!tocExpand) { + toc.removeClass('expand'); + toggle.text('Expand all'); + } else { + toc.addClass('expand'); + toggle.text('Collapse all'); + } + } + + function scrollToTop() { + $('body, html').stop(true, true).animate({ + scrollTop: 0 + }, 100, "linear"); + } + + function scrollToBottom() { + $('body, html').stop(true, true).animate({ + scrollTop: $(document.body)[0].scrollHeight + }, 100, "linear"); + } + </script> +</body> + +</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/master-slide.md Wed Feb 12 05:02:27 2020 +0900 @@ -0,0 +1,572 @@ +Continuation Based C の Hoare Logic を用いた仕様記述と検証 +===== + +琉球大学大学院 : 並列信頼研究室\ +外間 政尊 + +--- + +## OS の検証技術としての Hoare Logic の問題点 +- OS やアプリケーションの信頼性は重要な課題 + +- 信頼性を上げるために仕様の検証が必要 + +- 検証にはモデル検査や**定理証明**などが存在する + +- また、仕様検証の手法として **Hoare Logic** がある + -通常の関数でも実行する前に必要な引数があって何らかの出力がある + - Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ +- Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等) + +--- +## Hoare Logic をベースにした Gears 単位での検証 +- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 +- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む +- CodeGear は継続を用いて次の CodeGear に接続される +- 定理証明支援機の Agda 上で Gears 単位を用いた検証を行う +- 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する + +--- + +## Agda + Agda は関数型言語 +```AGAD + name : type + name = value +``` +関数には型と定義を与える\ +型は **:** で、 値は **=** で与える\ +仮定なしに使えるのは Set のみ + +構成要素としては以下の3種類 +1. 関数 + - 型は(A : Set かつ B : Set のとき) A → B + - 値は(x : A かつ y : B) λ x → y +1. record +1. data + +--- + +## Agda の record とその例 ∧ +導入は2つのものが同時に存在すること +``` + A B +------------ + A ∧ B +``` +除去は名前を区別する必要がある +``` + A ∧ B A ∧ B + --------- pi1 --------- pi2 + A B +``` +A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B\ +Agda ではこのような同時に存在する型を **record** で書く +```AGDA + record _∧_ (A B : Set) : Set + field + pi1 : A + pi2 : B +``` +\_∧\_ は中間記法、変数が入る位置を _ で示せる\ +実際の構築は x : A かつ y : B のとき +```AGDA +createAnd : (A : Set) → (B : Set) → A ∧ B +createAnd x y = record {pi1 = x ; pi2 = y} +``` +のように記述する\ +C 言語での構造体のようなもの + +A や B に論理式が入ると2つのものが同時に成り立つ証明ができる + +--- + +## Agda の data とその例 Sum +導入\ +一つでも存在すること +``` + A B + ----------- p1 ---------- p2 + A ∨ B A ∨ B +``` +除去\ +A → C か B → C のとき C +``` + A B + : : + A ∨ B C C + ------------------------ + C +``` + + +A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B\ +どちらかが成り立つ型を **data** で書く\ +```AGDA + data _∨_ (A B : Set) : Set where + p1 : A → A ∨ B + p2 : B → A ∨ B +``` +のように記述できる\ +C 言語での union のようなもの\ +p1、 p2 は case 文みたいな感じ + +--- + +## Hoare Logic +Hoare Logic はプログラム検証の手法\ +事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ + +これは **{ P } C { Q }** の形で表され、Hoare Triple と呼ばれる + + +今回は以下のような while program を検証する + +n = 10 となっているが検証では n は任意の自然数 +```C + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +``` + +--- + +## Agda での Hoare Logic +Hoare Logic のプログラムは Command で構成される + +Comm 型は data で記述されたコマンドのデータ構造 + +実際に実行するには解釈して動かす関数が必要 + +Commを使って while program を構築する + +```AGDA + data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm → Comm + Seq : Comm → Comm → Comm + If : Cond → Comm → Comm → Comm + While : Cond → Comm → Comm +``` + +--- + +## Hoare Logic での while program +検証する while program の擬似コード +```C + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +``` +コマンドで構成した while program +```AGDA + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +``` + +これは Hoare Logic のコマンドで以下のような構文木を記述している + +``` + Seq + / \ + PComm Seq + (n=c10) / \ + PComm While + (i=0) | + Cond + (0<n) + | + Seq + / \ + PComm PComm + (i+1) (n-1) +``` + +--- + +## Hoare Logic での Command に対応する仕様 +Command に対応する証明がある + +**HTProof** は Hoare Triple Proof + +**{P} Q {C}** が **Cond → Comm → Cond** に対応している + +```agda + data HTProof : Cond → Comm → Cond → Set where +``` +すべての Command に対応する Proof を載せると長いので +必要なものだけ + +\ +PrimRule は 代入のときに成り立ってほしいルール + +Axiom は Triple を受け取ってすべての Env は事前の Env が正しければ コマンドを実行した後のEnv も正しくなるという命題 +```AGDA + PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → + (pr : Axiom bPre pcm bPost) → + HTProof bPre (PComm pcm) bPost +``` +WekeningRule は 条件を緩める規則 + +While コマンドなどで条件が厳しいときに同時に成り立つ異なる条件へ変更必要がある + +Tautology は2つの Cond 型 bPre、 bPre' を受け取り、 bPre が成り立つとき、 bPre'が成り立つという命題 +```agda + WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → + {bPost' : Cond} → {bPost : Cond} → + Tautology bPre bPre' → + HTProof bPre' cm bPost' → + Tautology bPost' bPost → + HTProof bPre cm bPost +``` +SeqRule は Seqcuence が正しい順番で行われることを保証 + +cm1、cm2 という2つのCommを受け取ってそれらがcm1、cm2の順で実行される + +``` + SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → + {cm2 : Comm} → {bPost : Cond} → + HTProof bPre cm1 bMid → + HTProof bMid cm2 bPost → + HTProof bPre (Seq cm1 cm2) bPost +``` +WhileRule は Comm 型の cm と Cond型の bInv、 bが存在するとき、 +事前に +``` + WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → + HTProof (bInv and b) cm bInv → + HTProof bInv (While b cm) (bInv and neg b) +``` +検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある + +## Hoare Logic での 仕様記述 +HTProof で記述した仕様 + +HTProof が コマンドに対応しているのでほとんど同じ形で書けてる +```AGDA + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +``` + +```AGDA + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +``` +proof1 は条件がつながるのに必要な条件を lemma で記述している(lemma は長いので省略) + +部分正当性は示せている + +全体がつながっているが証明にはなっていない + + +--- +## Hoare Logic での健全性の証明 +実際に正しく動作すること(健全性)を証明する必要がある + +Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す + +PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する +```AGDA + PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost + PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +``` +Soundness は HTProof に対応した非常に複雑な証明 + +HTProof を渡すと Ruleに対応した証明を行う + +proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している + +```AGDA + proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true + proofOfProgram c10 input output ic sem = + PrimSoundness (proof1 c10) input output ic sem +``` + +--- +## Continuation based C について +Continuation based C (CbC) は当研究室で開発してるプログラミング言語 + +CbC では処理の単位を **CodeGear** 、データの単位を **DataGear** とする + +CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す + +Output の DataGear は次の CodeGear の Input として接続される + +![cgdg-small.svg](/attachment/5e42fdea7b378d004670d2fc) +CodeGear の接続処理などのメタ計算は Meta CodeGear として定義 + +Meta CodeGear で信頼性の検証を行う + + + + + +--- +## Agda での CodeGear、 DataGear の記述 + +- Agda での CodeGear は継続渡しで記述された関数 +```AGDA + whileTest : {t : Set} → (c10 : Nat) + → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 + ; vari = 0} ) + ``` + - CodeGear の型は継続先を返す関数 + - **(Code : fa → t)** は継続先 + - 引数として継続先の CodeGear を受け取る + + + + + + + +--- +## CbC での Hoare Logic +CodeGear、DataGear を用いた Hoare Logic は図のようになる +![hoare-cg-dg.svg](/attachment/5e42baee7b378d004670d1f5) +CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる + +下のコードは CodeGear、 DataGear を用いた Hoare Logic ベースの記述例である + +```AGDA + whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) + → whileTestStateP s1 env → t) → t + whileTestPwP c10 next = next (whileTestP c10 ( λ env → env )) + record { pi1 = refl ; pi2 = refl } +``` + + + + + + + + + + + + +--- +## CbC での while program +```C + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +``` + +CbC での while program +```AGDA + whileTestPCall : (c10 : ℕ ) → Envc + whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env)) +``` +- whileTestP' が n = c10、 i = 0 の代入、 loopP' が while loop に対応している +- CbC での Hoare Logic 上でコマンドは CodeGear そのもの + - CodeGear は Hoare Logic のコマンドより自由な記述 + + +--- +## CbC での Hoare Logic 記述 +CbC での Hoare Logic 記述では CodeGear が条件を受け取る + +whileTestPwP は代入を行う CodeGear + +```AGDA + whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) + → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t + whileTestPwP c10 next = + next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl }) +``` +loopPwP' は while loop をするための条件を持ち、ループをする CodeGear + +n と (n ≡ varn env) を受け取り varn でのパターンマッチをしている + +suc n の場合はループを抜けるか判断する CodeGear に継続する + +更に継続先で loopPwP' を呼ぶことで再帰的にループする +```AGDA + loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → (vari env + varn env ≡ c10 env) → + (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t + loopPwP' zero env refl refl exit = exit env refl + loopPwP' (suc n) env refl refl exit = + whileLoopPwP' (suc n) env refl refl + (λ env x y → loopPwP' n env x y exit) exit +``` +whileLoopPwP' は while loop を抜けるか判断する CodeGear + +loopPwP'から呼ばれている +```AGDA + whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → (vari env + varn env ≡ c10 env) + → (next : (env : Envc ) → (pred n ≡ varn env) + → (vari env + varn env ≡ c10 env) → t) + → (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t + whileLoopPwP' zero env refl refl _ exit = exit env refl + whileLoopPwP' (suc n) env refl refl next _ = + next (record env {varn = pred (varn env) ; vari = suc (vari env)}) + refl (+-suc n (vari env)) +``` + +conv は whileTestPwP の事後条件から while loop のための loop invaliant に変更する + +```AGDA + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) + → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero +``` + +whileTestPCallwP' は先程までの Hoare Logic の記述をつなげたもの + +継続先の CodeGear に渡す条件が +```AGDA + whileTestPCallwP' : (c : ℕ ) → Set + whileTestPCallwP' c = whileTestPwP {_} {_} c ( + λ env s → loopPwP' (varn env) env refl (conv env s) + ( λ env s → vari env ≡ c10 env ) ) +``` + +whileTestPCallwP' では Hoare Logic の条件が接続できた + +--- + +## Hoare Logic をベースにした CbC での while loop +先程条件を接続した whileTestPCallwP' を型に入れ、実際に実行してみる +```AGDA + whileCallwP : (c : ℕ) → whileTestPCallwP' c + whileCallwP c = whileTestPwP {_} {_} c (λ env s → + loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) +``` +loopPwP'は任意の値を取ってループを行う CodeGear であった + +しかし、引数で受け取った任意の自然数で実行するとループが停まらない + +任意の自然数回ループする loopPwP' が停まることを補助する loopHelper を記述した +```AGDA + loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) + → (varn env + vari env ≡ c10 env) + → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) + loopHelper zero env eq refl rewrite eq = refl + loopHelper (suc n) env eq refl rewrite eq = loopHelper n + (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) + refl (+-suc n (vari env)) +``` +loopHelper を用いて記述した実行は実際に停止した +```AGDA + helperCallwP : (c : ℕ) → whileTestPCallwP' c + helperCallwP c = whileTestPwP {_} {_} c + (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) +``` + +--- +## CbC での Hoare Logic の健全性 + +implies という data を用いて健全性の証明を行う + +implies の型は A と B の条件を受け取る + +このとき proof として A → B が存在すれば A implies B が証明できる +```AGDA + data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A → B ) → A implies B +``` +代入を行う CodeGear である **whileTestP** を実行したとき、\ +常に真の命題 **⊤** と代入を終えたときの事後条件である\ +**(vari env ≡ 0) ∧ (varn env ≡ c10 env)** +を implies に入れた型を記述する + +```AGDA + whileTestPSem : (c : ℕ) → whileTestP c + ( λ env → ⊤ implies (vari env ≡ 0) ∧ (varn env ≡ c10 env) ) + whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) +``` + +証明では proof に( ⊤ → (vari env ≡ 0) ∧ (varn env ≡ c10 env) )であると記述できればよく\ +ここでは λ _ → record { pi1 = refl ; pi2 = refl } がこれに対応する + +**whileTestPSemSound** は output ≡ whileTestP c (λ e → e) を受け取ることで whileTestP の実行が終わった結果、つまり停止した CodeGear の実行結果が事後条件を満たしていることを証明している + +```AGDA + whileTestPSemSound : (c : ℕ ) (output : Envc ) → + output ≡ whileTestP c (λ e → e) + → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c)) + whileTestPSemSound c output refl = whileTestPSem c +``` + +同様に他の CodeGear に対しても健全性の証明が可能 + +whileConvPSemSound は制約を緩める conversion の健全性の証明 +```AGDA +whileConvPSemSound : {l : Level} → (input : Envc) → ((vari input ≡ 0) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input) +whileConvPSemSound input = proof λ x → (conversion input x) where + conversion : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conversion e record { pi1 = refl ; pi2 = refl } = +zero +``` + +whileLoopPSemSound は ループを行う CodeGear の 健全性の証明 + +```AGDA +whileLoopPSemSound : {l : Level} → (input output : Envc ) + → (varn input + vari input ≡ c10 input) + → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre +``` + +loopPPSem を使って証明を行っている + +```AGDA +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input ) + → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p +``` + +--- +## まとめと今後の課題 +- CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した +- Hoare Logic ベースの検証で停止性を含めて検証できた +- Hoare Logic ベースの検証の健全性を証明できた + - while Program で使用した CodeGear を使って証明できた +- 今後の課題 + - BinaryTree の有限ループに対する証明 + - Hoare Logic で検証されたコードの CbC 変換 + - 並列実行での検証 + +--- \ No newline at end of file
--- a/slide/slide.html Tue Feb 11 02:31:26 2020 +0900 +++ b/slide/slide.html Wed Feb 12 05:02:27 2020 +0900 @@ -7,7 +7,7 @@ <html> <head> <meta http-equiv="content-type" content="text/html;charset=utf-8"> - <title>Continuation based C での Hoare Logic を用いた記述と検証</title> + <title>Continuation based C での Hoare Logic を用いた仕様記述と検証</title> <meta name="generator" content="Slide Show (S9) v4.0.1 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]"> <meta name="author" content="外間政尊" > @@ -70,7 +70,7 @@ <tr> <td> <div align="center"> - <h1><font color="#808db5">Continuation based C での Hoare Logic を用いた記述と検証</font></h1> + <h1><font color="#808db5">Continuation based C での Hoare Logic を用いた仕様記述と検証</font></h1> </div> </td> </tr> @@ -91,9 +91,40 @@ <div class='slide'> <!-- 発表30~40分、質疑応答20~30分くらい…? --> <!-- TODO -- 章構成を slide.mm の形に直す。 -- Agda の説明と Gears の説明をなおす -- Gears での Hoare Logic の説明する前になんで Hoare Logic ベースなのかのスライドを入れてみる +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- HoareLogic + - hoare logic の説明 + - while program + + +- 使う Agda のイントロ + - and と lambda + - でーた分け? + +- Hoare logic と agda + - while program + - hoare logic の while program + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ --> @@ -105,13 +136,11 @@ <li>検証にはモデル検査や<strong>定理証明</strong>などが存在する</li> <li>また、仕様検証の手法として <strong>Hoare Logic</strong> がある <ul> - <li>プログラムを書く上である関数は実行する前に必要な引数があって何らかの出力がある</li> - <li>Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ -<!-- - 関数実行前に、引数が存在していて、出力が意図した通りになる --></li> + <li>通常の関数でも実行する前に必要な引数があって何らかの出力がある</li> + <li>Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ</li> </ul> </li> - <li>Hoare Logic では関数が最低限のコマンドまで分割されており記述が困難(変数の代入、コマンド実行の遷移等)</li> - <li>大規模なプログラムは構築しづらい</li> + <li>Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等)</li> </ul> @@ -129,31 +158,190 @@ <li>本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する</li> </ul> +<!-- ## 証明の基礎 --> +<!-- - A は論理式を表す変数、もしくは型Aという集合 --> +<!-- - 論理式は変数と論理演算子で表される --> +<!-- - 変数や演算子は構文要素 --> + +<!-- ``` --> +<!-- A → B --> +<!-- ``` --> +<!-- - A → B は 「A ならば B」 --> +<!-- - 関数としてみると A を受け取って B を返す関数 --> +<!-- - A を仮定したとき B が証明される --> +<!-- <\!-- ``` -\-> --> +<!-- <\!-- A -\-> --> +<!-- <\!-- --------- -\-> --> +<!-- <\!-- B -\-> --> +<!-- <\!-- ``` -\-> --> + +<!-- ## 関数適用による証明 --> +<!-- - --> + +<!-- ``` --> +<!-- λ x → y --> +<!-- ``` --> +<!-- - x は変数 y は項 --> +<!-- - x は関数の引数と同じ扱い --> +<!-- - 項には型が対応し、再帰的に定義される --> +<!-- ``` --> +<!-- x : A --> +<!-- ``` --> +<!-- - x という項が型A を持つことを表す --> +<!-- x : A かつ y : B のとき --> +<!-- ``` --> +<!-- λ x → y : A → B --> +<!-- ``` --> +<!-- となる --> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda">Agda</h2> +<ul> + <li>Agda は関数型言語 + <div class="language-AGAD highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> name : type +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> name = value +</pre></div> +</div> + </div> + </li> + <li>関数には型と定義を与える + <ul> + <li>型は <strong>:</strong> で、 値は <strong>=</strong> で与える</li> + </ul> + </li> + <li>仮定なしに使えるのは Set のみ</li> + <li>構成要素としては以下の3種類 + <ol> + <li>関数 + <ul> + <li>型は A → B</li> + <li>値は λ x → y</li> + </ul> + </li> + <li>record</li> + <li>data</li> + </ol> + </li> + <li>つぎは record と data について</li> +</ul> + </div> <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-のデータ型">Agda のデータ型</h2> +<h2 id="agda-の-record-とその例-">Agda の record とその例 ∧</h2> <ul> - <li><strong>データ型</strong>はプリミティブなデータ</li> - <li>この型のとき値は一意に定まる - <div class="language-SHELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Nat : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> zero : Nat -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> suc : Nat → Nat + <li>2つのものが同時に存在すること</li> + <li>A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B</li> + <li>Agda ではこのような同時に存在する型を <strong>record</strong> で書く + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record _∧_ (A B : Set) : Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> pi1 : A +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> pi2 : B +</pre></div> +</div> + </div> + </li> + <li><em>∧</em> は中間記法、変数が入る位置を _ で示せる</li> + <li>実際の構築は x : A かつ y : B のとき + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record {pi1 = x ; pi2 = y} +</pre></div> +</div> + </div> + </li> + <li>のように記述する</li> + <li>C での構造体のようなもの</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda-の-data-とその例-sum">Agda の data とその例 Sum</h2> +<ul> + <li>一つでも存在すること</li> + <li>A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B</li> + <li>どちらかが成り立つ型を <strong>data</strong> で書く + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data _∨_ (A B : Set) : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> p1 : A → A ∨ B +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> p2 : B → A ∨ B </pre></div> </div> </div> </li> - <li><strong>レコード型</strong>は複数のデータをまとめる</li> - <li>複数の値を保持できる - <div class="language-SHELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : Nat -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : Nat + <li>のように記述できる</li> + <li>C での union のようなもの</li> + <li> + <p>p1、 p2 は case 文みたいな</p> + </li> + <li>次は Hoare Logic</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic">Hoare Logic</h2> +<ul> + <li>Hoare Logic はプログラム検証の手法</li> + <li>事前条件(P)が成り立つとき、コマンド(C)を実行すると事後条件(Q)が成り立つ + <ul> + <li><strong>{P} C {Q}</strong> の形で表される</li> + <li>コマンドが制限されてる</li> + </ul> + </li> + <li>今回は以下のような while program を検証する</li> + <li>n = 10 となっているが検証では n は任意の自然数 + <div class="language-C highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } +</pre></div> +</div> + </div> + </li> + <li>次は Agda の Hoare Logic で while program をみる</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda-での-hoare-logic">Agda での Hoare Logic</h2> +<ul> + <li>Hoare Logic のプログラムは Command で構成される</li> + <li>Comm は data で記述されたコマンド</li> + <li>このコマンドを使って while program を構築する + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Comm : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Skip : Comm +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Abort : Comm +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> PComm : PrimComm → Comm +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> Seq : Comm → Comm → Comm +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> If : Cond → Comm → Comm → Comm +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> While : Cond → Comm → Comm </pre></div> </div> </div> @@ -166,22 +354,104 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-の関数">Agda の関数</h2> +<h2 id="hoare-logic-での-while-program">Hoare Logic での while program</h2> <ul> - <li>関数にも同様に型が必要 - <div class="language-HASKELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> +1 : ℕ → ℕ -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> +1 m = suc m + <li>C の while program + <div class="language-C highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; <span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- eval +1 zero -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> -- return suc zero +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } +</pre></div> +</div> + </div> + </li> + <li>Hoare Logic での while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li>関数の型は <strong>input → output</strong></li> - <li>複数入力がある場合は <strong>input1 → input2 → output</strong></li> - <li><strong>=</strong> の左側は関数名と引数、右側に実装</li> + <li>次は Hoare Logic での検証</li> +</ul> + +<!-- TODO +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ +--> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic-での-command-に対応する仕様">Hoare Logic での Command に対応する仕様</h2> +<ul> + <li>Command に対応する証明がある + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> data HTProof : Cond → Comm → Cond → Set where +<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → +<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> (pr : Axiom bPre pcm bPost) → +<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> HTProof bPre (PComm pcm) bPost +<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> SkipRule : (b : Cond) → HTProof b Skip b +<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> AbortRule : (bPre : Cond) → (bPost : Cond) → +<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> HTProof bPre Abort bPost +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> {bPost' : Cond} → {bPost : Cond} → +<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> Tautology bPre bPre' → +<span class="line-numbers"><a href="#n11" name="n11">11</a></span> HTProof bPre' cm bPost' → +<span class="line-numbers"><a href="#n12" name="n12">12</a></span> Tautology bPost' bPost → +<span class="line-numbers"><a href="#n13" name="n13">13</a></span> HTProof bPre cm bPost +<span class="line-numbers"><a href="#n14" name="n14">14</a></span> SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → +<span class="line-numbers"><a href="#n15" name="n15">15</a></span> {cm2 : Comm} → {bPost : Cond} → +<span class="line-numbers"><a href="#n16" name="n16">16</a></span> HTProof bPre cm1 bMid → +<span class="line-numbers"><a href="#n17" name="n17">17</a></span> HTProof bMid cm2 bPost → +<span class="line-numbers"><a href="#n18" name="n18">18</a></span> HTProof bPre (Seq cm1 cm2) bPost +<span class="line-numbers"><a href="#n19" name="n19">19</a></span> IfRule : {cmThen : Comm} → {cmElse : Comm} → +<span class="line-numbers"><strong><a href="#n20" name="n20">20</a></strong></span> {bPre : Cond} → {bPost : Cond} → +<span class="line-numbers"><a href="#n21" name="n21">21</a></span> {b : Cond} → +<span class="line-numbers"><a href="#n22" name="n22">22</a></span> HTProof (bPre and b) cmThen bPost → +<span class="line-numbers"><a href="#n23" name="n23">23</a></span> HTProof (bPre and neg b) cmElse bPost → +<span class="line-numbers"><a href="#n24" name="n24">24</a></span> HTProof bPre (If b cmThen cmElse) bPost +<span class="line-numbers"><a href="#n25" name="n25">25</a></span> WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → +<span class="line-numbers"><a href="#n26" name="n26">26</a></span> HTProof (bInv and b) cm bInv → +<span class="line-numbers"><a href="#n27" name="n27">27</a></span> HTProof bInv (While b cm) (bInv and neg b) +</pre></div> +</div> + </div> + </li> + <li>検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある</li> </ul> @@ -190,25 +460,76 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での証明">Agda での証明</h2> +<h2 id="hoare-logic-での-仕様記述と部分正当性">Hoare Logic での 仕様記述と部分正当性</h2> <ul> - <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong> - <div class="language-HASKELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> +zero : { y : Nat } → y + zero ≡ y -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> +zero {zero} = refl -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> +zero {suc y} = cong suc ( +zero {y} ) + <li>HTProof で記述した仕様</li> + <li>lemma は事前条件からコマンドを通して事後条件が成り立つこと(部分正当性)の証明(長いので省略) + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proof1 c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule (init-case {c10} )) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +</pre></div> +</div> + </div> + </li> + <li>比較のために元の while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li><strong>refl</strong> は <strong>x ≡ x</strong></li> - <li><strong>cong</strong> は <strong>関数</strong> と等式を受け取って、等式の両辺に関数を適応しても等しくなること</li> - <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明 + <li>Command と対応した仕様があるため形がほぼ一緒 <ul> - <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li> - <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして帰納的に証明している</li> + <li>while ループするときに強い条件を緩めている規則が違うくらい(Weacening Rule)</li> </ul> </li> + <li>proof1 は HTProof が正しく繋げることで部分正当性まで証明</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic-での健全性の証明">Hoare Logic での健全性の証明</h2> +<ul> + <li>proof1 は部分正当性を示せた</li> + <li>実際に正しく動作すること(健全性)を証明する必要がある</li> + <li>Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す</li> + <li>PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> HTProof bPre cm bPost -> Satisfies bPre cm bPost +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +</pre></div> +</div> + </div> + </li> + <li>proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofOfProgram : (c10 : ℕ) → (input output : Env ) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → initCond input ≡ true +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> → (SemComm (program c10) input output) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> → termCond {c10} output ≡ true +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> proofOfProgram c10 input output ic sem = +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> PrimSoundness (proof1 c10) input output ic sem +</pre></div> +</div> + </div> + </li> </ul> @@ -217,18 +538,16 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-について">Gears について</h2> +<h2 id="continuation-based-c-について">Continuation based C について</h2> <ul> - <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li> - <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li> + <li>Continuation based C (CbC) は当研究室で開発してるプログラミング言語</li> + <li>CbC では処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong> とする</li> <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li> - <li>Output の DataGear は次の CodeGear の Input として接続される -<!-- [fig1](file://./fig/cgdg.pdf) --></li> + <li>Output の DataGear は次の CodeGear の Input として接続される</li> <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li> <li>Meta CodeGear で信頼性の検証を行う</li> </ul> <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p> -<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> --> @@ -236,34 +555,13 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での-datagear">Agda での DataGear</h2> +<h2 id="cbc-での-hoare-logic">CbC での Hoare Logic</h2> <ul> - <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li> - <li>Agda は CodeGear、 DataGear は検証メタ計算そのものと考えられる</li> - <li>DataGear は Agda の CodeGear で使われる<strong>全てのデータ</strong>に当たる</li> + <li>CodeGear、DataGear を用いた Hoare Logic は図のようになる</li> </ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="agda-での-codegear">Agda での CodeGear</h2> +<p style="text-align:center;"><img src="./fig/hoare-cg-dg.svg" alt="" width="60%" height="60%" /></p> <ul> - <li>Agda での CodeGear は継続渡しで記述された関数 - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest : {t : Set} → (c10 : Nat) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (Code : Env → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest c10 next = next (record {varn = c10 -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ; vari = 0} ) -</pre></div> -</div> - </div> - </li> - <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li> - <li><strong>(Code : fa → t)</strong> は継続先</li> - <li>引数として継続先を受け取って計算結果を渡す</li> + <li>CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる</li> </ul> @@ -272,68 +570,33 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2> +<h2 id="cbc-での-while-program">CbC での while program</h2> <ul> - <li>関数の動作を条件で変えたいときはパターンマッチを行う + <li>比較用の Hoare Logic での while program <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileLoop : {l : Level} {t : Set l} → Envc -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (next : Envc → t) → (exit : Envc → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li>whileLoop は varn が 0 より大きい間ループする</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2> -<div class="language-C highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } + <li>CbC での while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCall : (c10 : ℕ ) → Envc +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env)) </pre></div> </div> -</div> -<ul> - <li>今回 Hoare Logic で証明する次のようなコードを検証した</li> - <li>このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす</li> - <li>n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> test : Env -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> -- whileLoop : {t : Set} → Env → (Code : Env → t) → t -</pre></div> -</div> -</div> -<ul> - <li>test は whileTest と whileLoop を実行した結果を返す関数</li> - <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す + </div> + </li> + <li>whileTestP’ が n = c10、 i = 0 の代入、 loopP’ が while loop に対応している</li> + <li>CbC での Hoare Logic 上でコマンドは CodeGear そのもの <ul> - <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li> + <li>CodeGear は Hoare Logic のコマンドより自由な記述</li> </ul> </li> </ul> @@ -344,49 +607,46 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-をベースにした-hoare-logic-と証明全体">Gears をベースにした Hoare Logic と証明(全体)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears : {c10 : Nat } → Set -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> (λ n2 → ( vari n2 ≡ c10 )))) +<h2 id="cbc-での-htproof">CbC での HTProof</h2> +<ul> + <li>HTProof に対応するものは各 Meta CodeGear に条件を渡したもの</li> + <li>それぞれが事前条件から事後条件を導く証明を持っている + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTestPwP c10 next = +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl }) </pre></div> </div> -</div> -<ul> - <li>proofGears は Hoare Logic をベースとした証明 - <ul> - <li>先程のプログラムと違い、引数として証明も持っている</li> - </ul> + </div> </li> - <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明whiletest">Gears と Hoare Logic をベースにした証明(whileTest)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest' : {l : Level} {t : Set l} {c10 : ℕ } -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest' {_} {_} {c10} next = next -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) + <li>whileTestPCallwP’ は Hoare Logic の HTProof 記述 proof1 に相当</li> + <li>比較用 proof1 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proof1 c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule (init-case {c10} )) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 </pre></div> </div> + </div> + </li> + <li>proof1 の lemma に相当する証明は Meta CodeGear で、継続先の CodeGear に渡す条件の証明 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCallwP' : (c : ℕ ) → Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCallwP' c = whileTestPwP {_} {_} c ( +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> λ env s → loopPwP' (varn env) env refl (conv env s) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → vari env ≡ c10 env ) ) +</pre></div> </div> -<ul> - <li>最初の Command なので PreCondition はない</li> - <li>(record {pi1 = refl ; pi2 = refl}) は <strong>(vari env) ≡ 0</strong> と <strong>(varn env) ≡ c10</strong>の証明 - <ul> - <li><strong><em>∧</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li> - <li>両方とも成り立つので <strong>refl</strong></li> - </ul> + </div> </li> - <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong></li> + <li>Hoare Logic では実装、部分正当性を分けて記述していた</li> + <li>CbC での Hoare Logic は実装と部分正当性を一体化できる</li> </ul> @@ -395,111 +655,27 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明conversion">Gears と Hoare Logic をベースにした証明(conversion)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> conv e record { pi1 = refl ; pi2 = refl } = +zero -</pre></div> -</div> -</div> +<h2 id="cbc-での-soundness">CbC での Soundness</h2> <ul> - <li>conv は制約を緩める CodeGear - <ul> - <li><strong>(vari env ≡ 0) ∧ (varn env ≡ c10 env)</strong> が成り立つとき <strong>varn env + vari env ≡ c10 env</strong> が成り立つ</li> - </ul> - </li> -</ul> - -<!-- ## Hoare Logic の証明 --> -<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している --> -<!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している --> -<!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 --> -<!-- - 変換後の式を次の行に書いて変換を続ける --> -<!-- ```AGDA --> -<!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) --> -<!-- → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env)) --> -<!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t --> -<!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero --> -<!-- ``` --> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明whileloop">Gears と Hoare Logic をベースにした証明(whileLoop)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> whileLoopPwP' zero env refl refl next exit = exit env refl -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> whileLoopPwP' (suc n) env refl refl next exit = -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> loopPwP' zero env refl refl exit = exit env refl -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> (λ env x y → loopPwP' n env x y exit) exit + <li>先程の whileTestPCallwP’ を命題として証明すると健全性が示せる + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCallwP' : (c : ℕ ) → Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCallwP' c = whileTestPwP {_} {_} c ( +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> λ env s → loopPwP' (varn env) env refl (conv env s) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → vari env ≡ c10 env ) ) </pre></div> </div> -</div> -<ul> - <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li> - <li>ループが回るごとに、<strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした仕様記述">Gears と Hoare Logic をベースにした仕様記述</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileProofs : (c : ℕ ) → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> ( λ env s → conv1 env s -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> ( λ env s → vari env ≡ c10 env ))) + </div> + </li> + <li>実際に値が入ると命題は成り立つが任意の値だと停止せず証明が終わらない + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileCallwP : (c : ℕ) → whileTestPCallwP' c +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileCallwP c = whileTestPwP {_} {_} c (λ env s → +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) </pre></div> </div> -</div> -<ul> - <li><strong>whileProofs</strong> では最終状態が vari と c10 が等しくなるため仕様になっている</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-を用いた仕様の証明">Gears と Hoare Logic を用いた仕様の証明</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>-- ( λ env s → conv1 env s -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>-- ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>-- ( λ env s → vari env ≡ c10 env ))) -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> ProofGears : (c : ℕ) → whileProofs c -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> ProofGears c = whileTestPwP {_} {_} c -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> (λ env₁ s₁ → {!!})) -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> ------------------------------------------------------------ -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> s₁ : vari env₁ ≡ c10 env₁ -<span class="line-numbers"><a href="#n15" name="n15">15</a></span> env₁ : Envc -<span class="line-numbers"><a href="#n16" name="n16">16</a></span> s : (vari env ≡ 0) /\ (varn env ≡ c10 env) -<span class="line-numbers"><a href="#n17" name="n17">17</a></span> env : Envc -<span class="line-numbers"><a href="#n18" name="n18">18</a></span> c : ℕ -</pre></div> -</div> -</div> -<ul> - <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li> - <li>しかし loopPwP’ のループが進まず証明できない</li> + </div> + </li> </ul> @@ -509,18 +685,21 @@ <div class='slide'> <!-- _S9SLIDE_ --> <h2 id="検証時の-loop-の解決">検証時の Loop の解決</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> loopHelper zero env eq refl rewrite eq = refl -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> loopHelper (suc n) env eq refl rewrite eq = loopHelper n -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) +<ul> + <li><strong>loopHelper</strong> は今回のループを解決する証明 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (varn env + vari env ≡ c10 env) +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> loopHelper zero env eq refl rewrite eq = refl +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> loopHelper (suc n) env eq refl rewrite eq = loopHelper n +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> refl (+-suc n (vari env)) </pre></div> </div> -</div> -<ul> - <li><strong>loopHelper</strong> は今回のループを解決する証明</li> - <li>ループ解決のためにループの簡約ができた</li> + </div> + </li> + <li>ここでは任意の回数回る while loop が必ず最終条件を満たす</li> </ul> @@ -531,13 +710,9 @@ <!-- _S9SLIDE_ --> <h2 id="gears-と-hoare-logic-を用いた仕様の証明完成">Gears と Hoare Logic を用いた仕様の証明(完成)</h2> <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> -- whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> -- ( λ env s → conv1 env s -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -- ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- ( λ env s → vari env ≡ c10 env ))) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> ProofGears : (c : ℕ) → whileProofs c -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> ProofGears c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> helperCallwP : (c : ℕ) → whileTestPCallwP' c +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> helperCallwP c = whileTestPwP {_} {_} c +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) </pre></div> </div> </div> @@ -565,6 +740,200 @@ </li> </ul> +<!-- ## Gears について --> +<!-- - **Gears** は当研究室で提案しているプログラム記述手法 --> +<!-- - 処理の単位を **CodeGear** 、データの単位を **DataGear** --> +<!-- - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す --> +<!-- - Output の DataGear は次の CodeGear の Input として接続される --> +<!-- <\!-- [fig1](file://./fig/cgdg.pdf) -\-> --> +<!-- - CodeGear の接続処理などのメタ計算は Meta CodeGear として定義 --> +<!-- - Meta CodeGear で信頼性の検証を行う --> +<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%"/></p> --> +<!-- <\!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> -\-> --> + +<!-- ## Agda での DataGear --> +<!-- - **DataGear** は CodeGear でつかわれる引数をまとめたもの --> +<!-- - Agda は CbC の上位言語 --> +<!-- - メタ計算を含めて記述できる --> +<!-- - DataGear は Agda の CodeGear で使うことのできる**全てのデータ** --> + +<!-- ## Agda での CodeGear --> +<!-- - Agda での CodeGear は継続渡しで記述された関数 --> +<!-- ```AGDA --> +<!-- whileTest : {t : Set} → (c10 : Nat) --> +<!-- → (Code : Env → t) → t --> +<!-- whileTest c10 next = next (record {varn = c10 --> +<!-- ; vari = 0} ) --> +<!-- ``` --> +<!-- - CodeGear の型は継続先を返す関数 --> +<!-- - **(Code : fa → t)** は継続先 --> +<!-- - 引数として継続先の CodeGear を受け取る --> + +<!-- ## Agda での Gears の記述(whileLoop) --> +<!-- - 関数の動作を条件で変えたいときはパターンマッチを行う --> +<!-- ```AGDA --> +<!-- whileLoop : {l : Level} {t : Set l} → Envc --> +<!-- → (next : Envc → t) → (exit : Envc → t) → t --> +<!-- whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env --> +<!-- whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = --> +<!-- next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) --> +<!-- ``` --> +<!-- - whileLoop は varn が 0 より大きい間ループする --> + +<!-- ## Hoare Logic をベースとした Gears での検証手法 --> +<!-- ```C --> +<!-- n = 10; --> +<!-- i = 0; --> + +<!-- while (n>0) --> +<!-- { --> +<!-- i++; --> +<!-- n--; --> +<!-- } --> +<!-- ``` --> +<!-- - 今回 Hoare Logic で証明する次のようなコードを検証した --> +<!-- - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす --> +<!-- - n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる --> + +<!-- ## Gears をベースにしたプログラム --> +<!-- ```AGDA --> +<!-- test : Env --> +<!-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> + +<!-- -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t --> +<!-- -- whileLoop : {t : Set} → Env → (Code : Env → t) → t --> +<!-- ``` --> +<!-- - test は whileTest と whileLoop を実行した結果を返す関数 --> +<!-- - whileTest の継続先にDataGear を受け取って whileLoop に渡す --> +<!-- - **(λ 引数 → )**は無名の関数で引数を受け取って継続する --> + +<!-- ## Gears をベースにした Hoare Logic と証明(全体) --> +<!-- ```AGDA --> +<!-- -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> +<!-- proofGears : {c10 : Nat } → Set --> +<!-- proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → --> +<!-- conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 --> +<!-- (λ n2 → ( vari n2 ≡ c10 )))) --> +<!-- ``` --> +<!-- - proofGears は Hoare Logic をベースとした証明 --> +<!-- - 先程のプログラムと違い、引数として証明も持っている --> +<!-- - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileTest) --> +<!-- ```AGDA --> +<!-- whileTest' : {l : Level} {t : Set l} {c10 : ℕ } --> +<!-- → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t --> +<!-- whileTest' {_} {_} {c10} next = next --> +<!-- (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) --> +<!-- ``` --> +<!-- - 最初の Command なので PreCondition はない --> +<!-- - (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明 --> +<!-- - **_∧_** は pi1 と pi2 のフィールドをもつレコード型 --> +<!-- - 両方とも成り立つので **refl** --> +<!-- - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** --> + +<!-- ## Gears と Hoare Logic をベースにした証明(conversion) --> +<!-- ```AGDA --> +<!-- conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env --> +<!-- conv e record { pi1 = refl ; pi2 = refl } = +zero --> +<!-- ``` --> +<!-- - conv は制約を緩める CodeGear --> +<!-- - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ --> + +<!-- <\!-- ## Hoare Logic の証明 -\-> --> +<!-- <\!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -\-> --> +<!-- <\!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している -\-> --> +<!-- <\!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 -\-> --> +<!-- <\!-- - 変換後の式を次の行に書いて変換を続ける -\-> --> +<!-- <\!-- ```AGDA -\-> --> +<!-- <\!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) -\-> --> +<!-- <\!-- → ((vari env) ≡ 0) ∧ ((varn env) ≡ (c10 env)) -\-> --> +<!-- <\!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t -\-> --> +<!-- <\!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero -\-> --> +<!-- <\!-- ``` -\-> --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileLoop) --> +<!-- ```AGDA --> +<!-- whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env --> +<!-- → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) --> +<!-- → (exit : (env : Envc ) → whileTestStateP sf env → t) → t --> +<!-- whileLoopPwP' zero env refl refl next exit = exit env refl --> +<!-- whileLoopPwP' (suc n) env refl refl next exit = --> +<!-- next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> + +<!-- loopPwP' zero env refl refl exit = exit env refl --> +<!-- loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl --> +<!-- (λ env x y → loopPwP' n env x y exit) exit --> +<!-- ``` --> +<!-- - whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている --> +<!-- - ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る --> + +<!-- ## Gears と Hoare Logic をベースにした仕様記述 --> +<!-- ```AGDA --> +<!-- whileProofs : (c : ℕ ) → Set --> +<!-- whileProofs c = whileTestPwP {_} {_} c --> +<!-- ( λ env s → conv1 env s --> +<!-- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ``` --> +<!-- - **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている --> + +<!-- ## Gears と Hoare Logic を用いた仕様の証明 --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> + +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero --> +<!-- (λ env₁ s₁ → {!!})) --> + +<!-- Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl --> +<!-- +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) --> +<!-- ------------------------------------------------------------ --> +<!-- s₁ : vari env₁ ≡ c10 env₁ --> +<!-- env₁ : Envc --> +<!-- s : (vari env ≡ 0) ∧ (varn env ≡ c10 env) --> +<!-- env : Envc --> +<!-- c : ℕ --> +<!-- ``` --> +<!-- - 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく --> +<!-- - しかし loopPwP' のループが進まず証明できない --> + +<!-- ## 検証時の Loop の解決 --> +<!-- ```AGDA --> +<!-- loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) --> +<!-- → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) --> +<!-- loopHelper zero env eq refl rewrite eq = refl --> +<!-- loopHelper (suc n) env eq refl rewrite eq = loopHelper n --> +<!-- (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> +<!-- ``` --> +<!-- - **loopHelper** は今回のループを解決する証明 --> +<!-- - ループ解決のためにループの簡約ができた --> + +<!-- ## Gears と Hoare Logic を用いた仕様の証明(完成) --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) --> +<!-- ``` --> +<!-- - **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた --> + +<!-- ## まとめと今後の課題 --> +<!-- - CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した --> +<!-- - Hoare Logic ベースの検証を実際に行うことができた --> +<!-- - 証明時の任意回の有限ループに対する解決を行えた --> +<!-- - 今後の課題 --> +<!-- - BinaryTree の有限ループに対する証明 --> +<!-- - Hoare Logic で検証されたコードの CbC 変換 --> +<!-- - 並列実行での検証 --> + </div>
--- a/slide/slide.md Tue Feb 11 02:31:26 2020 +0900 +++ b/slide/slide.md Wed Feb 12 05:02:27 2020 +0900 @@ -1,13 +1,44 @@ -title: Continuation based C での Hoare Logic を用いた記述と検証 +title: Continuation based C での Hoare Logic を用いた仕様記述と検証 author: 外間政尊 profile: - 琉球大学 : 並列信頼研究室 lang: Japanese <!-- 発表30~40分、質疑応答20~30分くらい…? --> <!-- TODO -- 章構成を slide.mm の形に直す。 -- Agda の説明と Gears の説明をなおす -- Gears での Hoare Logic の説明する前になんで Hoare Logic ベースなのかのスライドを入れてみる +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- HoareLogic + - hoare logic の説明 + - while program + + +- 使う Agda のイントロ + - and と lambda + - でーた分け? + +- Hoare logic と agda + - while program + - hoare logic の while program + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ --> @@ -17,11 +48,9 @@ - 信頼性を上げるために仕様の検証が必要 - 検証にはモデル検査や**定理証明**などが存在する - また、仕様検証の手法として **Hoare Logic** がある - - プログラムを書く上である関数は実行する前に必要な引数があって何らかの出力がある + - 通常の関数でも実行する前に必要な引数があって何らかの出力がある - Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ - <!-- - 関数実行前に、引数が存在していて、出力が意図した通りになる --> -- Hoare Logic では関数が最低限のコマンドまで分割されており記述が困難(変数の代入、コマンド実行の遷移等) -- 大規模なプログラムは構築しづらい +- Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等) ## Hoare Logic をベースにした Gears 単位での検証 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 @@ -30,240 +59,358 @@ - 定理証明支援機の Agda 上で Gears 単位を用いた検証を行う - 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する -## Agda のデータ型 -- **データ型**はプリミティブなデータ -- この型のとき値は一意に定まる -```SHELL - data Nat : Set where - zero : Nat - suc : Nat → Nat + +<!-- ## 証明の基礎 --> +<!-- - A は論理式を表す変数、もしくは型Aという集合 --> +<!-- - 論理式は変数と論理演算子で表される --> +<!-- - 変数や演算子は構文要素 --> + +<!-- ``` --> +<!-- A → B --> +<!-- ``` --> +<!-- - A → B は 「A ならば B」 --> +<!-- - 関数としてみると A を受け取って B を返す関数 --> +<!-- - A を仮定したとき B が証明される --> +<!-- <\!-- ``` -\-> --> +<!-- <\!-- A -\-> --> +<!-- <\!-- --------- -\-> --> +<!-- <\!-- B -\-> --> +<!-- <\!-- ``` -\-> --> + + +<!-- ## 関数適用による証明 --> +<!-- - --> + +<!-- ``` --> +<!-- λ x → y --> +<!-- ``` --> +<!-- - x は変数 y は項 --> +<!-- - x は関数の引数と同じ扱い --> +<!-- - 項には型が対応し、再帰的に定義される --> +<!-- ``` --> +<!-- x : A --> +<!-- ``` --> +<!-- - x という項が型A を持つことを表す --> +<!-- x : A かつ y : B のとき --> +<!-- ``` --> +<!-- λ x → y : A → B --> +<!-- ``` --> +<!-- となる --> + +## Agda +- Agda は関数型言語 +```AGAD + name : type + name = value ``` -- **レコード型**は複数のデータをまとめる -- 複数の値を保持できる -```SHELL - record Env : Set where - field - varn : Nat - vari : Nat +- 関数には型と定義を与える + - 型は **:** で、 値は **=** で与える +- 仮定なしに使えるのは Set のみ +- 構成要素としては以下の3種類 + 1. 関数 + - 型は A → B + - 値は λ x → y + 1. record + 1. data +- つぎは record と data について + +## Agda の record とその例 ∧ +- 2つのものが同時に存在すること +- A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B +- Agda ではこのような同時に存在する型を **record** で書く +```AGDA + record _∧_ (A B : Set) : Set + field + pi1 : A + pi2 : B +``` +- _∧_ は中間記法、変数が入る位置を _ で示せる +- 実際の構築は x : A かつ y : B のとき +```AGDA + record {pi1 = x ; pi2 = y} +``` +- のように記述する +- C での構造体のようなもの + +## Agda の data とその例 Sum +- 一つでも存在すること +- A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B +- どちらかが成り立つ型を **data** で書く +```AGDA + data _∨_ (A B : Set) : Set where + p1 : A → A ∨ B + p2 : B → A ∨ B +``` +- のように記述できる +- C での union のようなもの +- p1、 p2 は case 文みたいな + +- 次は Hoare Logic + +## Hoare Logic +- Hoare Logic はプログラム検証の手法 +- 事前条件(P)が成り立つとき、コマンド(C)を実行すると事後条件(Q)が成り立つ + - **{P} C {Q}** の形で表される + - コマンドが制限されてる +- 今回は以下のような while program を検証する +- n = 10 となっているが検証では n は任意の自然数 +```C + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +``` +- 次は Agda の Hoare Logic で while program をみる + +## Agda での Hoare Logic +- Hoare Logic のプログラムは Command で構成される +- Comm は data で記述されたコマンド +- このコマンドを使って while program を構築する +```AGDA + data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm → Comm + Seq : Comm → Comm → Comm + If : Cond → Comm → Comm → Comm + While : Cond → Comm → Comm ``` -## Agda の関数 -- 関数にも同様に型が必要 -```HASKELL - +1 : ℕ → ℕ - +1 m = suc m +## Hoare Logic での while program +- C の while program +```C + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +``` +- Hoare Logic での while program +```AGDA + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +``` +- 次は Hoare Logic での検証 - -- eval +1 zero - -- return suc zero -``` -- 関数の型は **input → output** -- 複数入力がある場合は **input1 → input2 → output** -- **=** の左側は関数名と引数、右側に実装 +<!-- TODO +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ +--> -## Agda での証明 -- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出** -```HASKELL - +zero : { y : Nat } → y + zero ≡ y - +zero {zero} = refl - +zero {suc y} = cong suc ( +zero {y} ) +## Hoare Logic での Command に対応する仕様 +- Command に対応する証明がある +```AGDA + data HTProof : Cond → Comm → Cond → Set where + PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → + (pr : Axiom bPre pcm bPost) → + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) → HTProof b Skip b + AbortRule : (bPre : Cond) → (bPost : Cond) → + HTProof bPre Abort bPost + WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → + {bPost' : Cond} → {bPost : Cond} → + Tautology bPre bPre' → + HTProof bPre' cm bPost' → + Tautology bPost' bPost → + HTProof bPre cm bPost + SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → + {cm2 : Comm} → {bPost : Cond} → + HTProof bPre cm1 bMid → + HTProof bMid cm2 bPost → + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} → {cmElse : Comm} → + {bPre : Cond} → {bPost : Cond} → + {b : Cond} → + HTProof (bPre and b) cmThen bPost → + HTProof (bPre and neg b) cmElse bPost → + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → + HTProof (bInv and b) cm bInv → + HTProof bInv (While b cm) (bInv and neg b) ``` -- **refl** は **x ≡ x** -- **cong** は **関数** と等式を受け取って、等式の両辺に関数を適応しても等しくなること -- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明 - - **y = zero** のときは **zero ≡ zero** のため refl - - **y = suc y** のときは cong を使い y の数を減らして帰納的に証明している +- 検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある -## Gears について -- **Gears** は当研究室で提案しているプログラム記述手法 -- 処理の単位を **CodeGear** 、データの単位を **DataGear** +## Hoare Logic での 仕様記述と部分正当性 +- HTProof で記述した仕様 +- lemma は事前条件からコマンドを通して事後条件が成り立つこと(部分正当性)の証明(長いので省略) +```AGDA + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +``` +- 比較のために元の while program +```AGDA + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +``` +- Command と対応した仕様があるため形がほぼ一緒 + - while ループするときに強い条件を緩めている規則が違うくらい(Weacening Rule) +- proof1 は HTProof が正しく繋げることで部分正当性まで証明 + +## Hoare Logic での健全性の証明 +- proof1 は部分正当性を示せた +- 実際に正しく動作すること(健全性)を証明する必要がある +- Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す +- PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する +```AGDA + PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost + PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +``` +- proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している +```AGDA + proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true + proofOfProgram c10 input output ic sem = + PrimSoundness (proof1 c10) input output ic sem +``` + + +## Continuation based C について +- Continuation based C (CbC) は当研究室で開発してるプログラミング言語 +- CbC では処理の単位を **CodeGear** 、データの単位を **DataGear** とする - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す - Output の DataGear は次の CodeGear の Input として接続される -<!-- [fig1](file://./fig/cgdg.pdf) --> - CodeGear の接続処理などのメタ計算は Meta CodeGear として定義 - Meta CodeGear で信頼性の検証を行う <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%"/></p> -<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> --> - -## Agda での DataGear -- **DataGear** は CodeGear でつかわれる引数をまとめたもの -- Agda は CbC の上位言語 - - メタ計算を含めて記述できる -- DataGear は Agda の CodeGear で使うことのできる**全てのデータ** - - -## Agda での CodeGear -- Agda での CodeGear は継続渡しで記述された関数 -```AGDA - whileTest : {t : Set} → (c10 : Nat) - → (Code : Env → t) → t - whileTest c10 next = next (record {varn = c10 - ; vari = 0} ) -``` -- CodeGear の型は継続先を返す関数 -- **(Code : fa → t)** は継続先 -- 引数として継続先の CodeGear を受け取る - -## Agda での Gears の記述(whileLoop) -- 関数の動作を条件で変えたいときはパターンマッチを行う -```AGDA - whileLoop : {l : Level} {t : Set l} → Envc - → (next : Envc → t) → (exit : Envc → t) → t - whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env - whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = - next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) -``` -- whileLoop は varn が 0 より大きい間ループする - - -## Hoare Logic をベースとした Gears での検証手法 -```C - n = 10; - i = 0; - - while (n>0) - { - i++; - n--; - } -``` -- 今回 Hoare Logic で証明する次のようなコードを検証した -- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす -- n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる - -## Gears をベースにしたプログラム -```AGDA - test : Env - test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) - - -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t - -- whileLoop : {t : Set} → Env → (Code : Env → t) → t -``` -- test は whileTest と whileLoop を実行した結果を返す関数 -- whileTest の継続先にDataGear を受け取って whileLoop に渡す - - **(λ 引数 → )**は無名の関数で引数を受け取って継続する -## Gears をベースにした Hoare Logic と証明(全体) +## CbC での Hoare Logic +- CodeGear、DataGear を用いた Hoare Logic は図のようになる +<p style="text-align:center;"><img src="./fig/hoare-cg-dg.svg" alt="" width="60%" height="60%"/></p> +- CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる + +## CbC での while program +- 比較用の Hoare Logic での while program ```AGDA - -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) - proofGears : {c10 : Nat } → Set - proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → - conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 - (λ n2 → ( vari n2 ≡ c10 )))) -``` -- proofGears は Hoare Logic をベースとした証明 - - 先程のプログラムと違い、引数として証明も持っている -- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい - -## Gears と Hoare Logic をベースにした証明(whileTest) -```AGDA - whileTest' : {l : Level} {t : Set l} {c10 : ℕ } - → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t - whileTest' {_} {_} {c10} next = next - (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) ``` -- 最初の Command なので PreCondition はない -- (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明 - - **_∧_** は pi1 と pi2 のフィールドをもつレコード型 - - 両方とも成り立つので **refl** -- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** - -## Gears と Hoare Logic をベースにした証明(conversion) +- CbC での while program ```AGDA - conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env - conv e record { pi1 = refl ; pi2 = refl } = +zero + whileTestPCall : (c10 : ℕ ) → Envc + whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env)) ``` -- conv は制約を緩める CodeGear - - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ +- whileTestP' が n = c10、 i = 0 の代入、 loopP' が while loop に対応している +- CbC での Hoare Logic 上でコマンドは CodeGear そのもの + - CodeGear は Hoare Logic のコマンドより自由な記述 -<!-- ## Hoare Logic の証明 --> -<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している --> -<!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している --> -<!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 --> -<!-- - 変換後の式を次の行に書いて変換を続ける --> -<!-- ```AGDA --> -<!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) --> -<!-- → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env)) --> -<!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t --> -<!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero --> -<!-- ``` --> - -## Gears と Hoare Logic をベースにした証明(whileLoop) +## CbC での HTProof +- HTProof に対応するものは各 Meta CodeGear に条件を渡したもの +- それぞれが事前条件から事後条件を導く証明を持っている ```AGDA - whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env - → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) - → (exit : (env : Envc ) → whileTestStateP sf env → t) → t - whileLoopPwP' zero env refl refl next exit = exit env refl - whileLoopPwP' (suc n) env refl refl next exit = - next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) - - loopPwP' zero env refl refl exit = exit env refl - loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl - (λ env x y → loopPwP' n env x y exit) exit + whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) + → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t + whileTestPwP c10 next = + next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl }) ``` -- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている -- ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る - - -## Gears と Hoare Logic をベースにした仕様記述 +- whileTestPCallwP' は Hoare Logic の HTProof 記述 proof1 に相当 +- 比較用 proof1 ```AGDA - whileProofs : (c : ℕ ) → Set - whileProofs c = whileTestPwP {_} {_} c - ( λ env s → conv1 env s - ( λ env s → loopPwP' (varn env) env refl s - ( λ env s → vari env ≡ c10 env ))) + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 ``` -- **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている +- proof1 の lemma に相当する証明は Meta CodeGear で、継続先の CodeGear に渡す条件の証明 +```AGDA + whileTestPCallwP' : (c : ℕ ) → Set + whileTestPCallwP' c = whileTestPwP {_} {_} c ( + λ env s → loopPwP' (varn env) env refl (conv env s) + ( λ env s → vari env ≡ c10 env ) ) +``` +- Hoare Logic では実装、部分正当性を分けて記述していた +- CbC での Hoare Logic は実装と部分正当性を一体化できる - - -## Gears と Hoare Logic を用いた仕様の証明 +## CbC での Soundness +- 先程の whileTestPCallwP' を命題として証明すると健全性が示せる ```AGDA --- whileProofs c = whileTestPwP {_} {_} c --- ( λ env s → conv1 env s --- ( λ env s → loopPwP' (varn env) env refl s --- ( λ env s → vari env ≡ c10 env ))) - - ProofGears : (c : ℕ) → whileProofs c - ProofGears c = whileTestPwP {_} {_} c - (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero - (λ env₁ s₁ → {!!})) - - Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl - +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) - ———————————————————————————————————————————————————————————— - s₁ : vari env₁ ≡ c10 env₁ - env₁ : Envc - s : (vari env ≡ 0) /\ (varn env ≡ c10 env) - env : Envc - c : ℕ + whileTestPCallwP' : (c : ℕ ) → Set + whileTestPCallwP' c = whileTestPwP {_} {_} c ( + λ env s → loopPwP' (varn env) env refl (conv env s) + ( λ env s → vari env ≡ c10 env ) ) ``` -- 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく -- しかし loopPwP' のループが進まず証明できない +- 実際に値が入ると命題は成り立つが任意の値だと停止せず証明が終わらない +```AGDA + whileCallwP : (c : ℕ) → whileTestPCallwP' c + whileCallwP c = whileTestPwP {_} {_} c (λ env s → + loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) +``` ## 検証時の Loop の解決 +- **loopHelper** は今回のループを解決する証明 ```AGDA - loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) - → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) - loopHelper zero env eq refl rewrite eq = refl - loopHelper (suc n) env eq refl rewrite eq = loopHelper n - (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) + loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) + → (varn env + vari env ≡ c10 env) + → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) + loopHelper zero env eq refl rewrite eq = refl + loopHelper (suc n) env eq refl rewrite eq = loopHelper n + (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) + refl (+-suc n (vari env)) ``` -- **loopHelper** は今回のループを解決する証明 -- ループ解決のためにループの簡約ができた +- ここでは任意の回数回る while loop が必ず最終条件を満たす ## Gears と Hoare Logic を用いた仕様の証明(完成) ```AGDA - -- whileProofs c = whileTestPwP {_} {_} c - -- ( λ env s → conv1 env s - -- ( λ env s → loopPwP' (varn env) env refl s - -- ( λ env s → vari env ≡ c10 env ))) - ProofGears : (c : ℕ) → whileProofs c - ProofGears c = whileTestPwP {_} {_} c - (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) + helperCallwP : (c : ℕ) → whileTestPCallwP' c + helperCallwP c = whileTestPwP {_} {_} c + (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) ``` -- **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた + - **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた ## まとめと今後の課題 - CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した @@ -273,3 +420,236 @@ - BinaryTree の有限ループに対する証明 - Hoare Logic で検証されたコードの CbC 変換 - 並列実行での検証 + + +<!-- ## Gears について --> +<!-- - **Gears** は当研究室で提案しているプログラム記述手法 --> +<!-- - 処理の単位を **CodeGear** 、データの単位を **DataGear** --> +<!-- - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す --> +<!-- - Output の DataGear は次の CodeGear の Input として接続される --> +<!-- <\!-- [fig1](file://./fig/cgdg.pdf) -\-> --> +<!-- - CodeGear の接続処理などのメタ計算は Meta CodeGear として定義 --> +<!-- - Meta CodeGear で信頼性の検証を行う --> +<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%"/></p> --> +<!-- <\!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> -\-> --> + +<!-- ## Agda での DataGear --> +<!-- - **DataGear** は CodeGear でつかわれる引数をまとめたもの --> +<!-- - Agda は CbC の上位言語 --> +<!-- - メタ計算を含めて記述できる --> +<!-- - DataGear は Agda の CodeGear で使うことのできる**全てのデータ** --> + + +## Agda での CodeGear +- Agda での CodeGear は継続渡しで記述された関数 +```AGDA + whileTest : {t : Set} → (c10 : Nat) + → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 + ; vari = 0} ) + ``` + - CodeGear の型は継続先を返す関数 + - **(Code : fa → t)** は継続先 + - 引数として継続先の CodeGear を受け取る + +<!-- ## Agda での Gears の記述(whileLoop) --> +<!-- - 関数の動作を条件で変えたいときはパターンマッチを行う --> +<!-- ```AGDA --> +<!-- whileLoop : {l : Level} {t : Set l} → Envc --> +<!-- → (next : Envc → t) → (exit : Envc → t) → t --> +<!-- whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env --> +<!-- whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = --> +<!-- next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) --> +<!-- ``` --> +<!-- - whileLoop は varn が 0 より大きい間ループする --> + + +<!-- ## Hoare Logic をベースとした Gears での検証手法 --> +<!-- ```C --> +<!-- n = 10; --> +<!-- i = 0; --> + +<!-- while (n>0) --> +<!-- { --> +<!-- i++; --> +<!-- n--; --> +<!-- } --> +<!-- ``` --> +<!-- - 今回 Hoare Logic で証明する次のようなコードを検証した --> +<!-- - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす --> +<!-- - n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる --> + +<!-- ## Gears をベースにしたプログラム --> +<!-- ```AGDA --> +<!-- test : Env --> +<!-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> + +<!-- -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t --> +<!-- -- whileLoop : {t : Set} → Env → (Code : Env → t) → t --> +<!-- ``` --> +<!-- - test は whileTest と whileLoop を実行した結果を返す関数 --> +<!-- - whileTest の継続先にDataGear を受け取って whileLoop に渡す --> +<!-- - **(λ 引数 → )**は無名の関数で引数を受け取って継続する --> + + +<!-- ## Gears をベースにした Hoare Logic と証明(全体) --> +<!-- ```AGDA --> +<!-- -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> +<!-- proofGears : {c10 : Nat } → Set --> +<!-- proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → --> +<!-- conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 --> +<!-- (λ n2 → ( vari n2 ≡ c10 )))) --> +<!-- ``` --> +<!-- - proofGears は Hoare Logic をベースとした証明 --> +<!-- - 先程のプログラムと違い、引数として証明も持っている --> +<!-- - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileTest) --> +<!-- ```AGDA --> +<!-- whileTest' : {l : Level} {t : Set l} {c10 : ℕ } --> +<!-- → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t --> +<!-- whileTest' {_} {_} {c10} next = next --> +<!-- (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) --> +<!-- ``` --> +<!-- - 最初の Command なので PreCondition はない --> +<!-- - (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明 --> +<!-- - **_∧_** は pi1 と pi2 のフィールドをもつレコード型 --> +<!-- - 両方とも成り立つので **refl** --> +<!-- - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** --> + +<!-- ## Gears と Hoare Logic をベースにした証明(conversion) --> +<!-- ```AGDA --> +<!-- conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env --> +<!-- conv e record { pi1 = refl ; pi2 = refl } = +zero --> +<!-- ``` --> +<!-- - conv は制約を緩める CodeGear --> +<!-- - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ --> + +<!-- <\!-- ## Hoare Logic の証明 -\-> --> +<!-- <\!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -\-> --> +<!-- <\!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している -\-> --> +<!-- <\!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 -\-> --> +<!-- <\!-- - 変換後の式を次の行に書いて変換を続ける -\-> --> +<!-- <\!-- ```AGDA -\-> --> +<!-- <\!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) -\-> --> +<!-- <\!-- → ((vari env) ≡ 0) ∧ ((varn env) ≡ (c10 env)) -\-> --> +<!-- <\!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t -\-> --> +<!-- <\!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero -\-> --> +<!-- <\!-- ``` -\-> --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileLoop) --> +<!-- ```AGDA --> +<!-- whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env --> +<!-- → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) --> +<!-- → (exit : (env : Envc ) → whileTestStateP sf env → t) → t --> +<!-- whileLoopPwP' zero env refl refl next exit = exit env refl --> +<!-- whileLoopPwP' (suc n) env refl refl next exit = --> +<!-- next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> + +<!-- loopPwP' zero env refl refl exit = exit env refl --> +<!-- loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl --> +<!-- (λ env x y → loopPwP' n env x y exit) exit --> +<!-- ``` --> +<!-- - whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている --> +<!-- - ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る --> + + +<!-- ## Gears と Hoare Logic をベースにした仕様記述 --> +<!-- ```AGDA --> +<!-- whileProofs : (c : ℕ ) → Set --> +<!-- whileProofs c = whileTestPwP {_} {_} c --> +<!-- ( λ env s → conv1 env s --> +<!-- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ``` --> +<!-- - **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている --> + + + +<!-- ## Gears と Hoare Logic を用いた仕様の証明 --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> + +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero --> +<!-- (λ env₁ s₁ → {!!})) --> + +<!-- Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl --> +<!-- +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) --> +<!-- ———————————————————————————————————————————————————————————— --> +<!-- s₁ : vari env₁ ≡ c10 env₁ --> +<!-- env₁ : Envc --> +<!-- s : (vari env ≡ 0) ∧ (varn env ≡ c10 env) --> +<!-- env : Envc --> +<!-- c : ℕ --> +<!-- ``` --> +<!-- - 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく --> +<!-- - しかし loopPwP' のループが進まず証明できない --> + + +<!-- ## 検証時の Loop の解決 --> +<!-- ```AGDA --> +<!-- loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) --> +<!-- → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) --> +<!-- loopHelper zero env eq refl rewrite eq = refl --> +<!-- loopHelper (suc n) env eq refl rewrite eq = loopHelper n --> +<!-- (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> +<!-- ``` --> +<!-- - **loopHelper** は今回のループを解決する証明 --> +<!-- - ループ解決のためにループの簡約ができた --> + +<!-- ## Gears と Hoare Logic を用いた仕様の証明(完成) --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) --> +<!-- ``` --> +<!-- - **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた --> + +## まとめと今後の課題 +- CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した +- Hoare Logic ベースの検証を実際に行うことができた +- 証明時の任意回の有限ループに対する解決を行えた +- 今後の課題 + - BinaryTree の有限ループに対する証明 + - Hoare Logic で検証されたコードの CbC 変換 + - 並列実行での検証 + + +```AGDA +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input ) → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) + → (loopeq : output ≡ loopPP n current eq) + → (whileTestStateP s2 current ) + → (whileTestStateP s2 current ) implies (vari output ≡ c10 output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) +``` + +```AGDA +whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → varn input + vari input ≡ c10 input + → (next : (output : Envc ) + → (varn input + vari input ≡ c10 input) implies (varn output + vari output ≡ c10 output ) → t) + → (exit : (output : Envc ) + → (varn input + vari input ≡ c10 input ) implies (vari env) ≡ (c10 env) → t) → t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (λ z → z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) + (proof λ x → +-suc varn (vari env) ) +```
--- a/slide/slide.mm Tue Feb 11 02:31:26 2020 +0900 +++ b/slide/slide.mm Wed Feb 12 05:02:27 2020 +0900 @@ -34,17 +34,18 @@ <node CREATED="1581159235461" ID="ID_1980578968" MODIFIED="1581159362207" POSITION="left" TEXT="Gears の説明と Agda の説明と 証明が雑"> <node CREATED="1581164400268" ID="ID_884941803" MODIFIED="1581164423164" TEXT="多分順番がおかしいので整理した順に書く"/> </node> -<node CREATED="1581159372515" ID="ID_336006559" MODIFIED="1581159381847" POSITION="right" TEXT="研究のはなし"> +<node CREATED="1581406799922" ID="ID_1493747452" MODIFIED="1581406802912" POSITION="left" TEXT="old slide"> +<node CREATED="1581159372515" ID="ID_336006559" MODIFIED="1581159381847" TEXT="研究のはなし"> <node CREATED="1581159415904" ID="ID_59023356" MODIFIED="1581159618819" TEXT="Hoare Logic の話"/> </node> -<node CREATED="1581159382448" ID="ID_183626889" MODIFIED="1581159393008" POSITION="right" TEXT="Agda の説明"> +<node CREATED="1581159382448" ID="ID_183626889" MODIFIED="1581159393008" TEXT="Agda の説明"> <node CREATED="1581159474054" ID="ID_81428977" MODIFIED="1581159478593" TEXT="Data"/> <node CREATED="1581159479227" ID="ID_70865913" MODIFIED="1581159484369" TEXT="Function"/> </node> -<node CREATED="1581159393393" ID="ID_614580744" MODIFIED="1581159397656" POSITION="right" TEXT="Agda での検証"> +<node CREATED="1581159393393" ID="ID_614580744" MODIFIED="1581159397656" TEXT="Agda での検証"> <node CREATED="1581159489358" ID="ID_1464632287" MODIFIED="1581159493858" TEXT="Proof"/> </node> -<node CREATED="1581159405966" ID="ID_153385067" MODIFIED="1581159415464" POSITION="right" TEXT="Gears と Agda の関連"> +<node CREATED="1581159405966" ID="ID_153385067" MODIFIED="1581159415464" TEXT="Gears と Agda の関連"> <node CREATED="1581159398128" ID="ID_176678065" MODIFIED="1581159679321" TEXT="Gears 単位の導入"> <node CREATED="1581159496107" ID="ID_1607974660" MODIFIED="1581159500106" TEXT="CodeGear"/> <node CREATED="1581159500654" ID="ID_1915254834" MODIFIED="1581159502649" TEXT="DataGear"/> @@ -53,11 +54,26 @@ <node CREATED="1581159534059" ID="ID_1701708289" MODIFIED="1581159544036" TEXT="DataGearのAgdaでの表現"/> <node CREATED="1581159566200" ID="ID_1511225703" MODIFIED="1581159579785" TEXT="? Gears での 証明"/> </node> -<node CREATED="1581159809871" ID="ID_1922620165" MODIFIED="1581164444772" POSITION="right" TEXT="Hoare Logic ベースの利点(再掲?)"/> -<node CREATED="1581159427576" ID="ID_1884090787" MODIFIED="1581159443449" POSITION="right" TEXT="Hoare Logic と Gears 単位"> +<node CREATED="1581159809871" ID="ID_1922620165" MODIFIED="1581164444772" TEXT="Hoare Logic ベースの利点(再掲?)"/> +<node CREATED="1581159427576" ID="ID_1884090787" MODIFIED="1581159443449" TEXT="Hoare Logic と Gears 単位"> <node CREATED="1581159772603" ID="ID_311212543" MODIFIED="1581159793096" TEXT="CodeGear での Hoare Logic の導入"/> <node CREATED="1581159461250" ID="ID_35745602" MODIFIED="1581159796485" TEXT="検証"/> </node> -<node CREATED="1581159434680" ID="ID_1776891719" MODIFIED="1581159449569" POSITION="right" TEXT="まとめ"/> +<node CREATED="1581159434680" ID="ID_1776891719" MODIFIED="1581159449569" TEXT="まとめ"/> +</node> +<node CREATED="1581406815657" ID="ID_978178001" MODIFIED="1581406822296" POSITION="right" TEXT="slide"> +<node CREATED="1581406822607" ID="ID_1611425820" MODIFIED="1581406832777" TEXT="問題意識"> +<node CREATED="1581406853477" ID="ID_1488399797" MODIFIED="1581406858554" TEXT="OS の信頼性を上げたい"/> +<node CREATED="1581406859259" ID="ID_680920276" MODIFIED="1581406873755" TEXT="信頼性には仕様検証がよい"/> +<node CREATED="1581406874282" ID="ID_627893567" MODIFIED="1581406930253" TEXT="仕様検証には Hoare Logic がある"/> +<node CREATED="1581406884214" ID="ID_1733507053" MODIFIED="1581406902908" TEXT="今の Hoare Logic は厳しい"/> +</node> +<node CREATED="1581406833394" ID="ID_335098629" MODIFIED="1581406845433" TEXT="本発表の趣旨"> +<node CREATED="1581406936589" ID="ID_1522497629" MODIFIED="1581406965245" TEXT="GodeGear DataGear で Hoare Logic ベースの検証"> +<node CREATED="1581406966598" ID="ID_901893261" MODIFIED="1581406976246" TEXT="従来の Hoare Logic より柔軟に"/> +<node CREATED="1581406976601" ID="ID_447245907" MODIFIED="1581406976601" TEXT=""/> +</node> +</node> +</node> </node> </map>
--- a/slide/slide.pdf.html Tue Feb 11 02:31:26 2020 +0900 +++ b/slide/slide.pdf.html Wed Feb 12 05:02:27 2020 +0900 @@ -7,7 +7,7 @@ <html> <head> <meta http-equiv="content-type" content="text/html;charset=utf-8"> - <title>Continuation based C での Hoare Logic を用いた記述と検証</title> + <title>Continuation based C での Hoare Logic を用いた仕様記述と検証</title> <meta name="generator" content="Slide Show (S9) v4.0.1 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]"> <meta name="author" content="外間政尊" > @@ -55,7 +55,7 @@ <tr> <td> <div align="center"> - <h1><font color="#808db5">Continuation based C での Hoare Logic を用いた記述と検証</font></h1> + <h1><font color="#808db5">Continuation based C での Hoare Logic を用いた仕様記述と検証</font></h1> </div> </td> </tr> @@ -75,9 +75,40 @@ <div class='slide'> <!-- 発表30~40分、質疑応答20~30分くらい…? --> <!-- TODO -- 章構成を slide.mm の形に直す。 -- Agda の説明と Gears の説明をなおす -- Gears での Hoare Logic の説明する前になんで Hoare Logic ベースなのかのスライドを入れてみる +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- HoareLogic + - hoare logic の説明 + - while program + + +- 使う Agda のイントロ + - and と lambda + - でーた分け? + +- Hoare logic と agda + - while program + - hoare logic の while program + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ --> @@ -89,13 +120,11 @@ <li>検証にはモデル検査や<strong>定理証明</strong>などが存在する</li> <li>また、仕様検証の手法として <strong>Hoare Logic</strong> がある <ul> - <li>プログラムを書く上である関数は実行する前に必要な引数があって何らかの出力がある</li> - <li>Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ -<!-- - 関数実行前に、引数が存在していて、出力が意図した通りになる --></li> + <li>通常の関数でも実行する前に必要な引数があって何らかの出力がある</li> + <li>Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ</li> </ul> </li> - <li>Hoare Logic では関数が最低限のコマンドまで分割されており記述が困難(変数の代入、コマンド実行の遷移等)</li> - <li>大規模なプログラムは構築しづらい</li> + <li>Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等)</li> </ul> @@ -113,31 +142,190 @@ <li>本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する</li> </ul> +<!-- ## 証明の基礎 --> +<!-- - A は論理式を表す変数、もしくは型Aという集合 --> +<!-- - 論理式は変数と論理演算子で表される --> +<!-- - 変数や演算子は構文要素 --> + +<!-- ``` --> +<!-- A → B --> +<!-- ``` --> +<!-- - A → B は 「A ならば B」 --> +<!-- - 関数としてみると A を受け取って B を返す関数 --> +<!-- - A を仮定したとき B が証明される --> +<!-- <\!-- ``` -\-> --> +<!-- <\!-- A -\-> --> +<!-- <\!-- --------- -\-> --> +<!-- <\!-- B -\-> --> +<!-- <\!-- ``` -\-> --> + +<!-- ## 関数適用による証明 --> +<!-- - --> + +<!-- ``` --> +<!-- λ x → y --> +<!-- ``` --> +<!-- - x は変数 y は項 --> +<!-- - x は関数の引数と同じ扱い --> +<!-- - 項には型が対応し、再帰的に定義される --> +<!-- ``` --> +<!-- x : A --> +<!-- ``` --> +<!-- - x という項が型A を持つことを表す --> +<!-- x : A かつ y : B のとき --> +<!-- ``` --> +<!-- λ x → y : A → B --> +<!-- ``` --> +<!-- となる --> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda">Agda</h2> +<ul> + <li>Agda は関数型言語 + <div class="language-AGAD highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> name : type +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> name = value +</pre></div> +</div> + </div> + </li> + <li>関数には型と定義を与える + <ul> + <li>型は <strong>:</strong> で、 値は <strong>=</strong> で与える</li> + </ul> + </li> + <li>仮定なしに使えるのは Set のみ</li> + <li>構成要素としては以下の3種類 + <ol> + <li>関数 + <ul> + <li>型は A → B</li> + <li>値は λ x → y</li> + </ul> + </li> + <li>record</li> + <li>data</li> + </ol> + </li> + <li>つぎは record と data について</li> +</ul> + </div> <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-のデータ型">Agda のデータ型</h2> +<h2 id="agda-の-record-とその例-">Agda の record とその例 ∧</h2> <ul> - <li><strong>データ型</strong>はプリミティブなデータ</li> - <li>この型のとき値は一意に定まる - <div class="language-SHELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Nat : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> zero : Nat -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> suc : Nat → Nat + <li>2つのものが同時に存在すること</li> + <li>A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B</li> + <li>Agda ではこのような同時に存在する型を <strong>record</strong> で書く + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record _∧_ (A B : Set) : Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> pi1 : A +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> pi2 : B +</pre></div> +</div> + </div> + </li> + <li><em>∧</em> は中間記法、変数が入る位置を _ で示せる</li> + <li>実際の構築は x : A かつ y : B のとき + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record {pi1 = x ; pi2 = y} +</pre></div> +</div> + </div> + </li> + <li>のように記述する</li> + <li>C での構造体のようなもの</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda-の-data-とその例-sum">Agda の data とその例 Sum</h2> +<ul> + <li>一つでも存在すること</li> + <li>A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B</li> + <li>どちらかが成り立つ型を <strong>data</strong> で書く + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data _∨_ (A B : Set) : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> p1 : A → A ∨ B +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> p2 : B → A ∨ B </pre></div> </div> </div> </li> - <li><strong>レコード型</strong>は複数のデータをまとめる</li> - <li>複数の値を保持できる - <div class="language-SHELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : Nat -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : Nat + <li>のように記述できる</li> + <li>C での union のようなもの</li> + <li> + <p>p1、 p2 は case 文みたいな</p> + </li> + <li>次は Hoare Logic</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic">Hoare Logic</h2> +<ul> + <li>Hoare Logic はプログラム検証の手法</li> + <li>事前条件(P)が成り立つとき、コマンド(C)を実行すると事後条件(Q)が成り立つ + <ul> + <li><strong>{P} C {Q}</strong> の形で表される</li> + <li>コマンドが制限されてる</li> + </ul> + </li> + <li>今回は以下のような while program を検証する</li> + <li>n = 10 となっているが検証では n は任意の自然数 + <div class="language-C highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } +</pre></div> +</div> + </div> + </li> + <li>次は Agda の Hoare Logic で while program をみる</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda-での-hoare-logic">Agda での Hoare Logic</h2> +<ul> + <li>Hoare Logic のプログラムは Command で構成される</li> + <li>Comm は data で記述されたコマンド</li> + <li>このコマンドを使って while program を構築する + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Comm : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Skip : Comm +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Abort : Comm +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> PComm : PrimComm → Comm +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> Seq : Comm → Comm → Comm +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> If : Cond → Comm → Comm → Comm +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> While : Cond → Comm → Comm </pre></div> </div> </div> @@ -150,22 +338,104 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-の関数">Agda の関数</h2> +<h2 id="hoare-logic-での-while-program">Hoare Logic での while program</h2> <ul> - <li>関数にも同様に型が必要 - <div class="language-HASKELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> +1 : ℕ → ℕ -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> +1 m = suc m + <li>C の while program + <div class="language-C highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; <span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- eval +1 zero -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> -- return suc zero +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } +</pre></div> +</div> + </div> + </li> + <li>Hoare Logic での while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li>関数の型は <strong>input → output</strong></li> - <li>複数入力がある場合は <strong>input1 → input2 → output</strong></li> - <li><strong>=</strong> の左側は関数名と引数、右側に実装</li> + <li>次は Hoare Logic での検証</li> +</ul> + +<!-- TODO +- 伝えたいものをはっきり +- 成果はどこ? +- Hoare Logic の説明で + - 今までの Hoare Logic でできなかったことをできるようになった + - 従来の Hoare Logic は Command ベースでしかかけなかったけど自由に書けるようになった + - Hoare Logic を主眼に + +- hoare logic の検証 + - htproof + - htproof での while program + - 検証 + +- cbc と hoare logic + - cbc での hoare logic 記述 + - cbc での while program + - 内訳(関数の話とか) + - cbc での while program の検証 + - 記述の比較 + - cbc での soundness + +- まとめ +--> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic-での-command-に対応する仕様">Hoare Logic での Command に対応する仕様</h2> +<ul> + <li>Command に対応する証明がある + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> data HTProof : Cond → Comm → Cond → Set where +<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → +<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> (pr : Axiom bPre pcm bPost) → +<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> HTProof bPre (PComm pcm) bPost +<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> SkipRule : (b : Cond) → HTProof b Skip b +<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> AbortRule : (bPre : Cond) → (bPost : Cond) → +<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> HTProof bPre Abort bPost +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> {bPost' : Cond} → {bPost : Cond} → +<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> Tautology bPre bPre' → +<span class="line-numbers"><a href="#n11" name="n11">11</a></span> HTProof bPre' cm bPost' → +<span class="line-numbers"><a href="#n12" name="n12">12</a></span> Tautology bPost' bPost → +<span class="line-numbers"><a href="#n13" name="n13">13</a></span> HTProof bPre cm bPost +<span class="line-numbers"><a href="#n14" name="n14">14</a></span> SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → +<span class="line-numbers"><a href="#n15" name="n15">15</a></span> {cm2 : Comm} → {bPost : Cond} → +<span class="line-numbers"><a href="#n16" name="n16">16</a></span> HTProof bPre cm1 bMid → +<span class="line-numbers"><a href="#n17" name="n17">17</a></span> HTProof bMid cm2 bPost → +<span class="line-numbers"><a href="#n18" name="n18">18</a></span> HTProof bPre (Seq cm1 cm2) bPost +<span class="line-numbers"><a href="#n19" name="n19">19</a></span> IfRule : {cmThen : Comm} → {cmElse : Comm} → +<span class="line-numbers"><strong><a href="#n20" name="n20">20</a></strong></span> {bPre : Cond} → {bPost : Cond} → +<span class="line-numbers"><a href="#n21" name="n21">21</a></span> {b : Cond} → +<span class="line-numbers"><a href="#n22" name="n22">22</a></span> HTProof (bPre and b) cmThen bPost → +<span class="line-numbers"><a href="#n23" name="n23">23</a></span> HTProof (bPre and neg b) cmElse bPost → +<span class="line-numbers"><a href="#n24" name="n24">24</a></span> HTProof bPre (If b cmThen cmElse) bPost +<span class="line-numbers"><a href="#n25" name="n25">25</a></span> WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → +<span class="line-numbers"><a href="#n26" name="n26">26</a></span> HTProof (bInv and b) cm bInv → +<span class="line-numbers"><a href="#n27" name="n27">27</a></span> HTProof bInv (While b cm) (bInv and neg b) +</pre></div> +</div> + </div> + </li> + <li>検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある</li> </ul> @@ -174,25 +444,76 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での証明">Agda での証明</h2> +<h2 id="hoare-logic-での-仕様記述と部分正当性">Hoare Logic での 仕様記述と部分正当性</h2> <ul> - <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong> - <div class="language-HASKELL highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> +zero : { y : Nat } → y + zero ≡ y -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> +zero {zero} = refl -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> +zero {suc y} = cong suc ( +zero {y} ) + <li>HTProof で記述した仕様</li> + <li>lemma は事前条件からコマンドを通して事後条件が成り立つこと(部分正当性)の証明(長いので省略) + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proof1 c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule (init-case {c10} )) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +</pre></div> +</div> + </div> + </li> + <li>比較のために元の while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li><strong>refl</strong> は <strong>x ≡ x</strong></li> - <li><strong>cong</strong> は <strong>関数</strong> と等式を受け取って、等式の両辺に関数を適応しても等しくなること</li> - <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明 + <li>Command と対応した仕様があるため形がほぼ一緒 <ul> - <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li> - <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして帰納的に証明している</li> + <li>while ループするときに強い条件を緩めている規則が違うくらい(Weacening Rule)</li> </ul> </li> + <li>proof1 は HTProof が正しく繋げることで部分正当性まで証明</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoare-logic-での健全性の証明">Hoare Logic での健全性の証明</h2> +<ul> + <li>proof1 は部分正当性を示せた</li> + <li>実際に正しく動作すること(健全性)を証明する必要がある</li> + <li>Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す</li> + <li>PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> HTProof bPre cm bPost -> Satisfies bPre cm bPost +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +</pre></div> +</div> + </div> + </li> + <li>proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofOfProgram : (c10 : ℕ) → (input output : Env ) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → initCond input ≡ true +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> → (SemComm (program c10) input output) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> → termCond {c10} output ≡ true +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> proofOfProgram c10 input output ic sem = +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> PrimSoundness (proof1 c10) input output ic sem +</pre></div> +</div> + </div> + </li> </ul> @@ -201,18 +522,16 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-について">Gears について</h2> +<h2 id="continuation-based-c-について">Continuation based C について</h2> <ul> - <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li> - <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li> + <li>Continuation based C (CbC) は当研究室で開発してるプログラミング言語</li> + <li>CbC では処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong> とする</li> <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li> - <li>Output の DataGear は次の CodeGear の Input として接続される -<!-- [fig1](file://./fig/cgdg.pdf) --></li> + <li>Output の DataGear は次の CodeGear の Input として接続される</li> <li>CodeGear の接続処理などのメタ計算は Meta CodeGear として定義</li> <li>Meta CodeGear で信頼性の検証を行う</li> </ul> <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%" /></p> -<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> --> @@ -220,34 +539,13 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での-datagear">Agda での DataGear</h2> +<h2 id="cbc-での-hoare-logic">CbC での Hoare Logic</h2> <ul> - <li><strong>DataGear</strong> は CodeGear でつかわれる引数をまとめたもの</li> - <li>Agda は CodeGear、 DataGear は検証メタ計算そのものと考えられる</li> - <li>DataGear は Agda の CodeGear で使われる<strong>全てのデータ</strong>に当たる</li> + <li>CodeGear、DataGear を用いた Hoare Logic は図のようになる</li> </ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="agda-での-codegear">Agda での CodeGear</h2> +<p style="text-align:center;"><img src="./fig/hoare-cg-dg.svg" alt="" width="60%" height="60%" /></p> <ul> - <li>Agda での CodeGear は継続渡しで記述された関数 - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest : {t : Set} → (c10 : Nat) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (Code : Env → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest c10 next = next (record {varn = c10 -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ; vari = 0} ) -</pre></div> -</div> - </div> - </li> - <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li> - <li><strong>(Code : fa → t)</strong> は継続先</li> - <li>引数として継続先を受け取って計算結果を渡す</li> + <li>CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる</li> </ul> @@ -256,68 +554,33 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2> +<h2 id="cbc-での-while-program">CbC での while program</h2> <ul> - <li>関数の動作を条件で変えたいときはパターンマッチを行う + <li>比較用の Hoare Logic での while program <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileLoop : {l : Level} {t : Set l} → Envc -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (next : Envc → t) → (exit : Envc → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> </div> </li> - <li>whileLoop は varn が 0 より大きい間ループする</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="hoare-logic-をベースとした-gears-での検証手法">Hoare Logic をベースとした Gears での検証手法</h2> -<div class="language-C highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } + <li>CbC での while program + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCall : (c10 : ℕ ) → Envc +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env)) </pre></div> </div> -</div> -<ul> - <li>今回 Hoare Logic で証明する次のようなコードを検証した</li> - <li>このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす</li> - <li>n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> test : Env -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> -- whileLoop : {t : Set} → Env → (Code : Env → t) → t -</pre></div> -</div> -</div> -<ul> - <li>test は whileTest と whileLoop を実行した結果を返す関数</li> - <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す + </div> + </li> + <li>whileTestP’ が n = c10、 i = 0 の代入、 loopP’ が while loop に対応している</li> + <li>CbC での Hoare Logic 上でコマンドは CodeGear そのもの <ul> - <li><strong>(λ 引数 → )</strong>は無名の関数で引数を受け取って継続する</li> + <li>CodeGear は Hoare Logic のコマンドより自由な記述</li> </ul> </li> </ul> @@ -328,49 +591,46 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-をベースにした-hoare-logic-と証明全体">Gears をベースにした Hoare Logic と証明(全体)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears : {c10 : Nat } → Set -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> (λ n2 → ( vari n2 ≡ c10 )))) +<h2 id="cbc-での-htproof">CbC での HTProof</h2> +<ul> + <li>HTProof に対応するものは各 Meta CodeGear に条件を渡したもの</li> + <li>それぞれが事前条件から事後条件を導く証明を持っている + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTestPwP c10 next = +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl }) </pre></div> </div> -</div> -<ul> - <li>proofGears は Hoare Logic をベースとした証明 - <ul> - <li>先程のプログラムと違い、引数として証明も持っている</li> - </ul> + </div> </li> - <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明whiletest">Gears と Hoare Logic をベースにした証明(whileTest)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest' : {l : Level} {t : Set l} {c10 : ℕ } -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest' {_} {_} {c10} next = next -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) + <li>whileTestPCallwP’ は Hoare Logic の HTProof 記述 proof1 に相当</li> + <li>比較用 proof1 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proof1 c10 = +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule (init-case {c10} )) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) +<span class="line-numbers"><a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 </pre></div> </div> + </div> + </li> + <li>proof1 の lemma に相当する証明は Meta CodeGear で、継続先の CodeGear に渡す条件の証明 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCallwP' : (c : ℕ ) → Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCallwP' c = whileTestPwP {_} {_} c ( +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> λ env s → loopPwP' (varn env) env refl (conv env s) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → vari env ≡ c10 env ) ) +</pre></div> </div> -<ul> - <li>最初の Command なので PreCondition はない</li> - <li>(record {pi1 = refl ; pi2 = refl}) は <strong>(vari env) ≡ 0</strong> と <strong>(varn env) ≡ c10</strong>の証明 - <ul> - <li><strong><em>∧</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li> - <li>両方とも成り立つので <strong>refl</strong></li> - </ul> + </div> </li> - <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong></li> + <li>Hoare Logic では実装、部分正当性を分けて記述していた</li> + <li>CbC での Hoare Logic は実装と部分正当性を一体化できる</li> </ul> @@ -379,111 +639,27 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明conversion">Gears と Hoare Logic をベースにした証明(conversion)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> conv e record { pi1 = refl ; pi2 = refl } = +zero -</pre></div> -</div> -</div> +<h2 id="cbc-での-soundness">CbC での Soundness</h2> <ul> - <li>conv は制約を緩める CodeGear - <ul> - <li><strong>(vari env ≡ 0) ∧ (varn env ≡ c10 env)</strong> が成り立つとき <strong>varn env + vari env ≡ c10 env</strong> が成り立つ</li> - </ul> - </li> -</ul> - -<!-- ## Hoare Logic の証明 --> -<!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している --> -<!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している --> -<!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 --> -<!-- - 変換後の式を次の行に書いて変換を続ける --> -<!-- ```AGDA --> -<!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) --> -<!-- → ((vari env) ≡ 0) /\ ((varn env) ≡ (c10 env)) --> -<!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t --> -<!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero --> -<!-- ``` --> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした証明whileloop">Gears と Hoare Logic をベースにした証明(whileLoop)</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> whileLoopPwP' zero env refl refl next exit = exit env refl -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> whileLoopPwP' (suc n) env refl refl next exit = -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> loopPwP' zero env refl refl exit = exit env refl -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> (λ env x y → loopPwP' n env x y exit) exit + <li>先程の whileTestPCallwP’ を命題として証明すると健全性が示せる + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTestPCallwP' : (c : ℕ ) → Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileTestPCallwP' c = whileTestPwP {_} {_} c ( +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> λ env s → loopPwP' (varn env) env refl (conv env s) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → vari env ≡ c10 env ) ) </pre></div> </div> -</div> -<ul> - <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている</li> - <li>ループが回るごとに、<strong>whileLoopPwP’</strong> で停止か継続かを判断し、 <strong>loopPwP’</strong> でループが回る</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-をベースにした仕様記述">Gears と Hoare Logic をベースにした仕様記述</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileProofs : (c : ℕ ) → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> ( λ env s → conv1 env s -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> ( λ env s → vari env ≡ c10 env ))) + </div> + </li> + <li>実際に値が入ると命題は成り立つが任意の値だと停止せず証明が終わらない + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileCallwP : (c : ℕ) → whileTestPCallwP' c +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileCallwP c = whileTestPwP {_} {_} c (λ env s → +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) </pre></div> </div> -</div> -<ul> - <li><strong>whileProofs</strong> では最終状態が vari と c10 が等しくなるため仕様になっている</li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoare-logic-を用いた仕様の証明">Gears と Hoare Logic を用いた仕様の証明</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>-- ( λ env s → conv1 env s -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>-- ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>-- ( λ env s → vari env ≡ c10 env ))) -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> ProofGears : (c : ℕ) → whileProofs c -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> ProofGears c = whileTestPwP {_} {_} c -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> (λ env₁ s₁ → {!!})) -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> ------------------------------------------------------------ -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> s₁ : vari env₁ ≡ c10 env₁ -<span class="line-numbers"><a href="#n15" name="n15">15</a></span> env₁ : Envc -<span class="line-numbers"><a href="#n16" name="n16">16</a></span> s : (vari env ≡ 0) /\ (varn env ≡ c10 env) -<span class="line-numbers"><a href="#n17" name="n17">17</a></span> env : Envc -<span class="line-numbers"><a href="#n18" name="n18">18</a></span> c : ℕ -</pre></div> -</div> -</div> -<ul> - <li>先程の <strong>whileProofs</strong> で行った仕様記述を型に記述し、実際に証明していく</li> - <li>しかし loopPwP’ のループが進まず証明できない</li> + </div> + </li> </ul> @@ -493,18 +669,21 @@ <div class='slide'> <!-- _S9SLIDE_ --> <h2 id="検証時の-loop-の解決">検証時の Loop の解決</h2> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> loopHelper zero env eq refl rewrite eq = refl -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> loopHelper (suc n) env eq refl rewrite eq = loopHelper n -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) +<ul> + <li><strong>loopHelper</strong> は今回のループを解決する証明 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> → (varn env + vari env ≡ c10 env) +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> loopHelper zero env eq refl rewrite eq = refl +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> loopHelper (suc n) env eq refl rewrite eq = loopHelper n +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> refl (+-suc n (vari env)) </pre></div> </div> -</div> -<ul> - <li><strong>loopHelper</strong> は今回のループを解決する証明</li> - <li>ループ解決のためにループの簡約ができた</li> + </div> + </li> + <li>ここでは任意の回数回る while loop が必ず最終条件を満たす</li> </ul> @@ -515,13 +694,9 @@ <!-- _S9SLIDE_ --> <h2 id="gears-と-hoare-logic-を用いた仕様の証明完成">Gears と Hoare Logic を用いた仕様の証明(完成)</h2> <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> -- whileProofs c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> -- ( λ env s → conv1 env s -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -- ( λ env s → loopPwP' (varn env) env refl s -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> -- ( λ env s → vari env ≡ c10 env ))) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> ProofGears : (c : ℕ) → whileProofs c -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> ProofGears c = whileTestPwP {_} {_} c -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> helperCallwP : (c : ℕ) → whileTestPCallwP' c +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> helperCallwP c = whileTestPwP {_} {_} c +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) </pre></div> </div> </div> @@ -549,6 +724,200 @@ </li> </ul> +<!-- ## Gears について --> +<!-- - **Gears** は当研究室で提案しているプログラム記述手法 --> +<!-- - 処理の単位を **CodeGear** 、データの単位を **DataGear** --> +<!-- - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す --> +<!-- - Output の DataGear は次の CodeGear の Input として接続される --> +<!-- <\!-- [fig1](file://./fig/cgdg.pdf) -\-> --> +<!-- - CodeGear の接続処理などのメタ計算は Meta CodeGear として定義 --> +<!-- - Meta CodeGear で信頼性の検証を行う --> +<!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="60%" height="75%"/></p> --> +<!-- <\!-- <p style="text-align:center;"><img src="./fig/cgdg-small.svg" alt="" width="75%" height="75%"/></p> -\-> --> + +<!-- ## Agda での DataGear --> +<!-- - **DataGear** は CodeGear でつかわれる引数をまとめたもの --> +<!-- - Agda は CbC の上位言語 --> +<!-- - メタ計算を含めて記述できる --> +<!-- - DataGear は Agda の CodeGear で使うことのできる**全てのデータ** --> + +<!-- ## Agda での CodeGear --> +<!-- - Agda での CodeGear は継続渡しで記述された関数 --> +<!-- ```AGDA --> +<!-- whileTest : {t : Set} → (c10 : Nat) --> +<!-- → (Code : Env → t) → t --> +<!-- whileTest c10 next = next (record {varn = c10 --> +<!-- ; vari = 0} ) --> +<!-- ``` --> +<!-- - CodeGear の型は継続先を返す関数 --> +<!-- - **(Code : fa → t)** は継続先 --> +<!-- - 引数として継続先の CodeGear を受け取る --> + +<!-- ## Agda での Gears の記述(whileLoop) --> +<!-- - 関数の動作を条件で変えたいときはパターンマッチを行う --> +<!-- ```AGDA --> +<!-- whileLoop : {l : Level} {t : Set l} → Envc --> +<!-- → (next : Envc → t) → (exit : Envc → t) → t --> +<!-- whileLoop env@(record { c10 = _ ; varn = zero ; vari = _ }) _ exit = exit env --> +<!-- whileLoop record { c10 = _ ; varn = suc varn1 ; vari = vari } next _ = --> +<!-- next (record {c10 = _ ; varn = varn1 ; vari = suc vari }) --> +<!-- ``` --> +<!-- - whileLoop は varn が 0 より大きい間ループする --> + +<!-- ## Hoare Logic をベースとした Gears での検証手法 --> +<!-- ```C --> +<!-- n = 10; --> +<!-- i = 0; --> + +<!-- while (n>0) --> +<!-- { --> +<!-- i++; --> +<!-- n--; --> +<!-- } --> +<!-- ``` --> +<!-- - 今回 Hoare Logic で証明する次のようなコードを検証した --> +<!-- - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす --> +<!-- - n ≡ 0 のとき停止するため、終了時の変数の結果は i ≡ 10、n ≡ 0 になる --> + +<!-- ## Gears をベースにしたプログラム --> +<!-- ```AGDA --> +<!-- test : Env --> +<!-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> + +<!-- -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t --> +<!-- -- whileLoop : {t : Set} → Env → (Code : Env → t) → t --> +<!-- ``` --> +<!-- - test は whileTest と whileLoop を実行した結果を返す関数 --> +<!-- - whileTest の継続先にDataGear を受け取って whileLoop に渡す --> +<!-- - **(λ 引数 → )**は無名の関数で引数を受け取って継続する --> + +<!-- ## Gears をベースにした Hoare Logic と証明(全体) --> +<!-- ```AGDA --> +<!-- -- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1)) --> +<!-- proofGears : {c10 : Nat } → Set --> +<!-- proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → --> +<!-- conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 --> +<!-- (λ n2 → ( vari n2 ≡ c10 )))) --> +<!-- ``` --> +<!-- - proofGears は Hoare Logic をベースとした証明 --> +<!-- - 先程のプログラムと違い、引数として証明も持っている --> +<!-- - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileTest) --> +<!-- ```AGDA --> +<!-- whileTest' : {l : Level} {t : Set l} {c10 : ℕ } --> +<!-- → (Code : (env : Env ) → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t --> +<!-- whileTest' {_} {_} {c10} next = next --> +<!-- (record env {vari = 0 ; varn = c10 }) (record {pi1 = refl ; pi2 = refl}) --> +<!-- ``` --> +<!-- - 最初の Command なので PreCondition はない --> +<!-- - (record {pi1 = refl ; pi2 = refl}) は **(vari env) ≡ 0** と **(varn env) ≡ c10**の証明 --> +<!-- - **_∧_** は pi1 と pi2 のフィールドをもつレコード型 --> +<!-- - 両方とも成り立つので **refl** --> +<!-- - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** --> + +<!-- ## Gears と Hoare Logic をベースにした証明(conversion) --> +<!-- ```AGDA --> +<!-- conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env --> +<!-- conv e record { pi1 = refl ; pi2 = refl } = +zero --> +<!-- ``` --> +<!-- - conv は制約を緩める CodeGear --> +<!-- - **(vari env ≡ 0) ∧ (varn env ≡ c10 env)** が成り立つとき **varn env + vari env ≡ c10 env** が成り立つ --> + +<!-- <\!-- ## Hoare Logic の証明 -\-> --> +<!-- <\!-- - Hoare Logic の証明では基本的に項の書き換えを行って証明している -\-> --> +<!-- <\!-- - proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している -\-> --> +<!-- <\!-- - 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 -\-> --> +<!-- <\!-- - 変換後の式を次の行に書いて変換を続ける -\-> --> +<!-- <\!-- ```AGDA -\-> --> +<!-- <\!-- conv1 : {l : Level} {t : Set l } → (env : Envc ) -\-> --> +<!-- <\!-- → ((vari env) ≡ 0) ∧ ((varn env) ≡ (c10 env)) -\-> --> +<!-- <\!-- → (Code : (env1 : Envc ) → (varn env1 + vari env1 ≡ (c10 env1)) → t) → t -\-> --> +<!-- <\!-- conv1 env record { pi1 = refl ; pi2 = refl } next = next env +zero -\-> --> +<!-- <\!-- ``` -\-> --> + +<!-- ## Gears と Hoare Logic をベースにした証明(whileLoop) --> +<!-- ```AGDA --> +<!-- whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env --> +<!-- → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) --> +<!-- → (exit : (env : Envc ) → whileTestStateP sf env → t) → t --> +<!-- whileLoopPwP' zero env refl refl next exit = exit env refl --> +<!-- whileLoopPwP' (suc n) env refl refl next exit = --> +<!-- next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> + +<!-- loopPwP' zero env refl refl exit = exit env refl --> +<!-- loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl --> +<!-- (λ env x y → loopPwP' n env x y exit) exit --> +<!-- ``` --> +<!-- - whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている --> +<!-- - ループが回るごとに、**whileLoopPwP'** で停止か継続かを判断し、 **loopPwP'** でループが回る --> + +<!-- ## Gears と Hoare Logic をベースにした仕様記述 --> +<!-- ```AGDA --> +<!-- whileProofs : (c : ℕ ) → Set --> +<!-- whileProofs c = whileTestPwP {_} {_} c --> +<!-- ( λ env s → conv1 env s --> +<!-- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ``` --> +<!-- - **whileProofs** では最終状態が vari と c10 が等しくなるため仕様になっている --> + +<!-- ## Gears と Hoare Logic を用いた仕様の証明 --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> + +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl +zero --> +<!-- (λ env₁ s₁ → {!!})) --> + +<!-- Goal: loopPwP' c (record { c10 = c ; varn = c ; vari = 0 }) refl --> +<!-- +zero (λ env₂ s₂ → vari env₂ ≡ c10 env₂) --> +<!-- ------------------------------------------------------------ --> +<!-- s₁ : vari env₁ ≡ c10 env₁ --> +<!-- env₁ : Envc --> +<!-- s : (vari env ≡ 0) ∧ (varn env ≡ c10 env) --> +<!-- env : Envc --> +<!-- c : ℕ --> +<!-- ``` --> +<!-- - 先程の **whileProofs** で行った仕様記述を型に記述し、実際に証明していく --> +<!-- - しかし loopPwP' のループが進まず証明できない --> + +<!-- ## 検証時の Loop の解決 --> +<!-- ```AGDA --> +<!-- loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) --> +<!-- → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) --> +<!-- loopHelper zero env eq refl rewrite eq = refl --> +<!-- loopHelper (suc n) env eq refl rewrite eq = loopHelper n --> +<!-- (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) --> +<!-- ``` --> +<!-- - **loopHelper** は今回のループを解決する証明 --> +<!-- - ループ解決のためにループの簡約ができた --> + +<!-- ## Gears と Hoare Logic を用いた仕様の証明(完成) --> +<!-- ```AGDA --> +<!-- -- whileProofs c = whileTestPwP {_} {_} c --> +<!-- -- ( λ env s → conv1 env s --> +<!-- -- ( λ env s → loopPwP' (varn env) env refl s --> +<!-- -- ( λ env s → vari env ≡ c10 env ))) --> +<!-- ProofGears : (c : ℕ) → whileProofs c --> +<!-- ProofGears c = whileTestPwP {_} {_} c --> +<!-- (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) --> +<!-- ``` --> +<!-- - **loopHelper** を使って簡約することで **whileProofs** の証明を行うことができた --> + +<!-- ## まとめと今後の課題 --> +<!-- - CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した --> +<!-- - Hoare Logic ベースの検証を実際に行うことができた --> +<!-- - 証明時の任意回の有限ループに対する解決を行えた --> +<!-- - 今後の課題 --> +<!-- - BinaryTree の有限ループに対する証明 --> +<!-- - Hoare Logic で検証されたコードの CbC 変換 --> +<!-- - 並列実行での検証 --> + </div>