From 3d7e3e69c06e210cf785ff4d51dbf7de83043585 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 15 Feb 2022 01:15:21 -0500 Subject: [PATCH 1/4] Fixed link --- content/blog/termtosvg.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/blog/termtosvg.md b/content/blog/termtosvg.md index 2bb07db..2d3fd3a 100644 --- a/content/blog/termtosvg.md +++ b/content/blog/termtosvg.md @@ -6,7 +6,7 @@ tags: [] math: false --- -With [`termtosvg`](https://github.com/nbedos/termtosvg) made by Nicolas Bedo we can make SVG animations from terminal output in the style of [asciinema](https://asciinema.org/). To install use [pipx](http://localhost:1313/blog/managepythonapps/). +With [`termtosvg`](https://github.com/nbedos/termtosvg) made by Nicolas Bedo we can make SVG animations from terminal output in the style of [asciinema](https://asciinema.org/). To install use [pipx](/blog/managepythonapps/). ```bash pipx install termtosvg From 7c865ae494d30838a7982e68afac0d9a7bff95fb Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 15 Feb 2022 01:15:38 -0500 Subject: [PATCH 2/4] Updated theme --- config.toml | 11 +++++++---- themes/pulp | 2 +- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/config.toml b/config.toml index 995aadb..5348845 100644 --- a/config.toml +++ b/config.toml @@ -14,7 +14,9 @@ enableGitInfo = true favicon = "favicon.ico" description = "Software Developer, Researcher, and Linux Enthusiast." publicationYear = "2021" - identities = ["https://github.com/brandon-rozek", "mailto:hello@brandonrozek.com"] + identities = [ + "mailto:hello@brandonrozek.com" + ] [outputs] section = ["JSON", "HTML", "RSS"] @@ -63,21 +65,22 @@ enableGitInfo = true weight = 50 -[[menu.main]] +[[menu.profile]] identifier = "github" name = "GitHub" pre = "" url = "https://github.com/brandon-rozek" weight = 80 + me = true -[[menu.main]] +[[menu.profile]] identifier = "scholar" name = "Google Scholar" pre = "" url = "https://scholar.google.com/citations?user=JrgtnwgAAAAJ&hl=en&oi=ao" weight = 85 -[[menu.main]] +[[menu.profile]] identifier = "email" name = "Email" pre = "" diff --git a/themes/pulp b/themes/pulp index d683165..e699ce6 160000 --- a/themes/pulp +++ b/themes/pulp @@ -1 +1 @@ -Subproject commit d6831651250e8bf6e8bfc33ed42728fac7b05c57 +Subproject commit e699ce661ed441f576f9f705e2437e8bb30e6501 From 0c11b1c4c21a1eb10ae2d46fdc1d073c9f6fd2e8 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 22 Feb 2022 21:40:04 -0500 Subject: [PATCH 3/4] Uploaded recitation materials --- content/ta/spring2022/csci2600/_index.md | 2 + .../ta/spring2022/csci2600/recitation06.md | 134 ++++++++++++++++++ 2 files changed, 136 insertions(+) create mode 100644 content/ta/spring2022/csci2600/recitation06.md diff --git a/content/ta/spring2022/csci2600/_index.md b/content/ta/spring2022/csci2600/_index.md index 44185fd..81d6e12 100644 --- a/content/ta/spring2022/csci2600/_index.md +++ b/content/ta/spring2022/csci2600/_index.md @@ -14,3 +14,5 @@ Below are links to the recitations I have given: [Recitation 4](recitation04.pdf) [Recitation 5](recitation05.pdf) + +[Recitation 6: Exam Review](recitation06) diff --git a/content/ta/spring2022/csci2600/recitation06.md b/content/ta/spring2022/csci2600/recitation06.md new file mode 100644 index 0000000..c28db14 --- /dev/null +++ b/content/ta/spring2022/csci2600/recitation06.md @@ -0,0 +1,134 @@ +--- +title: "PSoft Recitation 6: Exam Review" +date: 2022-02-22T21:28:34-04:00 +draft: false +--- + +## Question 1: Forward Reasoning + +Fill in the blanks using forward reasoning. Don't forget to: + +- Carry your variables forward +- Show your work +- Simplify expressions +- State the strongest postcondition + +```java +{x > 1} +y = x; +{ } +x = x + 5; +{ } +y = 2 * y; +{ } +if (z < 12) { + y = -z; + { } +} else { + y = -6 * y; + { } +} +{ } +``` + +## Question 2: Reasoning about loops + +Consider the following Dafny code: + +```csharp +method until_parity(y: int) returns (index: int) + requires y < 0 + ensures index == (1 - y) / 2 || index == (-y / 2) +{ + var p := y; + index := 0; + while (p != 0 && p != 1) + decreases -p + invariant y <= p <= 1 + invariant index == (p - y) / 2 + { + p := p + 2; + index := index + 1; + } +} +``` + +### Q2.1: Loop Invariants + +Prove that `index == (p - y) / 2` using induction + +### Q2.2 Postcondition Verification + +Show that the postcondition is provable from the loop invariant and loop condition. + +### Q2.2 (Bonus) Decrementing Function + +Prove that `-p` is the decrementing function. + +## Question 3: Dafny Invariants + +What is the missing invariant to make this code verify in Dafny? + +```csharp +method copy(in_arr: array) returns (out_arr: array) + ensures in_arr.Length == out_arr.Length + ensures forall j :: 0 <= j < in_arr.Length ==> in_arr[j] == out_arr[j] +{ + out_arr := new int[in_arr.Length]; + var i := 0; + while i < in_arr.Length + invariant 0 <= i <= in_arr.Length + // INVARIANT MISSING HERE + { + out_arr[i] := in_arr[i]; + i := i + 1; + } +} +``` + +## Question 4: Backwards Reasoning + +Fill in the blanks using forward reasoning. Don't forget to: + +- Carry your variables forward +- Show your work +- Simplify expressions +- State the strongest precondition + +```java +{ } +w = 2 * w; +{ } +z = -w; +{ } +y = v + 1; +{ } +x = min(y, z); +{ x < 0 } +``` + + + +## Question 5: Hoare Triple Validity + +Assume the following are true: + +``` +{b} code {y} +a -> b +b -> c +x -> y +y -> z +``` + +For the following Hoare triples state whether or not they are valid. + +If valid, why? If not valid, provide counterexample. + +*Hint: Recall Liskov Principle of Substitutability* + +**Q5.1:** Is `{a} code {y}` valid? + +**Q5.2:** Is `{b} code {x}` valid? + +**Q5.3:** Is `{b} code {z}` valid? \ No newline at end of file From aa76cbefa8bfb23ef460aacc185545657eb6ace7 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 22 Feb 2022 21:40:09 -0500 Subject: [PATCH 4/4] Theme update --- themes/pulp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/themes/pulp b/themes/pulp index e699ce6..c91c410 160000 --- a/themes/pulp +++ b/themes/pulp @@ -1 +1 @@ -Subproject commit e699ce661ed441f576f9f705e2437e8bb30e6501 +Subproject commit c91c4103db37d8a87cb62195e4df60847f9461ae