diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 40177ac..4c7e3af 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -385,7 +385,7 @@ "algorithms/sorting/heapsort.md": "94ac936dac6c841b4d0c9b7df3eba0d3", "_journal/2024-04-29.md": "f751826099e2c746605a4e562288d480", "_journal/2024-04/2024-04-28.md": "b34a9fe3bccb1f224b96ca00e78ad061", - "programming/assertions.md": "bdef9b934d8db94169d6befbc02f33d2", + "programming/assertions.md": "cf7996590c9f5eefd6f7862c4f92132e", "programming/text-sub.md": "003b8c32ae2f6767cb0d900f85196e67", "programming/equiv-trans.md": "fbadd593688e364ea92f74f23e54bcfc", "programming/index.md": "bb082325e269a95236aa6aff9307fe59" diff --git a/notes/_journal/2024-04-29.md b/notes/_journal/2024-04-29.md index 9d32f56..fe57e1e 100644 --- a/notes/_journal/2024-04-29.md +++ b/notes/_journal/2024-04-29.md @@ -10,6 +10,6 @@ title: "2024-04-29" - [ ] Interview Prep (1 Practice Problem) - [x] Log Work Hours (Max 3 hours) -* Notes on chapter 5.3 of "The Science of Programming". Covered nested arrays. -* Read chapter 6 of "The Science of Programming". Still need to convert into notes though. +* Notes on chapter 5.3 and 6 of "The Science of Programming". + * Covered nested arrays and assertions. * Finished notes on heaps and heapsort. \ No newline at end of file diff --git a/notes/programming/assertions.md b/notes/programming/assertions.md index 4aa21f8..dfd7742 100644 --- a/notes/programming/assertions.md +++ b/notes/programming/assertions.md @@ -9,7 +9,121 @@ tags: ## Overview -TODO +Define $\{Q\}\; S\; \{R\}$ as the predicate: + +> If execution of $S$ is begun in a state satisfying $Q$, then it is guaranteed to terminate in a finite amount of time in a state satisfying $R$. + +%%ANKI +Basic +*What* is $Q$ in predicate $\{Q\}\; S\; \{R\}$? +Back: A predicate. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to $Q$ in $\{Q\}\; S\; \{R\}$? +Back: The precondition of $S$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +*What* is $R$ in predicate $\{Q\}\; S\; \{R\}$? +Back: A predicate. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to $R$ in $\{Q\}\; S\; \{R\}$? +Back: The postcondition of $S$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +*What* is $S$ in predicate $\{Q\}\; S\; \{R\}$? +Back: A program (a sequence of statements). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the antecedent of $\{Q\}\; S\; \{R\}$ in English? +Back: $S$ is executed in a state satisfying $Q$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the consequenct of $\{Q\}\; S\; \{R\}$ in English? +Back: $S$ terminates in a finite amount of time in a state satisfying $R$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\{Q\}\; S\; \{R\}$ defined? +Back: If $S$ is executed in a state satisfying $Q$, it terminates in a finite amount of time in a state satisfying $R$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\{x = X \land y = Y\}\; swap\; \{x = Y \land y = X\}$ rewritten without free identifiers? +Back: $\forall x, y, X, Y, \{x = X \land y = Y\}\; swap\; \{x = Y \land y = X\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to $X$ in e.g. $\{x = X\}\; S\; \{y = Y\}$? +Back: The initial value of $x$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\{Q\}\; S\; \{R\}$ augmented so that $x$ has initial value $X$? +Back: $\{Q \land x = X\}\; S\; \{R\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to $Y$ in e.g. $\{x = X\}\; S\; \{y = Y\}$? +Back: The final value of $y$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\{Q\}\; S\; \{R\}$ augmented so that $y$ has final value $X$? +Back: $\{Q\}\; S\; \{R \land y = X\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\{Q\}\; S\; \{R\}$ augmented so that $y$ has initial value $X$? +Back: $\{Q \land y = X\}\; S\; \{R\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% ## Bibliography