Organize lectures a bit better

Author: tchajed

src/syntax1.dfy renamed to src/lec1_logic.dfy

@@ -50,9 +50,9 @@ function IsLarge(x: int): bool {
   x > 1000
 }
 
-// New syntax (predicate): `predicate` is a shorthand for a function that returns a boolean.
-// Functions that return a boolean are extremely common in verification since
-// they express logical predicates, hence the special syntax.
+// New feature (predicate): `predicate` is a shorthand for a function that
+// returns a boolean.  Functions that return a boolean are extremely common in
+// verification since they express logical predicates, hence the special syntax.
 predicate IsSmall(x: int) {
   !IsLarge(x)
 }
@@ -140,7 +140,7 @@ lemma ForallAssertionExamples()
 lemma AbsLargerForAll()
   ensures forall x: int :: abs(x) >= x
 {
-  // New syntax (forall statement): a _forall statement_ allows us to help Dafny with a proof of
+  // New feature (forall statement): a _forall statement_ allows us to help Dafny with a proof of
   // `forall x :: ...` by talking about an individual `x` */
   forall x: int
     ensures abs(x) >= x

src/lec2_sequences.dfy

@@ -0,0 +1,84 @@
+/* More interesting data to reason about: sequences. */
+
+/* In order to write proofs about interesting systems and protocols, we first
+need some way of modeling the state of those systems and protocols. We'll
+explore Dafy's built-in sequence type as well as algebraic data types, its core
+way of creating user-defined types. */
+
+/*** Sequences ***/
+
+/* These data types are very similar to data structures, but will be purely
+ * mathematical. We'll start with the sequence type `seq<T>`. The `T` in angle
+ * brackets is a _type parameter_, needed because sequences can hold values of
+ * any type. A sequence is related to data structures you're familiar with like
+ * linked lists or arrays/vectors (the terminology depends on the programming
+ * language). A sequence is the mathematical essence of the state of a
+ * list/vector/array without the implementation details.
+ */
+
+lemma SequenceOperations()
+{
+  // var is a (mutable) local variable, defined within a lemma
+  var s: seq<int> := [3, 1, 2];
+  // sequences can be indexed, starting at 1
+  assert s[1] == 1;
+  // we can extract a subsequence
+  assert s[1..2] == [1];
+  // we can re-assign the sequence and update one element using the `s[i := v]` syntax.
+  s := s[2 := 3];
+  assert s[0] == s[2] == 3;
+  // `|s|` is the sequence's length
+  assert |s| == 3;
+  // we can append two sequences
+  s := s + [7, 12];
+  assert |s| == 5;
+  assert s == [3, 1, 3, 7, 12];
+}
+
+/* Below we give some lemmas illustrating sequence operations. */
+
+function SeqGet(s: seq<int>, i: nat): int
+  // New feature (function preconditions): functions can have _requires_
+  // clauses, also called _preconditions_. Dafny will statically check  that the
+  // preconditions hold (in the same way as assertions) wherever a call to the
+  // function appears.
+  //
+  // This particular precondition requires that the index is in-bounds. The fact
+  // that `i` is of type `nat` already assures that it is non-negative.
+  requires i < |s|
+{
+  s[i]
+}
+
+function SeqUpdate(s: seq<int>, i: nat, n: int): seq<int>
+  requires i < |s|
+{
+  s[i := n]
+}
+
+lemma CheckedPreconditions(s: seq<int>, i: nat)
+  // Dafny does not allow even stating this because it tries to index a //
+  // sequence without a proof that the index is in-bounds, one of the preconditions
+  // for sequence indexing.
+  //
+  // We'd get the same error in an ensures clause or function definition.
+  requires s[i] > 0 // error: index out of range
+{}
+
+lemma CheckedFunctionPreconditions(s: seq<int>, i: nat)
+  // almost same as above, but notice that the error specifically points to the
+  // `SeqGet` precondition
+  requires SeqGet(s, i) > 0 // error: function precondition might not hold
+{}
+
+lemma SequenceAppendFact(s1: seq<int>, s2: seq<int>)
+  // New feature (forall where clause): notice the new pipe symbol after the `i`.
+  // The general syntax is of the form `forall x | p(x) :: q(x)`; it means the
+  // same thing as `forall x :: p(x) ==> q(x)` but can be easier to read. You
+  // might read this as "for all x where p(x), q(x)".
+  //
+  // We're also leaving off the type of `i` because Dafny can infer that it's an `int`.
+  ensures forall i | |s1| <= i < |s1| + |s2| :: (s1 + s2)[i] == s2[i - |s1|]
+{
+  // goes through without any extra proof
+}

src/syntax2.dfy renamed to src/lec3_algebraic_datatypes.dfy

@@ -1,101 +1,16 @@
-/* More interesting data to reason about: sequences. */
-
-/* Outline:
-- sequences
-- algebraic data types (user-defined data)
-*/
-
-/* In order to write proofs about interesting systems and protocols, we first
-need some way of modeling the state of those systems and protocols. We'll
-explore Dafy's built-in sequence type as well as algebraic data types, its core
-way of creating user-defined types. */
-
-/*** Sequences ***/
-
-/* These data types are very similar to data structures, but will be purely
- * mathematical. We'll start with the sequence type `seq<T>`. The `T` in angle
- * brackets is a _type parameter_, needed because sequences can hold values of
- * any type. A sequence is related to data structures you're familiar with like
- * linked lists or arrays/vectors (the terminology depends on the programming
- * language). A sequence is the mathematical essence of the state of a
- * list/vector/array without the implementation details.
- */
-
-lemma SequenceOperations()
-{
-  // var is a (mutable) local variable, defined within a lemma
-  var s: seq<int> := [3, 1, 2];
-  // sequences can be indexed, starting at 1
-  assert s[1] == 1;
-  // we can extract a subsequence
-  assert s[1..2] == [1];
-  // we can re-assign the sequence and update one element using the `s[i := v]` syntax.
-  s := s[2 := 3];
-  assert s[0] == s[2] == 3;
-  // `|s|` is the sequence's length
-  assert |s| == 3;
-  // we can append two sequences
-  s := s + [7, 12];
-  assert |s| == 5;
-  assert s == [3, 1, 3, 7, 12];
-}
-
-/* Below we give some lemmas illustrating sequence operations. */
-
-function SeqGet(s: seq<int>, i: nat): int
-  // New feature (function preconditions): functions can have _requires_
-  // clauses, also called _preconditions_. Dafny will statically check  that the
-  // preconditions hold (in the same way as assertions) wherever a call to the
-  // function appears.
-  //
-  // This particular precondition requires that the index is in-bounds. The fact
-  // that `i` is of type `nat` already assures that it is non-negative.
-  requires i < |s|
-{
-  s[i]
-}
-
-function SeqUpdate(s: seq<int>, i: nat, n: int): seq<int>
-  requires i < |s|
-{
-  s[i := n]
-}
-
-lemma CheckedPreconditions(s: seq<int>, i: nat)
-  // Dafny does not allow even stating this because it tries to index a //
-  // sequence without a proof that the index is in-bounds, one of the preconditions
-  // for sequence indexing.
-  //
-  // We'd get the same error in an ensures clause or function definition.
-  requires s[i] > 0 // error: index out of range
-{}
-
-lemma CheckedFunctionPreconditions(s: seq<int>, i: nat)
-  // almost same as above, but notice that the error specifically points to the
-  // `SeqGet` precondition
-  requires SeqGet(s, i) > 0 // error: function precondition might not hold
-{}
-
-lemma SequenceAppendFact(s1: seq<int>, s2: seq<int>)
-  // New syntax (forall where clause): notice the new pipe symbol after the `i`.
-  // The general syntax is of the form `forall x | p(x) :: q(x)`; it means the
-  // same thing as `forall x :: p(x) ==> q(x)` but can be easier to read. You
-  // might read this as "for all x where p(x), q(x)".
-  //
-  // We're also leaving off the type of `i` because Dafny can infer that it's an `int`.
-  ensures forall i | |s1| <= i < |s1| + |s2| :: (s1 + s2)[i] == s2[i - |s1|]
-{
-  // goes through without any extra proof
-}
-
+/* More interesting data to reason about: algebraic data types. */
 
 /*** Algebraic data types ***/
 
 /* Sequences are powerful and all, but eventually you'll want to define new data
-types. For that Dafny has algebraic data types which capture "products"
-(struct-like types) and "sums" (tagged unions). While we're explaining algebraic
-data types we'll take a short break from lemmas/proofs and just explain this bit
-of functional programming. */
+ * types. For that Dafny has algebraic data types which capture "products"
+ * (struct-like types) and "sums" (tagged unions). These are often abbreviated to
+ * "ADTs" (not to be confused with "abstract data types" which are a totally
+ * different concept related to object-oriented programming; we won't generally
+ * use that term). Algebraic data types are also used for programming (as opposed
+ * to in the course where we'll only see them used for mathematical models), so
+ * we'll take a short break and first explain them in the context of functions
+ * before seeing them used in lemmas and assertions. */
 
 /* Let's start with a struct that has two fields, x and y: */
 datatype Point = PointCtor(x: int, y: int)
@@ -174,19 +89,25 @@ datatype CoffeeRecipe =
     // a very incomplete list :)
 
 // How much milk will be in my coffee drink?
+//
+// (If you don't know much about coffee, that's okay! Take this as a
+// specification for what these drinks are, at least as far as milk is
+// concerned.)
 function MilkOz(coffee: CoffeeRecipe): nat {
   match coffee {
-    // New feature: we can put an underscore for fields that aren't needed in
-    // some "match arm". We can also name a field and refer to it on the right side
-    // (notice that this name also doesn't have to match the name in the datatype).
+    // New feature (ignore patterns): we can put an underscore for fields that
+    // aren't needed in some "match arm". We can also name a field and refer to
+    // it on the right side (notice that this name also doesn't have to match
+    // the name in the datatype).
     case Drip(_, milk) => if milk then 1 else 0
     case Espresso(_) => 0
     // standard-sized latte
     case Latte(_) => 8
   }
 }
 
-/* Below we illustrate some reasoning about data types. */
+/* Now that we've seen algebraic datatypes in functions, let's start using them
+ * in lemmas and assertions. */
 
 lemma VariantsDiffer() {
   assert Cytosine != Guanine;

src/syntax3.dfy renamed to src/lec4_advanced.dfy

@@ -3,7 +3,7 @@
 /* Outline:
 - Opacity and revealing
 - Recursive functions and lemmas
-- assign-such-that
+- Assign-such-that
 */
 
 
@@ -158,7 +158,7 @@ lemma PreviousFromC(s: State, s': State)
   requires Next(s, s') && s' == C
   ensures s == B || s == C
 {
-  // New syntax (assign such that): we can assign a variable using the syntax
+  // New feature (assign such that): we can assign a variable using the syntax
   // `var x:T :| p(x)` to get a (non-deterministic) value of type `T` that
   // satisfies `p(x)`. Dafny will first check that at least one such value
   // exists. As usual for `var` declarations the type `T` is optional if it can