Mercurial > hg > Papers > 2019 > menikon-midterm
changeset 19:1f50f5b5e33c
fix
| author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 23 Oct 2019 16:41:20 +0900 |
| parents | 26c4f49f1dcd |
| children | bfc913ee4393 |
| files | midterm.pdf midterm.tex |
| diffstat | 2 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/midterm.tex Wed Oct 23 16:34:03 2019 +0900 +++ b/midterm.tex Wed Oct 23 16:41:20 2019 +0900 @@ -73,7 +73,7 @@ %形式手法 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる． %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. -CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応している. +CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.そのため,CbCのInterfaceを使うとモジュール化ができる. これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す.