# HG changeset patch # User matac42 # Date 1707974228 -32400 # Node ID 4052b8572f02eed90eecd25edc9cdaf78be023af # Parent e81688943a04f1d0eb6df333f7f3b69d3c3e4296 ... diff -r e81688943a04 -r 4052b8572f02 marp-slide/slide.md --- 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も非破壊であるという問題がある - 証明しやすさを優先しているから - 非破壊である意味があまりない -- コピーの正しさ + ---