Add program assertions.

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"

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.
+* Notes on chapter 5.3 and 6 of "The Science of Programming".
-* Read chapter 6 of "The Science of Programming". Still need to convert into notes though.
+	* Covered nested arrays and assertions.
 * Finished notes on heaps and heapsort.

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.
+<!--ID: 1714420640219-->
+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.
+<!--ID: 1714420640222-->
+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.
+<!--ID: 1714420640224-->
+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.
+<!--ID: 1714420640226-->
+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.
+<!--ID: 1714420640227-->
+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.
+<!--ID: 1714420640229-->
+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.
+<!--ID: 1714420640231-->
+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.
+<!--ID: 1714420640232-->
+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.
+<!--ID: 1714420640234-->
+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.
+<!--ID: 1714420640235-->
+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.
+<!--ID: 1714420640237-->
+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.
+<!--ID: 1714420640238-->
+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.
+<!--ID: 1714420640240-->
+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.
+<!--ID: 1714420640241-->
+END%%
 
 ## Bibliography