Mercurial > hg > Papers > 2019 > ryokka-sigss
view ryokka-sigss.mm @ 17:61117df82f51 default tip
fix
author | ryokka |
---|---|
date | Wed, 16 Jan 2019 12:42:49 +0900 |
parents | 17b7605a5deb |
children |
line wrap: on
line source
<map version="1.1.0"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1542710800707" ID="ID_311099003" MODIFIED="1542710817736" TEXT="HoareLogic を用いた CbC の検証"> <node CREATED="1542710937504" ID="ID_569346512" MODIFIED="1547470706865" POSITION="right" TEXT="目次"> <node CREATED="1542710833654" FOLDED="true" ID="ID_422945004" MODIFIED="1547470956607" TEXT="研究目的"> <node CREATED="1542712135796" ID="ID_1556598404" MODIFIED="1542712159908" TEXT="動作するプログラムは高い信頼性を持っていてほしい"/> <node CREATED="1542712161341" ID="ID_1089776093" MODIFIED="1542712318458" TEXT="そのため当研究室では CodeGear, DataGear という単位を用いて記述する手法を提案している"/> <node CREATED="1542712325826" ID="ID_1328437172" MODIFIED="1542713353200" TEXT="処理の単位である CodeGear を継続してプログラミングをする"/> <node CREATED="1542713354500" ID="ID_1839316214" MODIFIED="1544604145156" TEXT="このプログラミングスタイルは、関数型言語の継続渡しの記述と等価である"/> <node CREATED="1544602583680" ID="ID_1768414893" MODIFIED="1544604155058" TEXT="継続渡しの記述と HoareLogic は相性良く記述ができるのではないかと考えている"/> <node CREATED="1544604130156" ID="ID_1466381113" MODIFIED="1544604233204" TEXT="本研究では Agda 上で 継続渡し記述と Hoare Logic を用いて SingleLinkedQueue に対して検証を行った(行いたい)"/> </node> <node CREATED="1542710849360" FOLDED="true" ID="ID_1011962353" MODIFIED="1547470963972" TEXT="研究概要"> <node CREATED="1544604865596" ID="ID_778442777" MODIFIED="1544605176196" TEXT="継続渡し記述をした Agda で、Hoare Logic を組み合わせての証明を行う"/> <node CREATED="1544604886373" ID="ID_742333345" MODIFIED="1544605273294" TEXT="通常は関数ごとの検証が厳しそう"> <node CREATED="1544605273841" ID="ID_1047842205" MODIFIED="1544605304755" TEXT="HoareLogic ベースだとそれぞれの関数ごとに検証ができそう"> <icon BUILTIN="forward"/> </node> </node> </node> <node CREATED="1544605418893" ID="ID_1631394138" MODIFIED="1544605424146" TEXT="GearsOS"> <node CREATED="1544605447524" ID="ID_1203956494" MODIFIED="1544605454361" TEXT="概要"> <node CREATED="1544605455331" ID="ID_1049429958" MODIFIED="1544605459641" TEXT="CbC"/> <node CREATED="1544605471951" ID="ID_1170775991" MODIFIED="1544605484612" TEXT="ぱるすさんの修論あたりから拾ってくる"/> </node> </node> <node CREATED="1542710861598" ID="ID_1569648968" MODIFIED="1547470946011" TEXT="Agda"> <node CREATED="1544603740555" ID="ID_1970865370" MODIFIED="1544603746306" TEXT="Agda について"> <node CREATED="1544604331911" ID="ID_1316542521" MODIFIED="1544604340263" TEXT="Agda とは?"/> <node CREATED="1544604340903" ID="ID_1025874674" MODIFIED="1544604470238" TEXT="Agda のデータ、文法記述"/> </node> <node CREATED="1544603752778" ID="ID_1655285120" MODIFIED="1544604330094" TEXT="検証に関する話"> <node CREATED="1544604295278" ID="ID_1571024257" MODIFIED="1544604451101" TEXT="Curry Howard とか書いたほうがいい?"/> <node CREATED="1544604345175" ID="ID_1245079261" MODIFIED="1544604485703" TEXT="Agda での証明"/> </node> <node CREATED="1542710855615" ID="ID_633104128" MODIFIED="1544605442284" TEXT="GearsOSとAgda"> <node CREATED="1544603433154" ID="ID_1178446548" MODIFIED="1544603443456" TEXT="CbC について"/> <node CREATED="1544603444224" ID="ID_1582475028" MODIFIED="1544603454233" TEXT="CodeGear, DataGear"/> <node CREATED="1544603454927" ID="ID_1017938996" MODIFIED="1544604274110" TEXT="Agda での CodeGear, DataGear(継続渡し記述の説明も)"/> <node CREATED="1544604389725" ID="ID_1200091175" MODIFIED="1544604415749" TEXT="Agda での CbC の検証"/> </node> <node CREATED="1544955510685" ID="ID_1378359833" MODIFIED="1544955531798" TEXT="等式変形の証明"> <node CREATED="1544955536030" ID="ID_1351263237" MODIFIED="1544955550375" TEXT="x==y を証明したい"/> <node CREATED="1544955552292" ID="ID_1396517005" MODIFIED="1544955578075" TEXT="Reasoning を 三つの ? でかく"/> <node CREATED="1544955585146" ID="ID_569206138" MODIFIED="1544955596370" TEXT="二つ目を見ると前後に必要な式がわかる"/> <node CREATED="1544955597250" ID="ID_1715686699" MODIFIED="1544955611283" TEXT="変形する式を羅列する"/> <node CREATED="1544955612652" ID="ID_985696591" MODIFIED="1544955630412" TEXT="変形する推論規則(x==x1)"> <node CREATED="1544955633523" ID="ID_1341233417" MODIFIED="1544955646711" TEXT="x1==y を証明すれば良い"/> </node> </node> </node> <node CREATED="1542710864438" ID="ID_1474492130" MODIFIED="1547470948229" TEXT="HoareLogic"> <node CREATED="1544952943134" ID="ID_10179037" MODIFIED="1544952949971" TEXT="While Program"> <node CREATED="1544952991409" ID="ID_596599032" MODIFIED="1544952997567" TEXT="Skip"/> <node CREATED="1544952998071" ID="ID_1502092759" MODIFIED="1544953002143" TEXT="Abort"/> <node CREATED="1544953002729" ID="ID_652512656" MODIFIED="1544953004935" TEXT="Seq"/> <node CREATED="1544953005280" ID="ID_1999779347" MODIFIED="1544953009167" TEXT="PComm"/> <node CREATED="1544953009656" ID="ID_143829516" MODIFIED="1544953010671" TEXT="If"/> <node CREATED="1544953010967" ID="ID_1707380993" MODIFIED="1544953012496" TEXT="While"/> </node> <node CREATED="1544953033123" ID="ID_1125077236" MODIFIED="1544953048274" TEXT="PreCondition Command PostCondition"> <node CREATED="1544953059289" ID="ID_554375384" MODIFIED="1544953065212" TEXT="HTProof"> <node CREATED="1544953087539" ID="ID_500044924" MODIFIED="1544953091662" TEXT="SkipRule"/> <node CREATED="1544953092210" ID="ID_1398126479" MODIFIED="1544953097342" TEXT="AbortRule"/> <node CREATED="1544953097973" ID="ID_1347734292" MODIFIED="1544953100799" TEXT="SeqRule"/> <node CREATED="1544953101143" ID="ID_810877387" MODIFIED="1544953114392" TEXT="PrimCommRule"/> <node CREATED="1544953115159" ID="ID_1693437242" MODIFIED="1544953119888" TEXT="IfRule"/> <node CREATED="1544953120428" ID="ID_403099872" MODIFIED="1544953122745" TEXT="WhileRule"/> <node CREATED="1544953131201" ID="ID_1694881778" MODIFIED="1544953193197" TEXT="WeakningRule"/> </node> <node CREATED="1544953067155" ID="ID_991425650" MODIFIED="1544953077405" TEXT="Axiom "/> <node CREATED="1544953078010" ID="ID_1967448460" MODIFIED="1544953082901" TEXT="Totology"/> </node> <node CREATED="1544953213492" ID="ID_1313761757" MODIFIED="1544953220280" TEXT="Example"/> <node CREATED="1544954625664" ID="ID_856350466" MODIFIED="1544954638560" TEXT="証明の手順"> <node CREATED="1544954639048" ID="ID_707405060" MODIFIED="1544954655114" TEXT="Programに沿ってルールを構築する"/> <node CREATED="1544954656137" ID="ID_1099647645" MODIFIED="1544954693892" TEXT="While Program に相似なProgram の構築方法になる"/> <node CREATED="1544954695449" ID="ID_167702231" MODIFIED="1544954726159" TEXT="ルールの Axiom 部分を ? とすると証明すべき論理式が得られる"/> <node CREATED="1544954728375" ID="ID_733013199" MODIFIED="1544954791492" TEXT="証明をラムダこうとして構築する"/> <node CREATED="1544954794025" ID="ID_1862482735" MODIFIED="1544954833648" TEXT="Invaliant のように PostCondition と PreCondition が合わない場合は"> <node CREATED="1544954837647" ID="ID_605650861" MODIFIED="1544954853144" TEXT="WeakningRuleを使う"/> </node> <node CREATED="1544954861191" ID="ID_1632760763" MODIFIED="1544954884779" TEXT="すべてが接続されると証明が終わる"/> <node CREATED="1544954887674" ID="ID_49477826" MODIFIED="1544954897316" TEXT="停止性はここではまだ証明していない"> <node CREATED="1544954900504" ID="ID_333078697" MODIFIED="1544954920046" TEXT="Agda では TERMINATING というアノテーションで抑制する"/> </node> </node> <node CREATED="1544603916933" ID="ID_912615419" MODIFIED="1544953262787" TEXT="CodeGear, DataGear"> <node CREATED="1544953301023" ID="ID_1936819038" MODIFIED="1544953341105" TEXT="add PreCondition to CodeGear Argument"/> <node CREATED="1544953364369" ID="ID_1897331085" MODIFIED="1544953383252" TEXT="use Conversion CodeGear as a WeakningRule"/> </node> <node CREATED="1544953390779" ID="ID_1221989718" MODIFIED="1544953393861" TEXT="Example"/> </node> <node CREATED="1544953534749" ID="ID_757078127" MODIFIED="1544953544019" TEXT="比較と評価"> <node CREATED="1544953548644" ID="ID_660804708" MODIFIED="1544953586327" TEXT="HoareLogic は Program の構造と証明が別"/> <node CREATED="1544953593558" ID="ID_1222836750" MODIFIED="1544953605696" TEXT="停止性はまだ未実装"/> <node CREATED="1544953607664" ID="ID_1418415681" MODIFIED="1544953624184" TEXT="CodeGear"> <node CREATED="1544953624446" ID="ID_1333500913" MODIFIED="1544953647627" TEXT="Program と証明が対応してる"/> <node CREATED="1544953649212" ID="ID_1043705676" MODIFIED="1544953685286" TEXT="while Program と違ってCodeGearの記述が自由"/> <node CREATED="1544953687507" ID="ID_213969675" MODIFIED="1544953714064" TEXT="証明がメタ計算の入力と出力に対応する"/> <node CREATED="1544953717022" ID="ID_960276791" MODIFIED="1544953734255" TEXT="入力がPreCondition で"/> <node CREATED="1544953736673" ID="ID_13390002" MODIFIED="1544953757401" TEXT="継続の呼び出しが PostCondition になる"/> </node> <node CREATED="1544953777092" ID="ID_1972622252" MODIFIED="1544953797711" TEXT="CodeGearでHoareLogic を簡潔に記述できることがわかった"/> </node> <node CREATED="1544953399717" ID="ID_1659003334" MODIFIED="1544953407985" TEXT="将来の課題"> <node CREATED="1544953411825" ID="ID_1766627105" MODIFIED="1544953435986" TEXT="HoareLogic 部分をメタ計算として記述"/> <node CREATED="1544953456250" ID="ID_37105044" MODIFIED="1544953464613" TEXT="元の計算の記述を保存する"/> <node CREATED="1544953465598" ID="ID_454238122" MODIFIED="1544953488516" TEXT="RedBlackTree"/> <node CREATED="1544953489813" ID="ID_286112576" MODIFIED="1544953506149" TEXT="Synchronized Queue"> <node CREATED="1544953803400" ID="ID_1363325581" MODIFIED="1544953823216" TEXT="並列プログラムを状態遷移に変換する"/> <node CREATED="1544953824288" ID="ID_649570454" MODIFIED="1544953862724" TEXT="Temporal Logic なプロパティを状態遷移として記述する"/> <node CREATED="1544953864581" ID="ID_1141579119" MODIFIED="1544953928385" TEXT="Omega Automaton の受理条件として証明する"/> </node> <node CREATED="1544953525955" ID="ID_796699968" MODIFIED="1544953529433" TEXT="GearsOS"/> </node> <node CREATED="1544952979891" ID="ID_1616071429" MODIFIED="1544952986481" TEXT="まとめ"/> </node> <node CREATED="1542710960435" ID="ID_167048397" MODIFIED="1542710984521" POSITION="right" TEXT="研究"/> <node CREATED="1545030891993" ID="ID_424599902" MODIFIED="1545030897348" POSITION="left" TEXT="研究目的"> <node CREATED="1545031695286" ID="ID_1807380852" MODIFIED="1545031828376" TEXT="OS やアプリケーションの信頼性をあげたい"/> <node CREATED="1545031829304" ID="ID_848338957" MODIFIED="1545031877618" TEXT="プログラム自体のバグがないことが重要"/> <node CREATED="1545031881555" ID="ID_1890176001" MODIFIED="1545031901586" TEXT="大半のバグは簡単なものである"/> <node CREATED="1545031915332" ID="ID_1766422576" MODIFIED="1545031926012" TEXT="本来なら当たり前に見つかるエラーを簡単に見つけたい"/> <node CREATED="1545031934733" ID="ID_819406039" MODIFIED="1545031952333" TEXT="プログラムの証明には HoareLogic が存在する"/> <node CREATED="1545031953430" ID="ID_189897321" MODIFIED="1545031992503" TEXT="プログラミングの方法論自体に HoareLogic を組み込むアプローチ"/> <node CREATED="1545031995576" ID="ID_455588060" MODIFIED="1545032022728" TEXT="そのためには既存のプログラミング言語ではダメなのかもしれない"/> <node CREATED="1545032024743" ID="ID_862300550" MODIFIED="1545032052066" TEXT="HoareLogic が広まらない理由"> <node CREATED="1545032068115" ID="ID_1062003354" MODIFIED="1545032100996" TEXT="既存の言語には HoareLogic を書く場所がない"/> <node CREATED="1545032104901" ID="ID_298160802" MODIFIED="1545032113668" TEXT="不当に難しいと思われている"> <node CREATED="1545032129477" ID="ID_952723861" MODIFIED="1545032134998" TEXT="格調高い"/> </node> </node> <node CREATED="1545032140487" ID="ID_1131641415" MODIFIED="1545032158255" TEXT="簡単なエラーを見つけるための証明が難しいはずはない"/> <node CREATED="1545032159792" ID="ID_1116096354" MODIFIED="1545032164071" TEXT="簡単なものから始める"/> <node CREATED="1545032299337" ID="ID_1249663292" MODIFIED="1545032321657" TEXT="Gears は HoareLogic との相性が良いように設計されたプログラミング言語になっている"/> <node CREATED="1545032436351" ID="ID_1535666009" MODIFIED="1545032467432" TEXT="WhileProgram と同じ形で Gears で証明ができる"/> </node> <node CREATED="1545030901019" ID="ID_901428450" MODIFIED="1545030905483" POSITION="left" TEXT="論文の流れ"> <node CREATED="1545031348434" ID="ID_685170876" MODIFIED="1545031357009" TEXT="現状"> <node CREATED="1545031359867" ID="ID_1180031106" MODIFIED="1545031386298" TEXT="kernel の検証例"> <node CREATED="1545031393090" ID="ID_410307657" MODIFIED="1545031412419" TEXT="Cによる実装と関数型言語の記述と証明を行う"/> </node> <node CREATED="1545031418116" ID="ID_536836987" MODIFIED="1545031432052" TEXT="低レベル記述向けの関数型言語"> <node CREATED="1545031433208" ID="ID_1290789880" MODIFIED="1545031441435" TEXT="ATS"/> <node CREATED="1545031442323" ID="ID_894719933" MODIFIED="1545031444003" TEXT="Rust"/> <node CREATED="1545031555795" ID="ID_813031602" MODIFIED="1545031611781" TEXT="証明を行うだけの型システムは持ってない"/> </node> <node CREATED="1545031472093" ID="ID_942826330" MODIFIED="1545031482407" TEXT="証明支援向けのプログラミング言語"> <node CREATED="1545031484349" ID="ID_24675818" MODIFIED="1545031491533" TEXT="Agda"/> <node CREATED="1545031492670" ID="ID_54745078" MODIFIED="1545031494677" TEXT="Coq"/> <node CREATED="1545031496988" ID="ID_1790735065" MODIFIED="1545031505366" TEXT="Issabella"/> <node CREATED="1545031511911" ID="ID_1140265385" MODIFIED="1545031517464" TEXT="実行には向かない"/> </node> <node CREATED="1545031663383" ID="ID_1834440802" MODIFIED="1545031679864" TEXT="証明の記述とプログラムの記述が別々なのが問題ではないか"/> </node> <node CREATED="1545031099382" ID="ID_1202631621" MODIFIED="1547296915498" TEXT="Agda の概要"> <node CREATED="1545031122593" ID="ID_1888101637" MODIFIED="1545031128590" TEXT="等式変形"/> <node CREATED="1545031131170" ID="ID_759945081" MODIFIED="1545031133318" TEXT="?"/> </node> <node CREATED="1545031223230" ID="ID_1271382711" MODIFIED="1545031233635" TEXT="Gears の概要"> <node CREATED="1545031240448" ID="ID_1246355278" MODIFIED="1545031248659" TEXT="CbC の実装"/> <node CREATED="1545031249811" ID="ID_1433130177" MODIFIED="1545031258084" TEXT="Agda による Gears の記述"/> </node> <node CREATED="1545031141237" ID="ID_906133157" MODIFIED="1545031146348" TEXT="While Progarm"/> <node CREATED="1545031153481" ID="ID_434127663" MODIFIED="1545031168863" TEXT="WhileProgram の Agda による証明"/> <node CREATED="1545031170853" ID="ID_1197992113" MODIFIED="1545031185689" TEXT="Gears による例題"/> <node CREATED="1545031186560" ID="ID_1521714484" MODIFIED="1545031200105" TEXT="Gears における HoareLogic の証明"/> </node> <node CREATED="1545030910084" ID="ID_372949892" MODIFIED="1545030913012" POSITION="left" TEXT="結果"> <node CREATED="1545030966535" ID="ID_1338356672" MODIFIED="1545030996904" TEXT="Agda で WhileProgram の HoareLogic による証明を作った"/> <node CREATED="1545030999516" ID="ID_35075799" MODIFIED="1545031016585" TEXT="Gears での HoareLogic の記述をした"/> <node CREATED="1545031027240" ID="ID_981326333" MODIFIED="1545031044786" TEXT="証明とプログラムの記述を一体化して記述できた"/> <node CREATED="1545031065628" ID="ID_457628232" MODIFIED="1545031085235" TEXT="証明をメタ計算の引数の受け渡しとして記述できた"/> </node> <node CREATED="1547296659423" ID="ID_1905231255" MODIFIED="1547296666872" POSITION="right" TEXT="Slide"> <node CREATED="1547296673449" ID="ID_326097753" MODIFIED="1547296725921" TEXT="研究目的"> <node CREATED="1547386601688" ID="ID_658328866" MODIFIED="1547386671077" TEXT="OS とか アプリケーションの信頼性が高いことは重要である"/> <node CREATED="1547386619947" ID="ID_464524492" MODIFIED="1547386747105" TEXT="検証をすることで動作を保証する→信頼性up"/> <node CREATED="1547386632438" ID="ID_230254962" MODIFIED="1547387120710" TEXT="検証の手法として HoareLogic がある"> <node CREATED="1547386919569" ID="ID_272380556" MODIFIED="1547387106641" TEXT="プログラム"/> </node> <node CREATED="1547387112461" ID="ID_1701764044" MODIFIED="1547387260803" TEXT="この方法は実際のプログラミング言語で使用できずあまりひろまっていない"/> <node CREATED="1547387263080" ID="ID_721622245" MODIFIED="1547387313432" TEXT="当研究室では信頼性の高い OS として Gears OS を開発している"/> </node> <node CREATED="1547296864709" ID="ID_450376854" MODIFIED="1547296873020" TEXT="Gears, GearsOS"> <node CREATED="1547297456269" ID="ID_1531966210" MODIFIED="1547297464129" TEXT="Gears って?"> <node CREATED="1547297464134" ID="ID_870199224" MODIFIED="1547298069746" TEXT="当研究室で提案しているodeGear、 DataGear という単位"/> <node CREATED="1547297503002" ID="ID_1634638250" MODIFIED="1547297649262" TEXT="処理の単位をGodeGear、 Dataの単位を DataGear とする"/> <node CREATED="1547297543828" ID="ID_833081910" MODIFIED="1547297650102" TEXT="CodeGear を継続してプログラミングをする"/> <node CREATED="1547297490386" ID="ID_901165581" MODIFIED="1547297720096" TEXT="継続は通常の言語の関数呼び出しとは異なり、現在の環境を破棄して次の CodeGear に遷移する"/> </node> <node CREATED="1547297561929" ID="ID_271914428" MODIFIED="1547298108614" TEXT="GearsOS って?"> <icon BUILTIN="button_cancel"/> <node CREATED="1547297725953" ID="ID_1462232623" MODIFIED="1547297756465" TEXT="先述の Gears という単位を用いて記述されているOS"/> <node CREATED="1547297762474" ID="ID_466083659" MODIFIED="1547298056338" TEXT="信頼性の保証や拡張性をメタレベルの計算で実現することを目標に開発している"/> </node> </node> <node CREATED="1547296726482" ID="ID_1016327903" MODIFIED="1547296883972" TEXT="Gears と Agda"> <node CREATED="1547297445639" ID="ID_38829678" MODIFIED="1547297451879" TEXT="Agda"> <node CREATED="1547298122147" ID="ID_285257604" MODIFIED="1547298126197" TEXT="Agdaって?"/> <node CREATED="1547298126865" ID="ID_741550943" MODIFIED="1547298133660" TEXT="どうやって書くものなの?"/> <node CREATED="1547298224210" ID="ID_152235889" MODIFIED="1547298229439" TEXT="証明とか"> <node CREATED="1547298191391" ID="ID_1481861598" MODIFIED="1547298305152" TEXT="証明の記述"/> <node CREATED="1547298305512" ID="ID_884856006" MODIFIED="1547298310985" TEXT="証明の仕方"/> <node CREATED="1547298311733" ID="ID_790203150" MODIFIED="1547298328602" TEXT="Reasoning の話"/> </node> </node> <node CREATED="1547298136301" ID="ID_1183092589" MODIFIED="1547298142540" TEXT="Agda での Gears"> <node CREATED="1547298143717" ID="ID_1947013376" MODIFIED="1547298211447" TEXT="CodeGear と DataGear の記述と対応"/> <node CREATED="1547298183847" ID="ID_1681965835" MODIFIED="1547298261833" TEXT="CodeGear の証明"/> </node> </node> <node CREATED="1547296742331" ID="ID_124842298" MODIFIED="1547296853787" TEXT="HoareLogic の説明 (in Agda)"> <node CREATED="1547297092738" ID="ID_547653717" MODIFIED="1547297100873" TEXT="HoareLogic の説明"/> <node CREATED="1547297101467" ID="ID_235129828" MODIFIED="1547297115138" TEXT="Rule の説明 "/> <node CREATED="1547297115986" ID="ID_1696132933" MODIFIED="1547297139673" TEXT="whileProgram の記述"/> <node CREATED="1547297126514" ID="ID_1872423698" MODIFIED="1547297156539" TEXT="while Program の証明"/> </node> <node CREATED="1547296780283" ID="ID_1963825092" MODIFIED="1547296789538" TEXT="HoareLogic In Gears"> <node CREATED="1547297084673" ID="ID_47827525" MODIFIED="1547297091497" TEXT="実際のコードとその解説"/> <node CREATED="1547297164153" ID="ID_1844898485" MODIFIED="1547297167275" TEXT="注意点"> <node CREATED="1547297189164" ID="ID_970220773" MODIFIED="1547297329588" TEXT="Soundness は示せてない"/> <node CREATED="1547297206686" ID="ID_1390974283" MODIFIED="1547297314325" TEXT="今の所一部が Non Terminating"/> </node> </node> <node CREATED="1547296790524" ID="ID_1720795334" MODIFIED="1547297178026" TEXT="まとめと今後の課題"> <node CREATED="1547297179867" ID="ID_343559749" MODIFIED="1547297183307" TEXT="まとめ"> <node CREATED="1547296933503" ID="ID_189642434" MODIFIED="1547297408470" TEXT="Agda での HoareLogic の理解ができた"/> <node CREATED="1547296974847" ID="ID_935894346" MODIFIED="1547296994575" TEXT="Gears での HoareLogic 記述"> <node CREATED="1547297003296" ID="ID_569435776" MODIFIED="1547297033782" TEXT="証明とプログラムを一体化して記述できた"/> <node CREATED="1547297035048" ID="ID_1106850001" MODIFIED="1547297078809" TEXT="証明がメタ計算上の引数の受け渡しとして記述できた"/> </node> </node> <node CREATED="1547297186356" ID="ID_1244354785" MODIFIED="1547297188859" TEXT="今後の課題"> <node CREATED="1547297226858" ID="ID_168576221" MODIFIED="1547297371886" TEXT="既存の証明を置き換えられるか?"/> <node CREATED="1547297372437" ID="ID_1413976043" MODIFIED="1547297382902" TEXT="既存の証明より簡易な記述ができるか?"/> </node> </node> </node> </node> </map>