Shifts and law of monotonicity.
parent
16ffe8d4ef
commit
06e0550b38
|
@ -260,7 +260,7 @@
|
|||
"filesystems/cas.md": "d41c0d2e943adecbadd10a03fd1e4274",
|
||||
"git/objects.md": "8c1da67ac3f568624c3f9623eb2133e1",
|
||||
"git/index.md": "ca842957bda479dfa1170ae85f2f37b8",
|
||||
"encoding/integer.md": "17387c74064bc738c4b4929ab37a0f56",
|
||||
"encoding/integer.md": "ab0db8d48734867d42279fb2f2362d25",
|
||||
"_journal/2024-02-29.md": "f610f3caed659c1de3eed5f226cab508",
|
||||
"_journal/2024-02/2024-02-28.md": "7489377c014a2ff3c535d581961b5b82",
|
||||
"_journal/2024-03-01.md": "a532486279190b0c12954966cbf8c3fe",
|
||||
|
@ -309,7 +309,7 @@
|
|||
"_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f",
|
||||
"_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b",
|
||||
"set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53",
|
||||
"set/index.md": "85eef335afe27f8c0308c9ef5aa5d3ca",
|
||||
"set/index.md": "b8165da42a81b5dc01b0a44ce365804e",
|
||||
"set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800",
|
||||
"_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb",
|
||||
"_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391",
|
||||
|
@ -328,7 +328,7 @@
|
|||
"_journal/2024-03-22.md": "8da8cda07d3de74f7130981a05dce254",
|
||||
"_journal/2024-03/2024-03-21.md": "cd465f71800b080afa5c6bdc75bf9cd3",
|
||||
"x86-64/declarations.md": "75bc7857cf2207a40cd7f0ee056af2f2",
|
||||
"x86-64/instructions.md": "6f18c3e6d01c80dc5ce6ec05c66ff627",
|
||||
"x86-64/instructions.md": "a9fa4596009395c4161fd8601a669c6c",
|
||||
"git/refs.md": "e20c2c9b14ba6c2bd235416017c5c474",
|
||||
"set/trees.md": "c29347ec0ac2e8d5339514c869ecaedf",
|
||||
"_journal/2024-03-24.md": "1974cdb9fc42c3a8bebb8ac76d4b1fd6",
|
||||
|
@ -432,7 +432,7 @@
|
|||
"_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b",
|
||||
"_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365",
|
||||
"git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b",
|
||||
"programming/pred-trans.md": "9ea72ae99f4de83531b27f4621d21616",
|
||||
"programming/pred-trans.md": "fe30f0cab01fd31640f0778bf983747f",
|
||||
"set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7",
|
||||
"_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5",
|
||||
"_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b",
|
||||
|
@ -446,12 +446,14 @@
|
|||
"_journal/2024-05-17.md": "fb880d68077b655ede36d994554f3aba",
|
||||
"_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c",
|
||||
"_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c",
|
||||
"hashing/direct-addressing.md": "05c93ad0fe50092f2abff696888147d0",
|
||||
"hashing/direct-addressing.md": "17daf22ed3dfcc465924a175e8f11ce3",
|
||||
"hashing/index.md": "340f8583eb51eaef011e3302bddb7ff8",
|
||||
"set/classes.md": "a0bb2532284dea67bbfe7c1e3d714fd1",
|
||||
"set/classes.md": "c933ca5dfebc3a0298e8ad948c6877a3",
|
||||
"_journal/2024-05-19.md": "fddd90fae08fab9bd83b0ef5d362c93a",
|
||||
"_journal/2024-05/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c",
|
||||
"_journal/2024-05/2024-05-17.md": "fb880d68077b655ede36d994554f3aba"
|
||||
"_journal/2024-05/2024-05-17.md": "fb880d68077b655ede36d994554f3aba",
|
||||
"_journal/2024-05-20.md": "350024abe16438d4cdd2ceaf95cb53c4",
|
||||
"_journal/2024-05/2024-05-19.md": "fc14fc23d4ddca3628df7eec71a07e27"
|
||||
},
|
||||
"fields_dict": {
|
||||
"Basic": [
|
||||
|
|
|
@ -0,0 +1,12 @@
|
|||
---
|
||||
title: "2024-05-20"
|
||||
---
|
||||
|
||||
- [x] Anki Flashcards
|
||||
- [x] KoL
|
||||
- [ ] Sheet Music (10 min.)
|
||||
- [ ] Go (1 Life & Death Problem)
|
||||
- [ ] Korean (Read 1 Story)
|
||||
|
||||
* Flashcards for x86-64 [[instructions#Shift Operations|shift operations]].
|
||||
* Flashcards on the [[pred-trans#Law of Monotonicity|Law of Monotonicity]].
|
|
@ -9,3 +9,4 @@ title: "2024-05-19"
|
|||
- [ ] Korean (Read 1 Story)
|
||||
|
||||
* Flashcards on x86-64 [[instructions#Unary Operations|unary operations]] and [[instructions#Binary Operations|binary operations]].
|
||||
* Struggled with getting Flutter up and running on NixOS.
|
|
@ -1440,7 +1440,7 @@ END%%
|
|||
%%ANKI
|
||||
Basic
|
||||
What kinds of right shift operations are there?
|
||||
Back: Logical and arithmetic
|
||||
Back: Logical and arithmetic.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1707854589784-->
|
||||
END%%
|
||||
|
|
|
@ -53,7 +53,7 @@ END%%
|
|||
%%ANKI
|
||||
Basic
|
||||
Write pseudocode to test membership of $x$ in direct-address table `T[0:m-1]`.
|
||||
Back
|
||||
Back:
|
||||
```c
|
||||
bool membership(T, x) {
|
||||
return T[x.key] != NIL;
|
||||
|
@ -66,7 +66,7 @@ END%%
|
|||
%%ANKI
|
||||
Basic
|
||||
Write pseudocode to insert $x$ into direct-address table `T[0:m-1]`.
|
||||
Back
|
||||
Back:
|
||||
```c
|
||||
void insert(T, x) {
|
||||
T[x.key] = x;
|
||||
|
@ -79,7 +79,7 @@ END%%
|
|||
%%ANKI
|
||||
Basic
|
||||
Write pseudocode to delete $x$ from direct-address table `T[0:m-1]`.
|
||||
Back
|
||||
Back:
|
||||
```c
|
||||
void delete(T, x) {
|
||||
T[x.key] = NIL;
|
||||
|
|
|
@ -297,6 +297,14 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon
|
|||
<!--ID: 1715806256921-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In Gries's exposition, is the Law of the Excluded Miracle taken as an axiom or a theorem?
|
||||
Back: An axiom.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1716227332852-->
|
||||
END%%
|
||||
|
||||
### Distributivity of Conjunction
|
||||
|
||||
Given command $S$ and predicates $Q$ and $R$, $$wp(S, Q \land R) = wp(S, Q) \land wp(S, R)$$
|
||||
|
@ -326,7 +334,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
Does $wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R)$ hold when $S$ is nondeterministic?
|
||||
Is $wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R)$ true if $S$ is nondeterministic?
|
||||
Back: Yes.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1715969047065-->
|
||||
|
@ -334,7 +342,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
Does $wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R)$ hold when $S$ is nondeterministic?
|
||||
Is $wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R)$ true if $S$ is nondeterministic?
|
||||
Back: Yes.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1715969047067-->
|
||||
|
@ -348,6 +356,39 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon
|
|||
<!--ID: 1715969047068-->
|
||||
END%%
|
||||
|
||||
### Law of Monotonicity
|
||||
|
||||
Given command $S$ and predicates $Q$ and $R$, if $Q \Rightarrow R$, then $wp(S, Q) \Rightarrow wp(S, R)$.
|
||||
|
||||
%%ANKI
|
||||
What does the Law of Monotonicity state?
|
||||
Back: Given command $S$ and predicates $Q$ and $R$, if $Q \Rightarrow R$, then $wp(S, 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
|
||||
Cloze
|
||||
Given command $S$, the Law of Monotonicity states that if {1:$Q$} $\Rightarrow$ {2:$R$}, then {2:$wp(S, Q)$} $\Rightarrow$ {1:$wp(S, R)$}.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1716227332862-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In Gries's exposition, is the Law of Monotonicity taken as an axiom or a theorem?
|
||||
Back: A theorem.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1716227332866-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is the Law of Monotonicity true if the relevant command is nondeterministic?
|
||||
Back: Yes.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1716227332870-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
|
@ -30,7 +30,7 @@ END%%
|
|||
%%ANKI
|
||||
Basic
|
||||
What does the Zermelo-Fraenkel alternative say about classes?
|
||||
Back: It gives it no ontological status at all.
|
||||
Back: It gives them no ontological status at all.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1715970576763-->
|
||||
END%%
|
||||
|
|
|
@ -418,7 +418,7 @@ For each formula $\_\_\_$ not containing $B$, the following is an axiom: $$\fora
|
|||
%%ANKI
|
||||
Basic
|
||||
What do the subset axioms state?
|
||||
Back: For each formula $\phi$ not containing $B$, the following is an axiom: $$\forall t_1, \cdots, \forall t_k, \forall c, \exists B, \forall x, (x \in B \Leftrightarrow x \in c \land \_\_\_)$$
|
||||
Back: For each formula $\_\_\_$ not containing $B$, the following is an axiom: $$\forall t_1, \cdots, \forall t_k, \forall c, \exists B, \forall x, (x \in B \Leftrightarrow x \in c \land \_\_\_)$$
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1716074312858-->
|
||||
END%%
|
||||
|
|
|
@ -1069,6 +1069,136 @@ Tags: c17
|
|||
<!--ID: 1716128138046-->
|
||||
END%%
|
||||
|
||||
### Shift Operations
|
||||
|
||||
| Instruction | Operands | Effect | Description |
|
||||
| ----------- | -------- | ------------ | ---------------------- |
|
||||
| `sal[bwlq]` | k, D | D <- D << k | Left shift |
|
||||
| `shl[bwlq]` | k, D | D <- D << k | Left shift |
|
||||
| `sar[bwlq]` | k, D | D <- D >> k | Arithmetic right shift |
|
||||
| `shr[bwlq]` | k, D | D <- D >>> k | Logical right shift |
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do instructions in the `SAL` instruction class do?
|
||||
Back: Performs a left shift.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827710-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do instructions in the `SHL` instruction class do?
|
||||
Back: Performs a left shift.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827717-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which instruction classes are related to left shifts?
|
||||
Back: `SAL` and `SHL`.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827720-->
|
||||
END%%
|
||||
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which instruction classes are related to right shifts?
|
||||
Back: `SAR` and `SHR`.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827723-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do instructions in the `SAR` instruction class do?
|
||||
Back: Performs an arithmetic right shift.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827725-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do instructions in the `SHR` instruction class do?
|
||||
Back: Performs a logical right shift.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827729-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What distinguishes the `SAR` and `SHR` instruction classes?
|
||||
Back: The former is arithmetic whereas the latter is logical.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827732-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What distinguishes the `SAL` and `SHL` instruction classes?
|
||||
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.
|
||||
<!--ID: 1716226827736-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which register are shift operations limited to?
|
||||
Back: `%cl`
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827740-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many lower-order bits of `%cl` does e.g. `salb` look at?
|
||||
Back: $3$
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827744-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What can the source of a shift operation be?
|
||||
Back: An immediate or the `%cl` register.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827748-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What can the destination of a shift operation be?
|
||||
Back: A register or memory location.
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827752-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many lower-order bits of `%cl` does e.g. `salw` look at?
|
||||
Back: $4$
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827756-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many lower-order bits of `%cl` does e.g. `sall` look at?
|
||||
Back: $5$
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827760-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many lower-order bits of `%cl` does e.g. `salq` look at?
|
||||
Back: $6$
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1716226827764-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
|
|
Loading…
Reference in New Issue