Captain's Log: CIS 301, Logical Foundations Of Programming, Fall 2013

1: Aug 26 (Mon)

Introduction to course:

go through syllabus
motivate why logic provides a foundation for software writing
(using the slide set "Intro.pdf", uploaded on K-State Online, that summarizes the introduction of the textbook.)

2: Aug 28 (Wed)

Introduce circuits and truth tables (using the slide set "Circuits.pdf", uploaded on K-State Online, that summarizes Chapter 0 of the textbook.)

3: Aug 30 (Fri)

Finish the chapter on circuits and truth tables, introducing the → connective and the NAND/NOR connectives.
See how algebraic reasoning helps us to predict the behavior of a program, as mentioned in Chapter 1 of the textbook,
but show that naive algebraic reasoning will not work for general programs.

Sep 2 (Mon)

University Holiday (Labor Day)

4: Sep 4 (Wed)

Start on the basics of general programming logic (Chapter 2 of the textbook); we cover the forwards rule for assignments (Section 2.1.1).

5: Sep 6 (Fri)

Continue the slides that summarize Chapter 2 of the textbook, giving the basics of programming logic; we cover

the backwards rule for assignments (Section 2.1.2), and
the forwards rule for conditionals (Section 2.2).

Discuss Assignment 1, due tonight, with students doing selected exercises on the board.

6: Sep 9 (Mon)

Finish the slides that summarize Chapter 2 of the textbook:

recall the forwards rule for conditionals
introduce the backwards rule for conditionals (Section 2.2.1).

Discuss model solutions for Assignment 1.

7: Sep 11 (Wed)

We extend the program logic to functions, as in Section 3.1 of the textbook:

we motivate the design by contract paradigm
we develop a contract for "integer square root"
we write proof rules for function calls.

8: Sep 13 (Fri)

We reason about procedures which modify global variables, cf. Section 3.2.1 of the textbook
Discuss Assignment 2, due tonight, with students doing selected exercises on the board.

9: Sep 16 (Mon)

Discuss model solutions for Assignment 2
Reason about global-variable invariants (Section 3.2.2 of the textbook)

10: Sep 18 (Wed)

Illustrate how functions can be used to build other functions (Section 3.3), in particular:

Introduce recursive functions (Section 3.3.1) and sketch how they are implemented.

Discuss Assignment 3, due Friday night, with students doing selected exercises on the board.

Sep 20 (Fri)

Class canceled.
Assignment 3 due tonight.

11: Sep 23 (Mon)

Discuss model solutions for Assignment 3
Prove the correctness of the recursive factorial function.
Introduce loops and loop invariants, as done in Section 4.1 of the textbook.

12: Sep 25 (Wed)

Continue loop invariants:

Discuss partial vs. total correctness, cf. Section 4.4 of the textbook
Discuss how to come up with loop invariants, cf. Section 4.2 of the textbook (we use the example from Section 4.2.1).

Discuss the upcoming Assignment 4.

13: Sep 27 (Fri)

Give one more example (Section 4.2.4 in textbook) of how to find invariants.
Motivate why we would like to write a program together with its proof.
Discuss Assignment 4, due tonight, with students doing selected exercises (Q1.Q2.Q3) on the board.

14: Sep 30 (Mon)

Prepare for Exam 1, discussing

Exam 1 from Fall 2011
Exam 1 from Fall 2012
model solutions for Assignment 4 (Q4 and Q3)

15: Oct 2 (Wed)

Exam 1

16: Oct 4 (Fri)

We address how to write a program together with its proof, illustrated by

word reversal (Section 4.2.5)
integer square root

17: Oct 7 (Mon)

We continue developing programs together with their proofs:

a fast program for integer square root (based on binary search)
Euclid's algorithm for finding greatest common divisor.

Briefly discuss Questions 1 and 2 in the upcoming Assignment 5.

18: Oct 9 (Wed)

we would like universal quantifiers in our assertion language, cf. Section 4.2.6 and Section 4.3.
we would like tools for systematic reasoning about boolean operators like "or" and "not", cf. Section 4.2.7.

Discuss Questions 2 and 3 in the upcoming Assignment 5.
We embark on using the Dafny system, going through the tutorial (stopping at "Pre- and Post-conditions")

19: Oct 11 (Fri)

Continue going through the Dafny tutorial, covering Functions and Loop Invariants
Discuss Assignment 5, due tonight, with students doing parts of Questions 1 and 3.

20: Oct 14 (Mon)

Discuss model solutions for Assignment 5.
Hand back, and discuss, graded Exam 1.
Introduce Assignment 6 (to be done on your own!)

21: Oct 16 (Wed)

Embark on Chapter 5 of the textbook, on propositional logic.

propositions and sequents (Sections 5.1-2)
inference rules for conjunction (Section 5.3) and disjunction (Section 5.4)
use the inference rules to prove one direction of one of the distributive laws.

Finish (for now) the Dafny tutorial, thus preparing for the upcoming Assignment 6.

22: Oct 18 (Fri)

Continue Propositional Logic:

Introduce the natural deduction proof-checker to be used frequently for the rest of the course
Do some more of the distributive laws, on the board and using the checker

Discuss Assignment 6, due tonight, with students doing selected exercises on the board.

