From d9690a03ac14baa0f9c4dc72144438a61f905a78 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 15 Aug 2024 20:35:23 +0200 Subject: Update TODO --- TODO | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/TODO b/TODO index b4916df..b3fe842 100644 --- a/TODO +++ b/TODO @@ -13,6 +13,7 @@ This is a rough outline of upcoming tasks: [x] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root. - Done by showing that the new tree contains all elements except the root, and the updated value. [x] Prove that heapPop leaves all values in the tree, except the root. + - Current proof is not rigorous. Needs more work in the future. [x] Prove that heapPop returns the root [ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index [ ] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index. @@ -21,4 +22,7 @@ This is a rough outline of upcoming tasks: [ ] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index. +Stuff below is not scheduled to happen any time soon. +[ ] Make proofs that currently aren't rigorous rigorous. + - For instance by using element counts instead of just contains. [ ] Write the performance part of this file. \ No newline at end of file -- cgit v1.2.3