Mercurial > hg > Papers > 2024 > matac-master
changeset 81:4052b8572f02
...
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 15 Feb 2024 14:17:08 +0900 |
parents | e81688943a04 |
children | be0e9a8ba0d3 |
files | marp-slide/slide.md |
diffstat | 1 files changed, 8 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/marp-slide/slide.md Thu Feb 15 12:28:59 2024 +0900 +++ b/marp-slide/slide.md Thu Feb 15 14:17:08 2024 +0900 @@ -107,7 +107,7 @@ - CodeGearの引数とContextにプログラムの状態が全部入っている - 通常のプログラムでは関数呼び出しのStackやループの状況が隠されている - CodeGear単位の切り替え点でモデル検査や証明が行える -- 状態の明示化は証明を行う際には必ず行う必要がある +- 証明の際に状態の明示化が必要である --- @@ -116,7 +116,7 @@ - 既存のプログラムをそのままCodeGearに書き換えることは可能 - しかし、CodeGear、DataGearともに複雑になる - なぜかというと、既存のプログラムは人間向けの読みやすさが優先だから -- 重要なのは信頼性なので、モデル検査のしやすさ兼証明のしやすさを優先する +- 重要なのは信頼性なので、**モデル検査のしやすさ**兼**証明のしやすさ**を優先する - 基本的なデータ構造を証明優先に書き換える必要がある - これらは既存のプログラムと異なるプログラミングスタイルになる @@ -173,7 +173,9 @@ --- -## メモリ管理や多重性の機能がない +## GearsFilesystemでの信頼性に関する課題 + +メモリ管理や多重性の機能がない <!-- それぞれが何のためにあるのか説明する感じでやると良い --> @@ -332,6 +334,8 @@ ## 評価 +<!-- こういう課題だったけどどうだったよという喋りで --> + - 非破壊RedBlackTreeの増大抑制できる - コピーで木の持続性を確保できる @@ -342,7 +346,7 @@ - Stackも非破壊であるという問題がある - 証明しやすさを優先しているから - 非破壊である意味があまりない -- コピーの正しさ +<!-- - コピーの正しさ --> ---