From 5eb338be7e6844739e8818d0d22ab7a0722f26bd Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 15 May 2024 07:59:08 -0600 Subject: [PATCH] Predicate transformers, set axioms, `leaq`. --- .../plugins/obsidian-to-anki-plugin/data.json | 21 +- notes/_journal/2024-05-13.md | 12 - notes/_journal/2024-05-15.md | 11 + notes/_journal/2024-05/2024-05-13.md | 14 + notes/_journal/2024-05/2024-05-14.md | 9 + notes/algorithms/sorting/heapsort.md | 4 +- notes/data-structures/heaps.md | 4 +- notes/programming/assertions.md | 130 --------- notes/programming/equiv-trans.md | 16 ++ notes/programming/pred-trans.md | 258 +++++++++++++++++ notes/programming/text-sub.md | 6 +- notes/set/axioms.md | 260 ++++++++++++++++++ notes/x86-64/instructions.md | 183 +++++++----- notes/x86-64/registers.md | 88 ++++++ 14 files changed, 785 insertions(+), 231 deletions(-) delete mode 100644 notes/_journal/2024-05-13.md create mode 100644 notes/_journal/2024-05-15.md create mode 100644 notes/_journal/2024-05/2024-05-13.md create mode 100644 notes/_journal/2024-05/2024-05-14.md delete mode 100644 notes/programming/assertions.md create mode 100644 notes/programming/pred-trans.md create mode 100644 notes/set/axioms.md create mode 100644 notes/x86-64/registers.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 9014009..5a61207 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -326,7 +326,7 @@ "_journal/2024-03-22.md": "8da8cda07d3de74f7130981a05dce254", "_journal/2024-03/2024-03-21.md": "cd465f71800b080afa5c6bdc75bf9cd3", "x86-64/declarations.md": "75bc7857cf2207a40cd7f0ee056af2f2", - "x86-64/instructions.md": "eef92b487920c7a15f38955c97a48a2d", + "x86-64/instructions.md": "c447f09c6b0ad504726c3232ff5871b4", "git/refs.md": "e20c2c9b14ba6c2bd235416017c5c474", "set/trees.md": "0d21b947917498f107da140cc9fb93a7", "_journal/2024-03-24.md": "1974cdb9fc42c3a8bebb8ac76d4b1fd6", @@ -390,12 +390,12 @@ "_journal/2024-04-28.md": "46726bf76a594b987c63ba8b9b6d13d3", "_journal/2024-04/2024-04-27.md": "b0f3753821c232bf819b00fb49415bd0", "_journal/2024-04/2024-04-26.md": "3ce37236a9e09e74b547a4f7231df5f0", - "algorithms/sorting/heapsort.md": "c5641af1431021751cba9bef96ee30bb", + "algorithms/sorting/heapsort.md": "d4f5a4d023b7a2e55035a8812acc71b6", "_journal/2024-04-29.md": "7888f4e9497c9d8bd6f4aa759d9abc4d", "_journal/2024-04/2024-04-28.md": "b34a9fe3bccb1f224b96ca00e78ad061", "programming/assertions.md": "d663ab31fc7e7296b6636edbffe9d8c7", - "programming/text-sub.md": "4bf5287353fc6571dd15be8f9f509bee", - "programming/equiv-trans.md": "fbadd593688e364ea92f74f23e54bcfc", + "programming/text-sub.md": "4ffcaf134858b478ffc3087b58026ee8", + "programming/equiv-trans.md": "77b02845208902d55d3048bc05584d6e", "programming/index.md": "bb082325e269a95236aa6aff9307fe59", "_journal/2024-04-30.md": "369f98b9d91de89cc1f4f581bc530c0d", "_journal/2024-04/2024-04-29.md": "b4fa2fd62e1b4fe34c1f71dc1e9f5b0b", @@ -404,7 +404,7 @@ "_journal/2024-05-01.md": "959ff67fe3db585ba6a7b121d853bbac", "_journal/2024-05-02.md": "d7d6ba7e065d807986f0bd77281c0bb1", "data-structures/priority-queues.md": "8c5c6bf62b1a39d8f1f72b800fcb17ff", - "data-structures/heaps.md": "0317372dcae8d81e4345c3ffa5c0cf90", + "data-structures/heaps.md": "a0289574930328d422b9b53047936274", "data-structures/index.md": "2605977fad54956b5dc2d8dda9be2b10", "abstract-data-types/priority-queues.md": "d3dad736cb05c47bdc93c52a3a4af083", "abstract-data-types/index.md": "6b110b20393c561497629ca4c3e09472", @@ -427,9 +427,16 @@ "_journal/2024-05/2024-05-08.md": "0f1b1b9e2abcf3203b511b9e034e86f4", "_journal/2024-05/2024-05-07.md": "4b1dde039a251f9a6dc7e606de98616d", "_journal/2024-05/2024-05-06.md": "bc9306348b7063b87741768391d9d8a7", - "_journal/2024-05-13.md": "2dfa53ff061ba94fcbe45261aad6bb30", + "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", - "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b" + "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b", + "programming/pred-trans.md": "241dc727a7a1cb5c899e5ddc7abb92fb", + "set/axioms.md": "8459540f07443284f80e8fb112c69d0a", + "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", + "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", + "x86-64/registers.md": "be5e22ceb14084c34f446dd91702477b", + "_journal/2024-05-15.md": "17e60d1515be44ac4121eb86060ec4dd", + "_journal/2024-05/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-13.md b/notes/_journal/2024-05-13.md deleted file mode 100644 index 4b0cbcc..0000000 --- a/notes/_journal/2024-05-13.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -title: "2024-05-13" ---- - -- [x] Anki Flashcards -- [x] KoL -- [ ] Sheet Music (10 min.) -- [ ] Go (1 Life & Death Problem) -- [ ] Korean (Read 1 Story) - -* Notes on [[graphs#Subgraphs|subgraphs]] and induced subgraphs. -* Notes on [[remotes]]. \ No newline at end of file diff --git a/notes/_journal/2024-05-15.md b/notes/_journal/2024-05-15.md new file mode 100644 index 0000000..f273943 --- /dev/null +++ b/notes/_journal/2024-05-15.md @@ -0,0 +1,11 @@ +--- +title: "2024-05-15" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Finished MOV instruction class practice problems in "Computer Systems: A Programmer's Perspective". Also notes on `leaq`. \ No newline at end of file diff --git a/notes/_journal/2024-05/2024-05-13.md b/notes/_journal/2024-05/2024-05-13.md new file mode 100644 index 0000000..3ea1a1f --- /dev/null +++ b/notes/_journal/2024-05/2024-05-13.md @@ -0,0 +1,14 @@ +--- +title: "2024-05-13" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Notes on [[graphs#Subgraphs|subgraphs]] and induced subgraphs. +* Notes on [[remotes]]. +* Read through chapter 7 of "The Science of Programming", touching on the $wp$ predicate transformer. +* Read chapter 1 of "Elements of Set Theory". Made some progress on chapter 2 which touches on the basic axiomatic foundations. \ No newline at end of file diff --git a/notes/_journal/2024-05/2024-05-14.md b/notes/_journal/2024-05/2024-05-14.md new file mode 100644 index 0000000..7c95aa0 --- /dev/null +++ b/notes/_journal/2024-05/2024-05-14.md @@ -0,0 +1,9 @@ +--- +title: "2024-05-14" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/algorithms/sorting/heapsort.md b/notes/algorithms/sorting/heapsort.md index 175a396..112838d 100644 --- a/notes/algorithms/sorting/heapsort.md +++ b/notes/algorithms/sorting/heapsort.md @@ -184,7 +184,7 @@ END%% %%ANKI Basic -What is initialization of `HEAPSORT`'s loop invariant? +What is initialization of `HEAPSORT`'s extraction-based loop invariant? Back: The input array is a max-heap. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). @@ -192,7 +192,7 @@ END%% %%ANKI Basic -What is maintenance of `HEAPSORT`'s loop invariant? +What is maintenance of `HEAPSORT`'s extraction-based loop invariant? Back: Swap the root with the last position of the heap. Heapify the new root. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). diff --git a/notes/data-structures/heaps.md b/notes/data-structures/heaps.md index 93c39df..9980e39 100644 --- a/notes/data-structures/heaps.md +++ b/notes/data-structures/heaps.md @@ -289,7 +289,7 @@ END%% %%ANKI Basic -How many internal nodes precede the first external node of a heap of size $n$? +How many internal nodes precede the first external node of a binary heap of size $n$? Back: $\lfloor n / 2 \rfloor$ Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). @@ -297,7 +297,7 @@ END%% %%ANKI Basic -What is the height of a binary heap defined? +How is the height of a binary heap defined? Back: The height of the heap's root when viewed as a complete binary tree. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). diff --git a/notes/programming/assertions.md b/notes/programming/assertions.md deleted file mode 100644 index 4074666..0000000 --- a/notes/programming/assertions.md +++ /dev/null @@ -1,130 +0,0 @@ ---- -title: Assertions -TARGET DECK: Obsidian::STEM -FILE TAGS: programming::assertions -tags: - - assertions - - programming ---- - -## Overview - -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 consequent 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 - -* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file diff --git a/notes/programming/equiv-trans.md b/notes/programming/equiv-trans.md index f71af50..1a20b73 100644 --- a/notes/programming/equiv-trans.md +++ b/notes/programming/equiv-trans.md @@ -153,6 +153,14 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +%%ANKI +Basic +If $p \Rightarrow q$, which of $p$ or $q$ is considered stronger? +Back: $p$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + %%ANKI Basic When is $p$ weaker than $q$? @@ -161,6 +169,14 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +%%ANKI +Basic +If $p \Rightarrow q$, which of $p$ or $q$ is considered weaker? +Back: $q$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + %%ANKI Basic A proposition is well-defined with respect to what? diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md new file mode 100644 index 0000000..db318de --- /dev/null +++ b/notes/programming/pred-trans.md @@ -0,0 +1,258 @@ +--- +title: Predicate Transformers +TARGET DECK: Obsidian::STEM +FILE TAGS: programming::pred-trans +tags: + - pred_trans + - programming +--- + +## Overview + +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 consequent 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 eventually terminates 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%% + +%%ANKI +Basic +*Why* is $\{T\}\; \text{while }T\text{ do skip}\; \{T\}$ everywhere false? +Back: Because $\text{while }T\text{ do skip}$ never terminates. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Weakest Precondition + +For any command $S$ and predicate $R$, we define the **weakest precondition** of $S$ with respect to $R$, denoted $wp(S, R)$, as + +> the set of *all* states such that execution of $S$ begun in any one of them is guaranteed to terminate in a finite amount of time in a state satisfying $R$. + +Expression $\{Q\}\; S\; \{R\}$ is equivalent to $Q \Rightarrow wp(S, R)$. + +%%ANKI +Basic +What is the predicate transformer $wp$ an acronym for? +Back: The **w**eakest **p**recondition. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given command $S$ and predicate $R$, how is $wp(S, R)$ defined? +Back: As the set of *all* states such that execution of $S$ in any one of them eventually terminates in a state satisfying $R$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In terms of implications, how does a precondition compare to the weakest precondition? +Back: A precondition implies the weakest precondition but not the other way around. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In terms of sets of states, how does a precondition compare to the weakest precondition? +Back: A precondition represents a subset of the states the weakest precondition represents. +Reference: 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\}$ equivalently written as a predicate involving $wp$? +Back: $Q \Rightarrow wp(S, R)$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $Q \Rightarrow wp(S, R)$ equivalently written as a predicate using assertions? +Back: $\{Q\}\; S\; \{R\}$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What kind of mathematical object is the $wp$ transformer? +Back: A function. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given command $S$ and predicate $R$, what kind of mathematical object is $wp(S, R)$? +Back: A set (of states). +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the term "predicate transformer" refer to? +Back: A function that transforms one predicate into another. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the following evaluate to? $$wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y)$$ +Back: $y \geq x$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the following evaluate to? $$wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y - 1)$$ +Back: $F$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the following evaluate to? $$wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y + 1)$$ +Back: $x = y + 1$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the following evaluate to? $$wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = max(x, y))$$ +Back: $T$ +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given command $S$, how is $wp(S, T)$ interpreted? +Back: As the set of all states such that execution of $S$ in any of them terminates in a finite amount of time. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Bibliography + +* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file diff --git a/notes/programming/text-sub.md b/notes/programming/text-sub.md index 7f6539a..3ead3ad 100644 --- a/notes/programming/text-sub.md +++ b/notes/programming/text-sub.md @@ -445,15 +445,15 @@ END%% %%ANKI Basic Given valid expression $(b; [i]{\circ}s{:}e)$, what is the type of $b$? -Back: A function. +Back: A function (an array). Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% %%ANKI Basic -Given valid expression $(b; \epsilon{\circ}s{:}e)$, what is the type of $b$? -Back: A scalar or function. +Given valid expression $(b; \epsilon{:}e)$, what is the type of $b$? +Back: A function or scalar. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% diff --git a/notes/set/axioms.md b/notes/set/axioms.md new file mode 100644 index 0000000..26c6150 --- /dev/null +++ b/notes/set/axioms.md @@ -0,0 +1,260 @@ +--- +title: Axioms +TARGET DECK: Obsidian::STEM +FILE TAGS: set +tags: + - set +--- + +## Overview + +Enderton describes ten different axioms in total which serve as the foundation of our set theory. + +## Extensionality + +If two sets have exactly the same members, then they are equal: $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ +%%ANKI +Basic +What does the extensionality axiom state? +Back: If two sets have exactly the same members, then they are equal. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the extensionality axiom expressed using first-order logic? +Back: $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following encodes which set theory axiom? $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ +Back: The extensionality axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How many sets exist with no members? +Back: Exactly one. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which set theory axiom proves uniqueness of $\varnothing$? +Back: The extensionality axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +## Empty Set Axiom + +There exists a set having no members: $$\exists B, \forall x, x \not\in B$$ + +%%ANKI +Basic +What does the empty set axiom state? +Back: There exists a set having no members. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the empty set axiom expressed using first-order logic? +Back: $$\exists B, \forall x, x \not\in B$$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following encodes which set theory axiom? $$\exists B, \forall x, x \not\in B$$ +Back: The empty set axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which set theory axiom proves existence of $\varnothing$? +Back: The empty set axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What two properties ensures definition $\varnothing$ is well-defined? +Back: The empty set exists and is unique. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +## Pairing Axiom + +For any sets $u$ and $v$, there exists a set having as members just $u$ and $v$: $$\forall u, \forall v, \exists B, \forall x, (x \in B \Leftrightarrow x = u \lor x = v)$$ + +%%ANKI +Basic +What does the pairing axiom state? +Back: For any sets $u$ and $v$, there exists a set having as members just $u$ and $v$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the pairing axiom expressed using first-order logic? +Back: $$\forall u, \forall v, \exists B, \forall x, (x \in B \Leftrightarrow x = u \lor x = v)$$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following encodes which set theory axiom? $$\forall u, \forall v, \exists B, \forall x, (x \in B \Leftrightarrow x = u \lor x = v)$$ +Back: The pairing axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which set theory axiom proves existence of set $\{x, y\}$ where $x \neq y$? +Back: The pairing axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which set theory axiom proves existence of set $\{x\}$? +Back: The pairing axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +For sets $u$ and $v$, what name is given to set $\{u, v\}$? +Back: The pair set of $u$ and $v$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +In set theory, what does a singleton refer to? +Back: A set with exactly one member. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What set theory axiom is used to prove existence of singletons? +Back: The pairing axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +## Union Axiom + +### Preliminary Form + +For any sets $a$ and $b$, there exists a set whose members are those sets belonging either to $a$ or to $b$ (or both): $$\forall a, \forall b, \exists B, \forall x, (x \in B \Leftrightarrow x \in a \lor x \in b)$$ + +%%ANKI +Basic +What does the union axiom (preliminary form) state? +Back: For any sets $a$ and $b$, there exists a set whose members are all in either $a$ or $b$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the union axiom (preliminary form) expressed using first-order logic? +Back: $$\forall a, \forall b, \exists B, \forall x, (x \in B \Leftrightarrow x \in a \lor x \in b)$$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following encodes which set theory axiom? $$\forall a, \forall b, \exists B, \forall x, (x \in B \Leftrightarrow x \in a \lor x \in b)$$ +Back: The union axiom (preliminary form). +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the union of sets $a$ and $b$ denoted? +Back: $a \cup b$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What two set theory axioms proves existence of e.g. $\{x_1, x_2, x_3\}$? +Back: The pairing axiom and union axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +## Power Set Axiom + +For any set $a$, there is a set whose members are exactly the subsets of $a$: $$\forall a, \exists B, \forall x, (x \in B \Leftrightarrow x \subseteq a)$$ + +%%ANKI +Basic +What does the power set axiom state? +Back: For any set $a$, there exists a set whose members are exactly the subsets of $a$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the power set axiom expressed using first-order logic? +Back: $$\forall a, \exists B, \forall x, (x \in B \Leftrightarrow x \subseteq a)$$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following encodes which set theory axiom? $$\forall a, \exists B, \forall x, (x \in B \Leftrightarrow x \subseteq a)$$ +Back: The power set axiom. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is $x \subseteq a$ rewritten using first-order logic and $\in$? +Back: $\forall t, t \in x \Rightarrow t \in a$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is the power set of set $a$ denoted? +Back: $\mathscr{P}{a}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +## Bibliography + +* Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). \ No newline at end of file diff --git a/notes/x86-64/instructions.md b/notes/x86-64/instructions.md index 6d1c02b..a245f5f 100644 --- a/notes/x86-64/instructions.md +++ b/notes/x86-64/instructions.md @@ -62,81 +62,6 @@ END%% ## Instruction Classes -An x86-64 CPU contains a set of 16 general-purpose registers storing 64-bit values. They are used to store integers and pointers. - -1 Byte | 2 Bytes | 4 Bytes | 8 Bytes | Purpose -------- | ------- | ------- | ------- | ------- -`%al` | `%ax` | `%eax` | `%rax` | Return value -`%bl` | `%bx` | `%ebx` | `%rbx` | Callee saved -`%cl` | `%cx` | `%ecx` | `%rcx` | 4th argument -`%dl` | `%dx` | `%edx` | `%rdx` | 3rd argument -`%sil` | `%si` | `%esi` | `%rsi` | 2nd argument -`%dil` | `%di` | `%edi` | `%rdi` | 1st argument -`%bpl` | `%bp` | `%ebp` | `%rbp` | Callee saved -`%spl` | `%sp` | `%esp` | `%rsp` | Stack pointer -`%r8b` | `%r8w` | `%r8d` | `%r8` | 5th argument -`%r9b` | `%r9w` | `%r9d` | `%r9` | 6th argument -`%r10b` | `%r10w` | `%r10d` | `%r10` | Caller saved -`%r11b` | `%r11w` | `%r11d` | `%r11` | Caller saved -`%r12b` | `%r12w` | `%r12d` | `%r12` | Callee saved -`%r13b` | `%r13w` | `%r13d` | `%r13` | Callee saved -`%r14b` | `%r14w` | `%r14d` | `%r14` | Callee saved -`%r15b` | `%r15w` | `%r15d` | `%r15` | Callee saved - -%%ANKI -Basic -How many general-purpose registers are available to x86-64 instructions? -Back: 16 -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Cloze -The x86 64-bit registers all start with prefix {`%r`}. -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Cloze -The x86 32-bit registers all start with prefix {`%e`}. -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Basic -Instructions that generate 1-byte quantities do what to the remaining bytes of a register? -Back: Leaves them alone. -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Basic -Instructions that generate 2-byte quantities do what to the remaining bytes of a register? -Back: Leaves them alone. -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Basic -Instructions that generate 4-byte quantities do what to the remaining bytes of a register? -Back: Zeroes them out. -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - -%%ANKI -Basic -Instructions that generate 8-byte quantities do what to the remaining bytes of a register? -Back: N/A -Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. - -END%% - There are three types of operands: * **Immediates**. These denote constant values. In ATT assembly, they are written with a `$` followed by an integer using standard C notation. @@ -774,6 +699,114 @@ Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Program END%% +### Load Effective Address + +| Instruction | Operands | Effect | Description | +| ----------- | -------- | ------- | ---------------------- | +| `leaq` | S, D | D <- &S | Load effective address | + +`leaq` is a variant of MOV. The first operand appears to be a memory address, but instead of reading from the designated location, the instruction copies the effective address to the designated location (a register). + +%%ANKI +Basic +`leaq` is considered a variant of what other instruction class? +Back: `MOV` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Why is the `leaq` instruction named the way it is? +Back: It stands for **l**oad **e**ffective **a**ddress. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Cloze +The {`leaq`} instruction is to x86-64 as the {`&`} operator is to C. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + +%%ANKI +Basic +Which x86-64 instruction is used to generate pointers? +Back: `leaq` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Why doesn't `leaq` have any other size variants? +Back: x96-64 addresses are always 64-bit. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Suppose `%rdx` contains $x$. Use `leaq` to set `%rax` to $5x + 7$. +Back: `leaq 7(%rdx, %rdx, 4), %rax` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Besides effect memory computations, how else is `leaq` used? +Back: For certain arithmetic operations. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Assume `%rbx` holds $p$ and `%rdx` holds $q$. What is the value of `%rax` in the following? +```asm +leaq 9(%rdx),%rax +``` +Back: $9 + q$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Assume `%rbx` holds $p$ and `%rdx` holds $q$. What is the value of `%rax` in the following? +```asm +leaq (%rdx, %rbx),%rax +``` +Back: $q + q$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Assume `%rbx` holds $p$ and `%rdx` holds $q$. What is the value of `%rax` in the following? +```asm +leaq 2(%rbx, %rbx, 7),%rax +``` +Back: $2 + 8p$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Assume `%rbx` holds $p$ and `%rdx` holds $q$. What is the value of `%rax` in the following? +```asm +leaq 0xE(, %rdx, 3),%rax +``` +Back: $14 + 3q$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + ## Bibliography * Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. diff --git a/notes/x86-64/registers.md b/notes/x86-64/registers.md new file mode 100644 index 0000000..aac4f6d --- /dev/null +++ b/notes/x86-64/registers.md @@ -0,0 +1,88 @@ +--- +title: Registers +TARGET DECK: Obsidian::STEM +FILE TAGS: x86-64 +tags: + - x86-64 +--- + +## Overview + +An x86-64 CPU contains a set of 16 general-purpose registers storing 64-bit values. They are used to store integers and pointers. + +1 Byte | 2 Bytes | 4 Bytes | 8 Bytes | Purpose +------- | ------- | ------- | ------- | ------- +`%al` | `%ax` | `%eax` | `%rax` | Return value +`%bl` | `%bx` | `%ebx` | `%rbx` | Callee saved +`%cl` | `%cx` | `%ecx` | `%rcx` | 4th argument +`%dl` | `%dx` | `%edx` | `%rdx` | 3rd argument +`%sil` | `%si` | `%esi` | `%rsi` | 2nd argument +`%dil` | `%di` | `%edi` | `%rdi` | 1st argument +`%bpl` | `%bp` | `%ebp` | `%rbp` | Callee saved +`%spl` | `%sp` | `%esp` | `%rsp` | Stack pointer +`%r8b` | `%r8w` | `%r8d` | `%r8` | 5th argument +`%r9b` | `%r9w` | `%r9d` | `%r9` | 6th argument +`%r10b` | `%r10w` | `%r10d` | `%r10` | Caller saved +`%r11b` | `%r11w` | `%r11d` | `%r11` | Caller saved +`%r12b` | `%r12w` | `%r12d` | `%r12` | Callee saved +`%r13b` | `%r13w` | `%r13d` | `%r13` | Callee saved +`%r14b` | `%r14w` | `%r14d` | `%r14` | Callee saved +`%r15b` | `%r15w` | `%r15d` | `%r15` | Callee saved + +%%ANKI +Basic +How many general-purpose registers are available to x86-64 instructions? +Back: 16 +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Cloze +The x86 64-bit registers all start with prefix {`%r`}. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Cloze +The x86 32-bit registers all start with prefix {`%e`}. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Instructions that generate 1-byte quantities do what to the remaining bytes of a register? +Back: Leaves them alone. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Instructions that generate 2-byte quantities do what to the remaining bytes of a register? +Back: Leaves them alone. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Instructions that generate 4-byte quantities do what to the remaining bytes of a register? +Back: Zeroes them out. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Instructions that generate 8-byte quantities do what to the remaining bytes of a register? +Back: N/A +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +## Bibliography + +* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. \ No newline at end of file