CIS 301. Logical Foundations of Programming, Spring 2001.

General course information:

Captain's log: see what was covered when.
Course prerequisites and expected outcomes;
Syllabus;
a worldwide web tutor, based on our textbook;
all assignments for this course;

Teaching Assistant:Your teaching assistant is Varsha Redkar. (Email: varsha@cis.ksu.edu). Her office is in Nichols Hall 19J, where she will conduct office hours on Mondays and Tuesdays at 9:30 - 10:30 A.M.

Ancillary material:

Chapter 1:
- Declarative sentences.
- Pseudo code for a deterministic algorithm that computes an equivalent conjunctive normal form for each formula of propositional logic:
  - computing an implication-free formula;
  - computing a negation normal form;
  - computing a conjunctive normal form;
  - the computationally expensive part: a subroutine that uses the distributivity law.
Chapter 2:
- An example and explanation of the satisfaction relation for predicate logic.
Chapter 3:
- An introduction to SMV: a puzzle;
- A discussion of fixed-point characterizations of those CTL connectives that reason about computation paths of two processes;
- A discussion of our SMV program for the mutual exclusion of two processes;
- Model Checking home page of the School of Computer Science at Carnegie Mellon University; and a manual for the programming language SMV by McMillan.
Chapter 4:
- Sample programs of our core programming language;
- a program for the minimal-sum section of an integer array;
- a four-line program for which nobody (so far) could prove termination!
- probabilistic program correctness and termination.