diff --git a/docs/120/03-datatypes.html b/docs/120/03-datatypes.html index a6f51efdf..192884cde 100644 --- a/docs/120/03-datatypes.html +++ b/docs/120/03-datatypes.html @@ -213,9 +213,10 @@ -
-

Data Types

+
+

Data Types


+

Example: Lists


@@ -263,10 +264,10 @@

Specifying the size of a List

(:::) :: x:a -> xs:List a -> {v:List a|size v = 1 + size xs}
-
-
-

Using Measures

+
+

Using Measures


+

Exercise: Partial Functions


@@ -372,12 +373,12 @@

Exercise: average

Q: What is a safe input type for average'?


-
-
-

Refining Data Types

+
+

Refining Data Types



    Make illegal states unrepresentable


+

Example: Year is 12 Months


@@ -565,7 +566,6 @@

Recap

  • Low-level Memory
  • -
    diff --git a/docs/120/04-case-study-insertsort.html b/docs/120/04-case-study-insertsort.html index bc5ad93ab..011d6f6ed 100644 --- a/docs/120/04-case-study-insertsort.html +++ b/docs/120/04-case-study-insertsort.html @@ -215,9 +215,10 @@


    -
    -

    Case Study: Insertion Sort

    +
    +

    Case Study: Insertion Sort


    +

    Insertion Sort


    @@ -242,10 +243,10 @@

    Goal: Verified Insertion Sort

    Has the same elements as the input,

    Is in increasing order.

    -
    -
    -

    Property 1: Size

    +
    +

    Property 1: Size


    +

    Exercise: insert


    @@ -271,10 +272,10 @@

    Exercise: insert


    -
    -
    -

    Property 2: Elements

    +
    +

    Property 2: Elements


    +

    Permutation


    @@ -341,14 +342,14 @@

    Exercise: Verifying Permutation

    Q: Can you fix the type for insertE so sortE verifies?

    -
    -
    -

    Property 3: Order

    +
    +

    Property 3: Order


    Yes, yes, but does sort actually sort ?


    How to specify ordered lists ?


    +

    Recall: Refined Data Types


    @@ -540,9 +541,9 @@

    Exercise: Insertion Sort

    +
    +

    Multiple Measures

    -
    -

    Multiple Measures

    Different Measures for List


    @@ -602,7 +603,6 @@

    Continue


    Continue: [Part II : Proofs]

    -
    diff --git a/docs/120/05-termination.html b/docs/120/05-termination.html index d57b359b7..d6d009326 100644 --- a/docs/120/05-termination.html +++ b/docs/120/05-termination.html @@ -193,9 +193,10 @@ -
    -

    Termination Checking

    +
    +

    Termination Checking


    +

    Why termination Checking?



    @@ -539,7 +540,6 @@

    What properties can be expressed in the logic?

    Next: Any Terminating Haskell Function

    Refinement Reflection

    -
    diff --git a/docs/120/06-reflection.html b/docs/120/06-reflection.html index a4a7cfead..7e3d177e0 100644 --- a/docs/120/06-reflection.html +++ b/docs/120/06-reflection.html @@ -205,9 +205,10 @@






    -
    -

    Refinement Reflection

    +
    +

    Refinement Reflection



    Allow terminating Haskell functions in refinements!

    +

    Theorems about Haskell functions


    @@ -585,7 +586,6 @@

    Recap


    Next: Structural Induction: Program Properties about data types!

    -
    diff --git a/docs/120/07-structural-induction.html b/docs/120/07-structural-induction.html index d12f48f25..1b398d47c 100644 --- a/docs/120/07-structural-induction.html +++ b/docs/120/07-structural-induction.html @@ -204,9 +204,10 @@






    -
    -

    Structural Induction

    +
    +

    Structural Induction



    How we express and prove properties on data types?

    +

    The list data type


    A user defined list,

    @@ -642,7 +643,6 @@

    Monoid Laws: Associativity

    &&& associativity xs f g -
    diff --git a/docs/120/08-case-study-map-reduce.html b/docs/120/08-case-study-map-reduce.html index 73b5a7eb1..640e7e0b9 100644 --- a/docs/120/08-case-study-map-reduce.html +++ b/docs/120/08-case-study-map-reduce.html @@ -209,12 +209,13 @@ -
    -

    Case Study: MapReduce

    +
    +

    Case Study: MapReduce


    Chunk input, map operation (in parallel), and reduce the results.

    +

    MapReduce "Library"


    Haskell definition and reflection

    @@ -626,7 +627,6 @@

    List Manipulation

    (C x xs) ++ ys = x `C` (xs ++ ys) -