title: メタ計算を用いた Continuation based C の検証手法
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* 動作するプログラムの信頼性を保証したい
* そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* 処理の単位であるコードセグメントはメタ計算によって相互に接続される
* メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する

# 研究内容
* コードを検証用に変更することなく、仕様を満たすか検証する
* 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる
* モデル検査はコードセグメントの接続部分を変更することで実現する
* 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する
* Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する

# 近況報告
* 部分型を使って定義した CS/DS のコードで n回 push して n回 pop すると戻る証明が書けました
* AMS-Tex は amsmath を使えば良さそうです
* 修論の目次を書きました
* グローバル公開しているサーバが攻撃を受けたようです
    * pukiwiki への攻撃。再監査などの動きもあると思います。

# n-push/n-pop
* 『任意のスタックに対して同じ回数だけ push して pop すると元に戻る』
    * 定義できましたが、前提がいくつかあります
    * たぶんこの前提を得られることの方に意味があると思っています
* push する要素を指定せずに push/pop すると一回popされてしまう
    * 今のコードは要素を指定しないと push しない
    * 実装依存のコードを証明できたので割と良い結果だと思っています
* continuation の処理内容によっては context は変更される
    * ので refl にならない『時もある』

# 修論の目次
* [Mercurial/hg/Papers/2017/atton-master ](http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2017/atton-master/)
* チェックお願いします

# AMS-TeX
* [amstex](https://www.ctan.org/pkg/amstex)
    * American Mathematical Society plain TeX macros
* 今は [AMS-LaTeX](https://www.ctan.org/pkg/amslatex) があるようです
    * 具体的には amsmath package
    * MacTeX 20161009 でも利用可能

<!-- vim: set filetype=markdown.slide: -->