From 0c11b1c4c21a1eb10ae2d46fdc1d073c9f6fd2e8 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <rozekbrandon@gmail.com>
Date: Tue, 22 Feb 2022 21:40:04 -0500
Subject: [PATCH] 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<int>) returns (out_arr: array<int>)
+    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