23: Oct 21 (Mon)

Present inference rules for:

implication (Section 5.5)
negation and contradiction (Section 5.6).

24: Oct 23 (Wed)

Give a classical proof for the famous result that the square root of 2 is not rational.
Do some example formal proofs, on the board and using the checker.
Motivate why ~~P may be considered different from P, cf Section 5.9.2-4.
Introduce proof by contradiction (PbC) which allows P to be derived from ~~P and which does not follow from the rules we have seen so far.

25: Oct 25 (Fri)

For each of the two DeMorgan's laws, present a proof for one direction.
Discuss Assignment 7, due tonight, with students doing selected exercises on the board.

26: Oct 28 (Mon)

Present a couple of proofs that show the power of PbC (Section 5.6.2)
Observe that the proof checker allows some useful shortcuts, such as "lem" (law of excluded middle)
Mention that our proof system is sound and complete (Section 5.9.1)
Introduce Conjunctive Normal Form (CNF, Section 5.8)

27: Oct 30 (Wed)

Introduce the Resolution method (Section 5.8.1):
- it is based on the "proof by contradiction" principle
- it often allows an easy path towards a proof.
Start on Chapter 6 of the textbook, introducing the universal quantifier (Section 6.1):
- Give the elimination and introduction proof rules
- Work out some example proofs (also using the proof checker)

28: Nov 1 (Fri)

Wrap up the universal quantifier (Section 6.1):

Do more proofs
Give an example where we cannot write a proof, because the sequent is invalid (as seen by counterexample)
Give alternative introduction rules, in particular induction.

Discuss model solutions for Assignment 7.
Discuss Assignment 8, due tonight, with students doing selected exercises on the board.

29: Nov 4 (Mon)

Prepare for Exam 2, discussing

Exam 2 from Fall 2011
Exam 2 from Fall 2012
model solutions for Assignment 8

See how to use the universal quantifier to reason about array programs.

30: Nov 6 (Wed)

Exam 2

31: Nov 8 (Fri)

Introduce the existential quantifier (Section 6.2):

illustrate its use
present its proof rules
construct some example proofs

32: Nov 11 (Mon)

Continue the existential quantifier, including some uses in program logic.
State important equivalences involving the quantifiers (Section 6.5).
Observe that for some pairs of quite similar formulae, one is strictly stronger than the other.
Example: ∃x ∀y P(x,y) and ∀y ∃x P(x,y).
Discuss how to translate numeric claims into predicate logic.

33: Nov 13 (Wed)

Discuss soundness and completeness for predicate logic (Section 6.8).
Give an axiomatization of arithmetic; a key rule is induction (cf. Section 4.5 of textbook).
Mention that no proof system can fully capture arithmetic truth (Section 6.8).

34: Nov 15 (Fri)

Hand back, and discuss, graded Exam 2.
Discuss Assignment 9, due tonight, with students doing selected exercises on the board.

35: Nov 18 (Mon)

Start reasoning about arrays:

give the proof rule for array assignment (Section 6.3)
illustrate by a simple example, on the board and in Dafny
Develop a program for binary search (cf. Section 6.4.2), and prove its correctness manually.

36: Nov 20 (Wed)

See that the binary search program we developed last time can be verified in Dafny.
Embark on a larger case study, Selection Sort (cf. Section 6.4.1):
- motivate the approach (comparing to Insertion Sort)
- develop the implementation while sketching a correctness proof

37: Nov 22 (Fri)

Further discuss how to translate certain English sentences:

donkey sentences
Russell's paradox.

Discuss model solutions for Assignment 9.
Discuss Assignment 10, due tonight.

Nov 25-29 (Mon-Fri)

Thanksgiving holiday

38: Dec 2 (Mon)

Embark on Prolog (Chapter 7 of the textbook):

How to get rid of existential quantifers: Skolem functions (Section 6.6)
How to extend the resolution method to predicate logic (Section 6.7)
How to query a database (Section 7.1)
Introduce Horn clauses (beginning of Section 7.2)

39: Dec 4 (Wed)

Guest lecture by Simon Ou on the MulVAL Project.

40: Dec 6 (Fri)

Continue Prolog:

Show how Prolog implements the resolution method
- using backwards chaining and backtracking, as described in Section 7.2
Introduce function symbols (Section 7.3.0)
Introduce lists, a key data structure (Section 7.3.1)

Briefly discuss the upcoming Assignment 11.

41: Dec 9 (Mon)

Continue Prolog:

elaborate on the list data structure
discuss various call patterns for the membership predicate
see a succinct solution to the combinatorial problem of giving exact change
(cf. Section 7.4, where the query and the solution is somewhat different).

Discuss model solutions for Assignment 10.
Further discuss the upcoming Assignment 11.

42: Dec 11 (Wed)

Use Prolog to succinctly solve a complex problem: sorting a list (Section 7.5).
Work on Assignment 11, due tonight.

43: Dec 13 (Fri)

General review session.

Discuss model solutions for Assignment 11.
Go through solutions to the final exam for Fall 2011.
Go through solutions to the final exam for Fall 2012.

Dec 20 (Fri)

Final exam, 11:50am-1:40pm

Torben Amtoft