Vague postconditions and proving correctness of algorithms
Introduction
diff --git a/algorithms/category/algorithms-and-correctness/index.html b/algorithms/category/algorithms-and-correctness/index.html index f4121da..ba4cecf 100644 --- a/algorithms/category/algorithms-and-correctness/index.html +++ b/algorithms/category/algorithms-and-correctness/index.html @@ -2,7 +2,7 @@ - +Algorithms and Correctness
Materials related to basic ideas behind algorithms and proofs of their diff --git a/algorithms/category/asymptotic-notation-and-time-complexity/index.html b/algorithms/category/asymptotic-notation-and-time-complexity/index.html index 0719d32..4f050f4 100644 --- a/algorithms/category/asymptotic-notation-and-time-complexity/index.html +++ b/algorithms/category/asymptotic-notation-and-time-complexity/index.html @@ -2,7 +2,7 @@
- +Asymptotic Notation and Time Complexity
Materials related to asymptotic notation and time complexity. diff --git a/algorithms/category/graphs/index.html b/algorithms/category/graphs/index.html index e88389c..e76d81b 100644 --- a/algorithms/category/graphs/index.html +++ b/algorithms/category/graphs/index.html @@ -2,7 +2,7 @@
- +Graphs
Materials related to basic graph algorithms and graph problems. diff --git a/algorithms/category/hash-tables/index.html b/algorithms/category/hash-tables/index.html index 0d9b51c..09de777 100644 --- a/algorithms/category/hash-tables/index.html +++ b/algorithms/category/hash-tables/index.html @@ -2,7 +2,7 @@
- +Hash Tables
Materials related to hash tables. diff --git a/algorithms/category/paths-in-graphs/index.html b/algorithms/category/paths-in-graphs/index.html index 6b72df4..ac0d488 100644 --- a/algorithms/category/paths-in-graphs/index.html +++ b/algorithms/category/paths-in-graphs/index.html @@ -2,7 +2,7 @@
- +Paths in Graphs
Materials related to finding paths in graphs. diff --git a/algorithms/category/recursion/index.html b/algorithms/category/recursion/index.html index 52d0958..5ecbe0a 100644 --- a/algorithms/category/recursion/index.html +++ b/algorithms/category/recursion/index.html @@ -2,7 +2,7 @@
- +Recursion
Materials related to recursive algorithms and their time complexity. diff --git a/algorithms/category/red-black-trees/index.html b/algorithms/category/red-black-trees/index.html index 6eb02c9..479b1c1 100644 --- a/algorithms/category/red-black-trees/index.html +++ b/algorithms/category/red-black-trees/index.html @@ -2,7 +2,7 @@
- +Red-Black Trees
Materials related to red-black trees. diff --git a/algorithms/graphs/bfs-tree/index.html b/algorithms/graphs/bfs-tree/index.html index 29dc08b..5bdb394 100644 --- a/algorithms/graphs/bfs-tree/index.html +++ b/algorithms/graphs/bfs-tree/index.html @@ -2,7 +2,7 @@
- +Distance boundaries from BFS tree on undirected graphs
Introduction
@@ -28,11 +28,11 @@Lower bound
Consider the following graph:
-
-
+
We run BFS from the vertex and obtain the following BFS tree:
-
-
+
Let's consider pair of vertices and . For them we can safely lay, from the BFS tree, following properties:
- lower bound: @@ -42,12 +42,12 @@
Proof by contradiction
Let's keep the same graph, but break the lower bound, i.e. I have gotten a lower bound , but “there must be a shorter path”! ;)
Now the more important question, is there a shorter path in that graph? The answer is no, there's no shorter path than the one with length . So what can we do about it? We'll add an edge to have a shorter path. Now we have gotten a lower bound of , which means the only shorter path we can construct has edge and that is ‹› (no intermediary vertices). Let's do this!
-
-
+
Okay, so we have a graph that breaks the rule we have laid. However, we need to run BFS to obtain the new BFS tree, since we have changed the graph.
Do we need to run BFS after every change?
I am leaving that as an exercise ;)
-
+
Oops, we have gotten a new BFS tree, that has a height difference of 1.
Try to think about a way this can be generalized for shortening of minimal length 3 to minimal length 2 ;)
Iterative algorithms via iterators
Introduction
diff --git a/algorithms/hash-tables/breaking/index.html b/algorithms/hash-tables/breaking/index.html index 9f78f55..b906f2e 100644 --- a/algorithms/hash-tables/breaking/index.html +++ b/algorithms/hash-tables/breaking/index.html @@ -2,7 +2,7 @@ - +Breaking Hash Table
We will try to break a hash table and discuss possible ways how to prevent such diff --git a/algorithms/hash-tables/breaking/mitigations/index.html b/algorithms/hash-tables/breaking/mitigations/index.html index f9e0f6c..0d747f9 100644 --- a/algorithms/hash-tables/breaking/mitigations/index.html +++ b/algorithms/hash-tables/breaking/mitigations/index.html @@ -2,7 +2,7 @@
- +Possible Mitigations
There are multiple ways the issues created above can be mitigated. Still we can diff --git a/algorithms/hash-tables/breaking/python/index.html b/algorithms/hash-tables/breaking/python/index.html index 8842389..374e4a9 100644 --- a/algorithms/hash-tables/breaking/python/index.html +++ b/algorithms/hash-tables/breaking/python/index.html @@ -2,7 +2,7 @@
- +Breaking the Hash Table in Python
diff --git a/algorithms/index.html b/algorithms/index.html index dd9e99f..b770774 100644 --- a/algorithms/index.html +++ b/algorithms/index.html @@ -2,7 +2,7 @@ - +Introduction
In this part you can find “random” additional materials I have written over the @@ -23,6 +23,6 @@ course of teaching Algorithms and data structures I.
It is a various mix of stuff that may have been produced as a follow-up on some question asked at the seminar or spontanously.
If you have some ideas for posts, please do not hesitate to submit them as issues -in the linked GitLab.
A* algorithm
Intro
diff --git a/algorithms/paths/bf-to-astar/bf/index.html b/algorithms/paths/bf-to-astar/bf/index.html index 290417e..6cbc407 100644 --- a/algorithms/paths/bf-to-astar/bf/index.html +++ b/algorithms/paths/bf-to-astar/bf/index.html @@ -2,7 +2,7 @@ - +BF
Basic idea
diff --git a/algorithms/paths/bf-to-astar/dijkstra/index.html b/algorithms/paths/bf-to-astar/dijkstra/index.html index 2b264d3..2b6e909 100644 --- a/algorithms/paths/bf-to-astar/dijkstra/index.html +++ b/algorithms/paths/bf-to-astar/dijkstra/index.html @@ -2,7 +2,7 @@ - +Dijkstra's algorithm
Intro
@@ -37,7 +37,7 @@ Would that be even possible?Yes, it would! And that's when Dijkstra's algorithm comes in.
Dijkstra's algorithm
I'll start with a well-known meme about Dijkstra's algorithm:
-
And then follow up on that with the actual backstory from Dijkstra himself:
What is the shortest way to travel from Rotterdam to Groningen, in general: diff --git a/algorithms/paths/bf-to-astar/index.html b/algorithms/paths/bf-to-astar/index.html index b9bf28a..013cf61 100644 --- a/algorithms/paths/bf-to-astar/index.html +++ b/algorithms/paths/bf-to-astar/index.html @@ -2,7 +2,7 @@
- +From BF to A* | mf @@ -16,8 +16,8 @@ - - + +From BF to A*
Intro
diff --git a/algorithms/rb-trees/applications/index.html b/algorithms/rb-trees/applications/index.html index ad3d439..6aaa4ba 100644 --- a/algorithms/rb-trees/applications/index.html +++ b/algorithms/rb-trees/applications/index.html @@ -2,7 +2,7 @@ - +Použití červeno-černých stromů | mf @@ -16,8 +16,8 @@ - - + +Použití červeno-černých stromů
Použití
diff --git a/algorithms/rb-trees/rules/index.html b/algorithms/rb-trees/rules/index.html index a6266c2..c96fc73 100644 --- a/algorithms/rb-trees/rules/index.html +++ b/algorithms/rb-trees/rules/index.html @@ -2,7 +2,7 @@ - +On the rules of the red-black tree | mf @@ -16,8 +16,8 @@ - - + +On the rules of the red-black tree
Introduction
@@ -54,8 +54,8 @@ it means that there was no black node added on the path between us and therefore my child would be colored red.Example of a red-black tree that keeps count of black nodes on paths to the leaves follows:
-+
-
We mark the black heights in superscript. You can see that all leaves have the black height equal to . Let's take a look at some of the interesting cases:
@@ -101,14 +101,14 @@ both relying on the invariant in the algorithm and afterwards by enforcing the black root property.
If we decide to omit this condition, we need to address it in the pseudocodes accordingly.
-+
Usual algorithm with black root Allowing red root
Usual algorithm with black root Allowing red root 3ª Every leaf (
nil) is black.Now, this rule is a funny one. What does this imply and can I interpret this in some other way? Let's go through some of the possible ways I can look at this and how would they affect the other rules and balancing.
We will experiment with the following tree: -
+-
We should start by counting the black nodes from root to the
@@ -160,9 +160,9 @@ further. balancing of the tree below. -nilleaves based on the rules. We have multiple similar paths, so we will pick only the interesting ones.+
- Enforcing this rule
- Omitting this rule
-
-
- Enforcing this rule
- Omitting this rule
We can create a big subtree with only red nodes and even when keeping the rest of the rules maintained, it will break the time complexity. It stops us from “hacking” the black height requirement laid by the 5th rule.
diff --git a/algorithms/recursion/karel/index.html b/algorithms/recursion/karel/index.html index 41b4d68..efad64f 100644 --- a/algorithms/recursion/karel/index.html +++ b/algorithms/recursion/karel/index.html @@ -2,7 +2,7 @@ - +Recursion and backtracking with Robot Karel | mf @@ -16,8 +16,8 @@ - - + +Recursion and backtracking with Robot Karel
@@ -66,13 +66,13 @@ current location
Problem
Your task is to decide whether there is an exit from the maze or not. You can see an example of a maze here:
-+
Simple problem to get familiar with the robot
If you feel completely lost after the previous description, let me start you off with a simpler problem.
You are standing in front of the stairs, your task is to walk up the stairs.
You can see an example of such map here:
-+
Brainstorm the idea
As a first step write down any ideas and things that you have noticed or came to your mind. Ideally:
diff --git a/algorithms/recursion/karel/solution/index.html b/algorithms/recursion/karel/solution/index.html index e326772..fd3d00d 100644 --- a/algorithms/recursion/karel/solution/index.html +++ b/algorithms/recursion/karel/solution/index.html @@ -2,7 +2,7 @@ - +Solution to the problem | mf @@ -16,8 +16,8 @@ - - + +Solving the maze problem
diff --git a/algorithms/recursion/pyramid-slide-down/bottom-up-dp/index.html b/algorithms/recursion/pyramid-slide-down/bottom-up-dp/index.html index e3f2cdc..7067c4b 100644 --- a/algorithms/recursion/pyramid-slide-down/bottom-up-dp/index.html +++ b/algorithms/recursion/pyramid-slide-down/bottom-up-dp/index.html @@ -2,7 +2,7 @@ - +Bottom-up DP solution | mf @@ -16,8 +16,8 @@ - - + +Bottom-up dynamic programming
diff --git a/algorithms/recursion/pyramid-slide-down/greedy/index.html b/algorithms/recursion/pyramid-slide-down/greedy/index.html index 1e8dc4e..b7a0c54 100644 --- a/algorithms/recursion/pyramid-slide-down/greedy/index.html +++ b/algorithms/recursion/pyramid-slide-down/greedy/index.html @@ -2,7 +2,7 @@ - +Greedy solution | mf @@ -16,8 +16,8 @@ - - + +Greedy solution
We will try to optimize it a bit. Let's start with a relatively simple greedy diff --git a/algorithms/recursion/pyramid-slide-down/index.html b/algorithms/recursion/pyramid-slide-down/index.html index 49b9b0a..d264368 100644 --- a/algorithms/recursion/pyramid-slide-down/index.html +++ b/algorithms/recursion/pyramid-slide-down/index.html @@ -2,7 +2,7 @@
- +Introduction to dynamic programming | mf @@ -16,8 +16,8 @@ - - + +Introduction to dynamic programming
In this series we will try to solve one problem in different ways.
diff --git a/algorithms/recursion/pyramid-slide-down/naive/index.html b/algorithms/recursion/pyramid-slide-down/naive/index.html index 6f1d528..adafdeb 100644 --- a/algorithms/recursion/pyramid-slide-down/naive/index.html +++ b/algorithms/recursion/pyramid-slide-down/naive/index.html @@ -2,7 +2,7 @@ - +Naïve solution | mf @@ -16,8 +16,8 @@ - - + +Naïve solution
Our naïve solution consists of trying out all the possible slides and finding diff --git a/algorithms/recursion/pyramid-slide-down/top-down-dp/index.html b/algorithms/recursion/pyramid-slide-down/top-down-dp/index.html index 0aec925..2415276 100644 --- a/algorithms/recursion/pyramid-slide-down/top-down-dp/index.html +++ b/algorithms/recursion/pyramid-slide-down/top-down-dp/index.html @@ -2,7 +2,7 @@
- +Top-down DP solution | mf @@ -16,8 +16,8 @@ - - + +Top-down dynamic programming
diff --git a/algorithms/tags/a-star/index.html b/algorithms/tags/a-star/index.html index a8c7f44..c1e11e5 100644 --- a/algorithms/tags/a-star/index.html +++ b/algorithms/tags/a-star/index.html @@ -2,7 +2,7 @@ - +One doc tagged with "a star" | mf @@ -14,8 +14,8 @@ - - + +
