CIS 301. Logical Foundations of Programming

Spring 2001 Syllabus

Location and Time: 122 Nichols Hall, MWF 2:30-3:20 P.M.

Instructor and E-Mail: Michael Huth (huth@cis.ksu.edu)

Office and Phone: 324B Nichols Hall, ph. 532-6350

Office Hours: Mondays 1:30-2:20 P.M. and Wednesdays 03:30-04:20 A.M. in N324B

Text: M. Huth and M. Ryan, Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press. ISBN 0521656028. This text is available in the KSU Union Bookstore. The book is supported by a worldwide web tutor, available at http://www.cis.ksu.edu/~huth/lics/tutor/index.html. The first printing has an errata file at http://www.cis.ksu.edu/~huth/lics/errata.ps.

Course home page: http://www.cis.ksu.edu/~huth/301/home.html

Course objectives: We study the fundamentals of symbolic logic: how to write proofs and how to reason semantically. We use those acquired techniques to check whether models of computer systems satisfy specified properties. We further use them for the design and verification of algorithms.

Topics:

Logic in general (as in "general education"). We study Propositional Logic as the prototypical logic formalism. We ask: `What constitutes valid arguments? How can we demonstrate that certain "inferences" have a valid argument (=proof)?' We utilize a proof calculus and a semantics based on truth tables to address these issues (Chapter 1; 3-4 weeks).

Predicate Logic. Database query languages implement formulas with quantifiers such as "there exists somebody who is older than 30, drives a Honda Accord, and likes Cajun food", or "all taxpayers of Manhattan are Wildcat fans". Polymorphically typed languages and data abstraction also require mechanisms for which Predicate Logic is a well suited mathematical foundation. We study the syntax and semantics of this logic and understand how to evaluate such formulas over their corresponding notion of models. We will also discuss its proof theory and prove important quantifier equivalences. (Chapter 2; 3-4 weeks).

Computation Tree Logic. Protocols, networks, and distributed systems in general cannot be described by code of some deterministic programming language. Such systems exhibit concurrent behavior and they are reactive in the sense that their behavior depends on what the environment can offer (e.g. "Is the printer busy?"). Computation Tree Logic is the framework currently used in verifying properties of concurrent systems. We will study its syntax and semantics, and use those insights to design an automated verification algorithm which takes a description of a system and a formula as input and checks whether that system enjoys that property. We illustrate this with some examples, e.g. elevator systems and a mutual exclusion protocol (Chapter 3; 3-4 weeks).
Program Logic. Given a program P, what can we say about its input/output behavior (without having any run-time information about its variables)? We develop a proof calculus for verifying triples {phi}P{psi}, where phi and psi are statements about the store (e.g. describing the values of variables) before, respectively after, the execution of P, which are programs written in a simple imperative language with if-statements and while-loops (Chapter 4; 2-3 weeks).

Prerequisites: CIS 200. If you have not taken this course, you must see the instructor; the College of Engineering may choose to drop you from this course without notice if you do not have that prerequisite.

Grading and Final Exam: Your entire homework (counting the best of ten assignments only) and all the three in-class and open-book exams (including the Final Exam) count as 25% each towards your final grade. The FINAL EXAM will be held on Friday, May 11, from 04:10 - 06:00 P.M. in Nichols 122. This is an open book exam. Relation of percentages to letter grades:

85% <= A <= 100%, 75% <= B < 85%, 65% <= C < 75%, 55% <= D < 65%, 0% <= F < 55%.

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

Policy statements:

Dropping this course: If you decide not to complete this course, it is your responsibility to drop---there are no ``automatic'' drops due to non-attendance.

Rights, responsibilities and resources --- Sexual and Racial Harassment

"I believe that engineers must not only be the people who know how to do things right, but also those who know the right things to do."

Dr. Joseph Bordogna
Acting Deputy Director
National Science Foundation

One purpose of your education is to help you develop skills, approaches, and abilities that are necessary for effective teamwork, and for your success in your profession and as a citizen. It is important that you understand your rights and responsibilities regarding the University's Sexual and Racial Harassment policies. (full text of the policies can be found on KSU's web site at http://www.ksu.edu/uauc/fhbook/fhxj.html) If you experience any situations, in or out of class, that seem inappropriate or that make you uncomfortable, a list of resources and courses of action to assist you can be found on the College of Engineering web site at http://www.engg.ksu.edu/students/statement-harassment.htm.

University Honor System: Kansas State University has an Undergraduate Honor System based on personal integrity which is presumed to be sufficient assurance that in academic matters one's work is performed honestly and without unauthorized assistance. Undergraduate students, by registration, acknowledge the jurisdiction of the Undergraduate Honor System. The policies and procedures of the Undergraduate Honor System apply to all full and part-time students enrolled in undergraduate courses on-campus, off- campus, and via distance learning. A prominent part of the Honor System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by undergraduate students. The Honor Pledge is implied, whether or not it is stated: "On my honor, as a student, I have neither given nor received unauthorized aid on this academic work." A grade of XF can result from a breach of academic honesty. An XF would be failure of the course with the X on the transcript indicating failure as a result of a breach of academic honesty. For more information, please visit the Honor System web page at: http://www.ksu.edu/honor.

Academic Accommodations for Students with Disabilities: If you have any condition, such as a physical or learning disability, which will make it difficult for you to carry out the work as the instructor has outlined it or which will require academic accommodations, please notify the instructor in the first two weeks of the course.

Notice of copyright for course syllabus and lectures: Copyright 2001 (Michael Huth) as to this syllabus and all lectures. During this course students are prohibited from selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of the professor teaching this course.