Mercurial > hg > Document > Growi
changeset 129:4bbd08ccb3c2
backup 2023-06-20
| author | autobackup |
|---|---|
| date | Tue, 20 Jun 2023 00:10:03 +0900 |
| parents | 8dfc12dd7740 |
| children | 67fd5b8413b0 |
| files | user/Moririn/メモ/2023/04/24.md |
| diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/user/Moririn/メモ/2023/04/24.md Tue Jun 13 00:10:03 2023 +0900 +++ b/user/Moririn/メモ/2023/04/24.md Tue Jun 20 00:10:03 2023 +0900 @@ -14,10 +14,10 @@ OSの信頼性は高ければ高いほど良い -- 当研究室ではGearsOSというOSを開発している。 GearsOSの信頼性を高めたい。 -このGearsOSにRedBlackTreeの概念を使用したい。 +このGearsOSにRedBlackTreeを使用したい。 RedBlackTreeが正しくGearsOS上で動作するかを検証する必要がある。 この検証手法としてAgdaを使用する。 GearsOSとは、CbCという言語で書かれている。 -Cbcの概念を取り入れたGearsAgdaでRedBlackTreeを実装していく +Cbcを取り入れたGearsAgdaでRedBlackTreeを実装していく RedBlackTreeとは、２分木の一種で、赤と黒の色の概念がある。どのノードを見ても黒色の深さが一定である。木が崩れた場合はバランスするという特徴がある。 BinaryTreeはできているので、これを利用してRedBlackTreeを書いていく。