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 KState 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 KState 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)


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 present some examples that show the need for a more powerful
logic:

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 Postconditions")

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.12)

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 proofchecker 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.24.

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 2529 (MonFri)

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:50am1:40pm
Torben Amtoft