Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/introduction.tex @ 126:18f872806bc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update reference
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 16 Feb 2017 13:39:49 +0900
parents ebe838b83ada
children
comparison
equal deleted inserted replaced
125:c1cc5407cefe 126:18f872806bc0
22 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。 22 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
23 検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。 23 検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。
24 24
25 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。 25 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
26 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。 26 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
27 CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。 27 CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha~\cite{atton-ipsjpro} を用いて仕様を検査する。
28 また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。 28 また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。
29 Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。 29 Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。
30 そして、Agda 上で Single Linked Stack の性質の証明を行なう。 30 そして、Agda 上で Single Linked Stack の性質の証明を行なう。
31 31
32 32