Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/introduction.tex @ 77:50c2d2f1a186

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update chapter akasha
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 14:27:06 +0900
parents 623c90a21227
children 3f63f697ed3a
comparison
equal deleted inserted replaced
76:a9ed6a6dc1f2 77:50c2d2f1a186
7 ソフトウェアの検証手法にはモデル検査と定理証明がある。 7 ソフトウェアの検証手法にはモデル検査と定理証明がある。
8 8
9 モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。 9 モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。
10 モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。 10 モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
11 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。 11 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
12 定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。 12 定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
13 13
14 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。 14 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
15 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。 15 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
16 検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。 16 検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードは検証のコードとは別の言語であったり、既存の実装に対する検証は行なえないなどの問題がある。
17 そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。 17 そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。
18 18
19 Continuation based C (CbC)はC言語と似た構文を持つ言語である。 19 Continuation based C (CbC)はC言語と似た構文を持つ言語である。
20 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。 20 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
21 CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。 21 CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。
22 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。 22 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
23 検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更することなくソフトウェアの検証を行なうことができる。 23 検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。
24 24
25 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。 25 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
26 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。 26 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
27 また、証明的な検証として CbC における型システムを部分型として定義する。 27 CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。
28 部分型を利用して CbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。 28 また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
29 Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
29 30
30 31
31 \section{本論文の構成} 32 \section{本論文の構成}
33 % TODO: もう一回構成しなおし
32 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 34 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
33 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。 35 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
34 次に第\ref{chapter:type}章で型システムについて取り上げる。 36 次に第\ref{chapter:type}章で型システムについて取り上げる。
35 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。 37 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。
36 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 38 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。