Vague postconditions and proving correctness of algorithms
Introduction
@@ -99,7 +99,7 @@ This will ensure that even if the maximum in the original array was the first elWe pass to the sorting function copy of the numbers we got, this ensures that once we are checking the more strict postcondition, we can gather the necessary information even after sorting the list in-situ, i.e. we can check if the result
is really a permutation
of the numbers
even though the sorting functions has modified the passed in list.
Now we get to the more complicated part and it is the decorators.
Now we get to the more complicated part and it is the decorators.
-
1st
diff --git a/algorithms/category/algorithms-and-correctness/index.html b/algorithms/category/algorithms-and-correctness/index.html index e543a7b..93dffe6 100644 --- a/algorithms/category/algorithms-and-correctness/index.html +++ b/algorithms/category/algorithms-and-correctness/index.html @@ -2,7 +2,7 @@ - +parametrize
from the bottomAlgorithms and Correctness | mf - - + + +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 4efcdad..98525b8 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 | mf @@ -15,9 +15,9 @@ - - - + + +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 e0ea94f..7989bb5 100644 --- a/algorithms/category/graphs/index.html +++ b/algorithms/category/graphs/index.html @@ -2,7 +2,7 @@
- +Graphs | mf @@ -15,9 +15,9 @@ - - - + + +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 afdf0ac..b6874ec 100644 --- a/algorithms/category/hash-tables/index.html +++ b/algorithms/category/hash-tables/index.html @@ -2,7 +2,7 @@
- +Hash Tables | mf @@ -15,9 +15,9 @@ - - - + + +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 ee3e48d..d02e6a3 100644 --- a/algorithms/category/paths-in-graphs/index.html +++ b/algorithms/category/paths-in-graphs/index.html @@ -2,7 +2,7 @@
- +Paths in Graphs | mf @@ -15,9 +15,9 @@ - - - + + +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 c4ab50b..d93a461 100644 --- a/algorithms/category/recursion/index.html +++ b/algorithms/category/recursion/index.html @@ -2,7 +2,7 @@
- +Recursion | mf @@ -15,9 +15,9 @@ - - - + + +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 178d71b..6e16d99 100644 --- a/algorithms/category/red-black-trees/index.html +++ b/algorithms/category/red-black-trees/index.html @@ -2,7 +2,7 @@
- +Red-Black Trees | mf @@ -15,9 +15,9 @@ - - - + + +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 799e504..35eb554 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 | mf @@ -15,9 +15,9 @@ - - - + + +diff --git a/algorithms/graphs/iterative-and-iterators/index.html b/algorithms/graphs/iterative-and-iterators/index.html index de575ed..63a77c5 100644 --- a/algorithms/graphs/iterative-and-iterators/index.html +++ b/algorithms/graphs/iterative-and-iterators/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.
-tipDo 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.
tipTry to think about a way this can be generalized for shortening of minimal length 3 to minimal length 2 ;)
Iterative algorithms via iterators | mf @@ -15,9 +15,9 @@ - - - + + +Iterative algorithms via iterators
Introduction
diff --git a/algorithms/hash-tables/breaking/index.html b/algorithms/hash-tables/breaking/index.html index 3e8e50f..b4f92aa 100644 --- a/algorithms/hash-tables/breaking/index.html +++ b/algorithms/hash-tables/breaking/index.html @@ -2,7 +2,7 @@ - +Breaking hash table | mf @@ -15,9 +15,9 @@ - - - + + +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 3a63f77..d9c1b5e 100644 --- a/algorithms/hash-tables/breaking/mitigations/index.html +++ b/algorithms/hash-tables/breaking/mitigations/index.html @@ -2,7 +2,7 @@
- +Possible Mitigations | mf @@ -15,9 +15,9 @@ - - - + + +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 e91e891..257051b 100644 --- a/algorithms/hash-tables/breaking/python/index.html +++ b/algorithms/hash-tables/breaking/python/index.html @@ -2,7 +2,7 @@
- +Breaking Python | mf @@ -15,9 +15,9 @@ - - - + + +\ No newline at end of file diff --git a/algorithms/paths/bf-to-astar/astar/index.html b/algorithms/paths/bf-to-astar/astar/index.html index 19dae16..3c46f0d 100644 --- a/algorithms/paths/bf-to-astar/astar/index.html +++ b/algorithms/paths/bf-to-astar/astar/index.html @@ -2,7 +2,7 @@ - +Breaking the Hash Table in Python
diff --git a/algorithms/index.html b/algorithms/index.html index 0edfb2e..9adfedf 100644 --- a/algorithms/index.html +++ b/algorithms/index.html @@ -2,7 +2,7 @@ - +Introduction | mf @@ -13,9 +13,9 @@ - - - + + ++in the linked GitLab.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 | mf @@ -15,9 +15,9 @@ - - - + + +A* algorithm
Intro
diff --git a/algorithms/paths/bf-to-astar/bf/index.html b/algorithms/paths/bf-to-astar/bf/index.html index ced7bce..869efe2 100644 --- a/algorithms/paths/bf-to-astar/bf/index.html +++ b/algorithms/paths/bf-to-astar/bf/index.html @@ -2,7 +2,7 @@ - +BF | mf - - + + +BF
Basic idea
diff --git a/algorithms/paths/bf-to-astar/dijkstra/index.html b/algorithms/paths/bf-to-astar/dijkstra/index.html index 67082b0..a5c542c 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 | mf @@ -15,9 +15,9 @@ - - - + + +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: @@ -56,7 +56,7 @@ cornerstones of my fame.
— Edsger Dijkstra, in an interview with Philip L. Frana, Communications of the ACM, 2001
PreconditionAs our own naïve algorithm, Dijkstra's algorithm has a precondition that places +
diff --git a/algorithms/paths/bf-to-astar/index.html b/algorithms/paths/bf-to-astar/index.html index bce689b..b3a4c01 100644 --- a/algorithms/paths/bf-to-astar/index.html +++ b/algorithms/paths/bf-to-astar/index.html @@ -2,7 +2,7 @@ - +PreconditionAs our own naïve algorithm, Dijkstra's algorithm has a precondition that places a requirement of no edges with negative weights in the graph. This precondition is required because of the nature of the algorithm that requires monotonically non-decreasing changes in the costs of shortest paths.
From BF to A* | mf @@ -15,9 +15,9 @@ - - - + + +From BF to A*
Intro
diff --git a/algorithms/rb-trees/applications/index.html b/algorithms/rb-trees/applications/index.html index f8cac0e..b8eca10 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 @@ -15,9 +15,9 @@ - - - + + +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 c673760..835c232 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 @@ -15,9 +15,9 @@ - - - + + +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.
- Enforcing this rule
- Omitting this rule
- Enforcing this rule
- Omitting this rule
-
We retrieve it from the cache. Same as in first point, but only twice, so we get
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
@@ -127,7 +127,7 @@ This affects all paths and therefore results in global decrease as it should be. However, there is one difference. Second path no longer satisfies the condition of a leaf. Technically it relaxes the 5th rule, because we leave out some of the nodes. We should probably avoid that. -nil
leaves based on the rules. We have multiple similar paths, so we will pick only the interesting ones.cautionWith the second idea, you may also feel that we are “bending” the rules a bit, +
@@ -160,9 +160,9 @@ further. balancing of the tree below. -cautionWith the second idea, you may also feel that we are “bending” the rules a bit, especially the definition of the “leaf” nodes.
Given the definition of the red-black tree, where
nil
is considered to be an external node, we have decided that bending it a bit just to stir a thought about it won't hurt anybody. 😉+-
-
+
+
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 3c5e554..431a0b6 100644 --- a/algorithms/recursion/karel/index.html +++ b/algorithms/recursion/karel/index.html @@ -2,7 +2,7 @@ - +Recursion and backtracking with Robot Karel | mf @@ -15,9 +15,9 @@ - - - + + +Recursion and backtracking with Robot Karel
-
@@ -62,17 +62,17 @@ current location
+cautionHelper functions / procedures are allowed. Return values are allowed.
Variables are prohibited!
cautionHelper functions / procedures are allowed. Return values are allowed.
Variables are prohibited!
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 82e59d3..72f8041 100644 --- a/algorithms/recursion/karel/solution/index.html +++ b/algorithms/recursion/karel/solution/index.html @@ -2,7 +2,7 @@ - +Solution to the problem | mf @@ -15,9 +15,9 @@ - - - + + +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 eeb6293..eed5f13 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 @@ -15,9 +15,9 @@ - - - + + +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 d786643..3fea29b 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 @@ -15,9 +15,9 @@ - - - + + +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 d1c7e0b..c95ac70 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 @@ -15,9 +15,9 @@ - - - + + +Introduction to dynamic programming
In this series we will try to solve one problem in different ways.
@@ -35,7 +35,7 @@75
95 64
17 47 82
18 35 87 10
20 4 82 47 65
19 1 23 3 34
88 2 77 73 7 63 67
99 65 4 28 6 16 70 92
41 41 26 56 83 40 80 70 33
41 48 72 33 47 32 37 16 94 29
53 71 44 65 25 43 91 52 97 51 14
70 11 33 28 77 73 17 78 39 68 17 57
91 71 52 38 17 14 91 43 58 50 27 29 48
63 66 4 68 89 53 67 30 73 16 69 87 40 31
4 62 98 27 23 9 70 98 73 93 38 53 60 4 23Slide down in this case is equal to
1074
.Solving the problem
-cautionI will describe the following ways you can approach this problem and implement +
cautionI will describe the following ways you can approach this problem and implement them in Java1.
For all of the following solutions I will be using basic
- +main
function that will outputtrue
/false
based on the expected output of our algorithm. Any diff --git a/algorithms/recursion/pyramid-slide-down/naive/index.html b/algorithms/recursion/pyramid-slide-down/naive/index.html index 8daf9f4..a79f3dd 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 @@ -15,9 +15,9 @@ - - - + + +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 dc36a30..1b1bebd 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 @@ - +Naïve solution
Our naïve solution consists of trying out all the possible slides and finding @@ -71,7 +71,7 @@ subtrees. binary tree of height
y
, in each node we do some work in constant time, therefore we can just sum the ones. -warningIt would've been more complicated to get an exact result. In the equation above +
dangerIt would've been more complicated to get an exact result. In the equation above we are assuming that the width of the pyramid is bound by the height.
Hopefully we can agree that this is not the best we can do. 😉
Top-down DP solution | mf @@ -15,9 +15,9 @@ - - - + + +Top-down dynamic programming
@@ -65,7 +65,7 @@ complexity and therefore this step is equivalent to -cautionYou might have noticed it's still not that easy, cause we're not having full +
cautionYou might have noticed it's still not that easy, cause we're not having full cache right from the beginning, but the sum of those logarithms cannot be expressed in a nice way, so taking the upper bound, i.e. expecting the cache to be full at all times, is the best option for nice and readable complexity @@ -75,7 +75,7 @@ of the whole approach.