CIS 301. Captain's Log: Logical Foundations of Programming, Fall 2002.
- August 26: Introduction to course. Syllabus handed out. Why study
this course? Examples of properties in safety critical systems. Mathematical
preliminaries: sets and operations on sets: membership, union, intersection,
difference, cartesian product, subset.
- August 28: Mathematical preliminaries: powerset, relations,
functions. Proofs of simple set-theoretic properties.
- August 30: Examples of relations and functions; Propositional logic;
propositions and propositional connectives; sequents; conjunction introduction
and elimination; double negation introduction and elimination; proofs of some
simple sequents. Homework 1 out.
Read: Begin reading Chapter1 in the texbook.
September 4: Implication introduction and elimination; examples.
September 6: Homework 1 in; Homework 2 out. Disjunction introduction and
elimination; examples. Disjunction elimination in proofs of properties of finite
sets.
September 9: More examples of disjunction elimination. Contradiction and
unary negation introduction, elimination. Examples. Proof of Law of excluded
middle (LEM)
September 11: Provable equivalences, DeMorgan's laws, using LEM in
proofs.
September 13: Assignment 2 in. Graded assignment 1 and solutions to
assignment 1 handed out. Assignment 3 out. BNF of well-formed propositional
formulae, tree representation of formulae, semantics via truth tables.
September 16: Soundness and Completeness of propositional
logic; consequences of soundness and completeness.
September 18: Proving semantic equivalences; conjunctive
normal form (CNF); function IMPL_FREE; negation normal form
September 20: Assignment 3 in. Graded assignment 2 +
solutions out. Assignment 4 out. CNF concluded.
September 23:
The fundamental concept of Mathematical Induction introduced,
and illustrated by a couple of examples.
September 25:
Some more examples of mathematical induction.
We saw that one might have to pick another base than 1.
Also, as illustrated by the fibonacci example,
the induction step establishing M(n+1) might have to exploit
not only M(n) but also M(n-1).
This motivates the variant
Course-of-values induction, described on p.54 in the book.
September 27:
Assignment 4 in. Assignment 5 out.
The data structure "lists".
The append function on lists.
The principle of structural induction,
applied to prove that append x nil = x.
See here for some notes
on the principle of induction.
September 30:
Repeated the principle of mathematical induction,
and repeated that we often need course-of-values induction,
for instance to prove properties about the fibonacci function.
Repeated the principle of structural induction,
and used it to prove that the append function is associative.
Again, the material covered can be found
here.
October 2:
Graded assignment 3 + solutions out.
Recalled the binding rules from p.5.
Took a preview at Assignment 5, exercise 7 on p.84, which
requires induction on formulas (cf. p.55).
Compared with structural induction on lists.
October 4:
Assignment 5 in. Assignment 6 out. Date for Exam I announced:
Wed Oct 16.
Concluded induction, by working through Exercise 1.14 #7, the
case for NNF.
Started on Chapter 2, by motivating the need for encoding of
phrases like "for all", "exists", "is",
"only".
October 7:
Graded assignment 4 out.
Finished Section 2.1, by
motivating the use of function symbols (which return objects)
as well as the use of predicate symbols (which return truth values).
Started on Section 2.2, by giving the syntax of terms
(denoting objects).
October 9:
Solutions for Assignment 4 out.
Covered Sections 2.2.1 and 2.2.2, introducing terms (denoting objects)
and formulas (denoting truth-values). We looked at Example 2.4,
illustrating that in general there are many ways to translate a
declarative sentence in a natural language into a formula in the
predicate logic.
October 11:
Assignment 6 in.
Solution for Assignment 6 online.
Graded Assignment 5 out.
Assignment 7 out.
Discussion about how to assign meaning to formulas:
some are always true, some are always false,
while the truth value of some depend on the interpretation
of the symbols, and the universe of discourse.
(Examples: "Part_of(Manhattan,New York)"
and "for all x exists y: y + x = 0)
Covered Sections 2.2.3 and 2.2.4, motivating the notion
of free and bound variables, the renaming of bound variables,
and how care must be taken when doing substitution
so as to avoid name-capture (the condition
"t is free for x in phi").
October 14:
Solution for Assignment 5 out.
Graded Assignment 6 out.
Went through the questions of Assignment 6, in particular
the ones on induction.
The bogus proof that "all elements in a set are equal",
which is quite interesting in that its "only" flaw
is in the inductive step and "only" when n = 2,
gave rise to much confusion (sorry about that).
Not surprisingly, since so many of our standard notions are
shaken while assuming (wrongly) the induction hypothesis!
Recapitulated Sections 2.2.3 and 2.2.4.
October 16:
1st Exam.
October 18:
Student holiday.
October 21:
Embarked on Sect. 2.3.1.
Taking a cue from the proof rules for conjunction,
an elimination rule and an introduction rule for universal quantification
was presented.
Taking a cue from the proof rules for disjunction,
an introduction rule for existential quantification was presented.
October 23:
Continued Sect. 2.3.1,
completing the elimination/introduction rules for
universal/existential quantification
and illustrating them by means of examples.
(The treatment of equality on pages 110-111 is postponed
until later.)
October 25:
Assignment 8 out. Assignment 7 in.
Graded Exam 1 back, together with solution.
Distribution of grades (max: 25 points):
1 x 21p;
2 x 20p;
5 x 19p;
2 x 18p;
3 x 17p;
1 x 16p;
6 x 15p;
8 x 14p;
2 x 13p;
2 x 12p;
4 x 11p;
4 x 10p;
5 x 9p;
1 x 8p;
1 x 7p;
1 x 6p.
17+ points should be considered good;
13-14 points is acceptable;
being below 13 points is reason for concern.
(A scheme for translating points into grades will not be
made until the final exam.)
We agreed that help sessions would be helpful;
day and time not decided yet.
October 28:
Continued giving examples of the use of
the introduction/elimination
rules for universal and existential quantification,
by proving the "infinite versions" of
(one of) de Morgan's laws (Theorem 2.9, 1(a), p. 121).
Help sessions (tentatively) scheduled for
Wednesdays, 5-6pm in N127,
starting this Wednesday (30th).
October 30:
Used the counterexample on p.120 to illustrate
that one should be very careful to obey the
requirement that nothing can escape a box.
Motivated Theorem 2.9 #2(a)
by looking at the example:
forall x. x^2 > 0 /\ c > 2.
Then proved the theorem,
repairing on the sloppy proof in the book (p.124)
which violates the box requirement :-(
November 1:
Assignment 9 out. Assignment 8 in.
Graded Assignment 7 + solutions out.
Date for Exam II announced: Mon Nov 18.
Started on Section 2.4, introducing the notion of a model
(formally defined on p.131).
November 4:
Recalled the notion of a model (p.131).
Motivated and defined (as on p.134) how to determine whether a model M
satisfies a formula phi with respect to environment l,
written M |=l phi. Doing so, we need the result of evaluating
a term t wrt. a model M and environment l,
to be written [[t]] with superscript M and subscript l
(this function is described only informally in the book,
p.134 l.6-8.)
November 6:
Recalling the definitions of a model M,
and the evaluation functions [[t]]M and [[phi]]M,
we looked at some examples.
Note that we write M |= phi to denote that [[phi]]M = T.
Also note that the interpretation of a predicate P with arity k
can be considered either a subset of A^k or a function from
A^k to {T,F}. These representations are equivalent.
For example, if A is the set of integers and
P is binary and P^M is the subset {(2,3),(4,5)},
then we can also consider P^M a function which returns
T for the values (2,3) and (4,5),
and returns F for all other values.
November 8:
Assignment 10 out. Assignment 9 in.
Graded Assignment 8 + solutions out.
Recalled the definition of M |= phi,
and looked at the derived properties of the relation
not(M |= phi).
Embarked on Section 2.4.2, definining semantic entailment.
Observed that the definition is very similar to the one
from Chap 1 (p.57), replacing "all truth value assignments"
by "all models".
November 11:
Stated Soundness (crucial property) and Completeness (desirable property)
for Predicate logic, cf. p.93.
Important observation (p.129): we need both |- and |=.
It is much easier to establish |- than to establish (not |-);
it is easier to establish (not |=) than to establish |=.
November 13:
Solutions to Assignment 9 out.
Considered the "=" predicate, with proof rules given on p.110-111.
Embarked on program verification (start reading Chapter 4!)
We saw an example (square root) of how to
convert an informal and ambiguous specification
into a logical formula. In the rest of the chapter,
we assume that this (highly non-trivial!) conversion already
has taken place,
and focus on how to prove that a given program satisfies
its specification.
November 15:
Graded Assignment 9 out.
Mentioned which type of exam questions
would be most likely.
Recalled induction (mathematical as well
as structural).
November 18:
2nd Exam.
November 20:
Final exam scheduled for Wed Dec 18, 11:50-1:40 in N122.
Please report conflicting schedules ASAP.
Some more
previous exam sets
are now available.
Continued Chapter 4. Discussed a 3-step framework for software
verication (p.218). The focus of the rest of this class is step 3:
to prove that a given program P satisfies a given formula phi.
Introduced our language (p.220-221),
which is sequential and transformational (cf. p.216).
Showed an example program (p.222) computing the factorial function.
November 22:
Assignment 11 out. Assignment 10 in.
Again looked at program for factorial (p.222).
Argued the need for logical variables (p.229) to express that
program variables don't change.
Presented an invariant for the loop,
and showed (i) that the invariant holds initially (base case);
(ii) that the invariant is preserved by each loop iteration (inductive case).
Therefore, the invariant holds after any number of iterations.
We also saw that the invariant, together with the negation
of the guard, implies the desired postcondition.
Finally, we saw that to ensure termination some notion
of "progress" is needed.
November 25:
Graded Exam II back, together with solutions.
Presented proof rule for C1;C2 (p.231).
November 27:
Student holiday (Thanksgiving)
November 29:
Holiday (Thanksgiving)
December 2:
Introduced the distinction between total correctness (the program terminates
with a correct result) and partial correctness (if the program terminates,
the result is correct). Continued the covering of Fig. 4.1 (p.231),
explaining the rules Composition (mentioned already last time),
Assignment, Partial-while, Implied.
December 4:
Graded Assignment 10 + solutions out.
Completed the proof rules from Fig. 4.1 (p.231).
A convenient way to represent such proofs is the
"tableaux" method (p.236-237)
which we used for showing correctness of the factorial
program (Example 4.12,p.249). Read until p.252.
December 6:
Assignment 11 in. Illustrated, by using the specification of square root
(cf. Nov 13) how one can develop a program
together with its proof.
An important trick is to decompose the desired postcondition
into two components which can then serve as loop invariant
and (negation of) loop guard.
December 9:
Last lecture. Graded Assignment 11 + solutions out.
Finished how to construct a program together with its proof
(not an exam question). Wrapped up the course.
December 11:
"Early" final exam (for those of you who have asked for a such),
10:30 - 11:20 am in N122
December 17:
Help session, 5-6pm in N127.
December 18: (Wednesday)
Final exam, 11:50 am - 1:10 pm in N122
Torben Amtoft