Mercurial > hg > Papers > 2021 > soto-prosym
view slide/note.md @ 12:62e56d73f104
WIP カンペを追加 14ページまで
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 07 Jan 2022 00:58:07 +0900 |
parents | |
children | 76c3378c61dc |
line wrap: on
line source
<!--カンペだよ--> # タイトル Gears Agdaにおける Left Learning Red Black Tree の検証について 琉球大学 並列信頼研究室の上地が発表します # 目的 そのまま読む # CbC もそのまま読む # Agda もそのまま読む # Agda の基本 Agda の基本となる型の1つである Data 型について説明します record Env とあるところで Env という Record 型を定義 することを示しています そしてその中にvarnとvariがあり、その型が自然数であることを定義しています 次に、記述する際の導入が以下のようになり varxに0を、variに1を定義しています 導入後は変数 スペース record名でその中身にアクセスできます # Gears Agda の記法 何と対応しているからLoopで記述するんだっけ Agdaの構文的に禁止していないので再帰呼び出しは使用しないよう注意が必要です 以下がwhile loopのノーマルレベルでの記述になります まず型の方で Envを受け取り、Codeを受け取り、 tを返すといった流れになっています このCodeはEnvを受け取った後にtを返すというものです 次に、入力を env next で受け取っています このcodeは後で再び説明するので、withの方はおいておいてください パターンマッチの方で、false trueの場合をかんがえています これはfalseの場合はnextにenvを渡します nextはenvを受け取ってtを返すので正しいです これがtを返すことでこの後も関数が続くこと、継続を示します # Gears Agdaと Gears CbCの対応 そのまま読むでよさそう Contextだけ調べた方がよいかも # Normal levelと~ 今回検証に使用するHoare Conditionと証明も Meta levelです 画像はよなおせ # Hoare logic プログラム が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当(correct)であるという 簡単な例としてGears Agdaにてwhile loopを検証します 以下のコードを詳細に説明します 入力と出力に関しては前述しました このたーみねーてぃんぐはこの関数が停止することを示しています この実装ではagdaはloopが終了するのかわからず、コンパイルできないので このあのてーとをつけて停止することを明示します with文は引数であたえられた値を展開します。 今回はその値をパターンマッチしています。 これがless than で0とvarnを比較しています このwhileloopは、 varnがこれからループする回数で、variがループした回数になります なので、これが0になると終了し次の関数であるnextに遷移し 0でないならループする回数varxから今回分の1引いて variには今回分の1を足したものをEnvとしてもう一度関数を実行するという記述になっています # post condition 先ほど実装したノーマルレベルなwhile loopに対して 事前条件となるPre / Post Condition を追加した実装をします そのまえにterminatingが付いていると停止性の証明をしたことにはならないので~ このconditionはループしたい回数は これからループする回数とループした回数の和と等しいというものです exitのPostConditionもつけるべきだな… # loopの接続 loopが前のページのWhile LoopSeg だな loopの部分の証明のみだな # 実際のloopの接続 最終的にはループした回数が入力のループしたい回数と一致していることを 証明したいので以下のようになります で、前回のものは最初から構造体(record)に値が格納されている状態から始まっていたので proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている そしてそれを行っているのが最初の関数であるwhileTest'で ここでvarnが入力c10と一致し、variが0であることを証明している 次の関数であるversionでは、whileTest'のrecord定義時のConditionから loop時のconditionを生成しています # testとの違い そのまま読むよ Condition