Unit 0: Admin & Proof Techniques

This is an archived version of this module from Fall 2022.
Click here for the current iteration.

This unit covers:

• organization of the module (administrative part)
• strategies for mathematical proofs
• mathematical induction
• loop invariants

Learning outcomes

1. Know logical proof strategies for proving implications, set inclusions, set equality, and quantified statements.
2. Be able to use mathematical induction in simple proofs.
3. Know techniques for proving termination and correctness of procedures.

Material

• slides on administrativa

• slides on proof techniques

• lecture notes on administrativa

• lecture notes on proof techniques

• Video 0-1 · transcript (2022-09-26, 34:52): Welcome, teaching mode, overview, assessment, Campuswire, prior knowledge survey
  
  Chapters

  4:49 Communication and feedback
  7:11 Assessment structure
  13:54 Teaching methods and goals
  22:50 Campuswire and participation
  31:12 Scientific philosophy and survey
  
• Video 0-2 · transcript (2022-09-28, 32:13): §0.1 Random shuffle motivation, logical statements
  
  Chapters

  1:33 Array shuffling algorithm
  7:27 Analyzing shuffle correctness
  11:43 Identifying algorithm flaws
  16:46 Formal proofs and systems
  23:39 Logical statements and terms
  29:21 Logical implications exercise
  
• Video 0-3 · transcript (2022-09-28, 13:47): §0.2 Proof templates, random shuffle motivation
  
  Chapters

  0:09 Implications
  10:06 Clicker Question
  12:33 Set Inclusion and Equality
  
• Video 0-4 · transcript (2022-09-28, 29:29): §0.3 Mathematical induction, Towers of Hanoi
  
  Chapters

  1:48 Existential and Universal Quantifiers Existential
  4:08 The Limits of a Function
  5:33 The Epsilon Delta Criterion
  6:02 Nested Quantifiers
  6:54 Limits of Continuous Functions
  9:05 Proof by Contradiction
  16:52 Question 50
  25:03 Inductive Hypothesis
  
• Video 0-5 · transcript (2022-09-28, 12:17): §0.4 Correctness proofs (part 1)
  
  Chapters

  0:10 Formal verification
  2:23 Proving termination
  8:18 Loop invariant - Example
  11:18 Loop invariants
  
• Video 0-6 · transcript (2022-10-03, 17:57): §0.4 Correctness proofs (part 2): example
  

Further reading and sources

A much more in-depth introduction to proof techniques, with many examples and exercises can be found, e.g., here:

• Velleman: How to Prove It, 2nd ed. (2006), Cambridge University Press

The loop invariants are the center piece of Hoare Logic for program verification. More background on Hoare Logic is given for example here:

• Gordon: Lecture Notes on Hoare Logic

---

Syllabus  ⋅  Unit 1