CIS 301. Logical Foundations of Programming

Fall 2003 Syllabus

Course Home page

Where, When, Who?

Location and Time:

122 Nichols Hall, MWF 10:30-11:20 A.M.

Instructor:

Torben Amtoft tamtoft@cis.ksu.edu
Office and Phone: 216 Nichols Hall, ph. 532-6350
Home page URL: www.cis.ksu.edu/~tamtoft
Review sessions: Tuesdays 5:00pm-6:00pm, in N127.
Office Hours: Mondays and Wednesdays 3:15pm-4:30pm, and by appointment.
He will try to respond to emails at least within the next workday, but in most cases much sooner.

Teaching Assistant:

Vivek Subramaniam viveks@ksu.edu
Home page URL: www.cis.ksu.edu/~viveks/home.html
Office Hours: Fridays from 2:00pm to 4:30pm, and by appointment, in N19G.

Text

Course objectives

Prerequisites

Topics:

Propositional Logic

Arguments and their validity. How to do rigorous proofs, that is, how to demonstrate that certain "inferences" are valid. We utilize a proof calculus and a semantics based on truth tables to address these issues.
(selected parts of Chapters 1-8; 4-5 weeks.)

First-Order Logic

Database query languages often allow queries like "find all students who are sophomores and have tried out for the varsity rowing team" or "find someone who is a resident of Manhattan and is older than 30 and drives a Honda Accord, and likes Italian food"; such queries manipulate formulae written in first-order logic. We study the syntax and semantics of this logic and understand how to evaluate (i.e., give meanings to) sentences. We will also discuss its proof theory and prove important quantifier equivalences.
(selected parts of Chapters 9-13; 4-5 weeks.)

Mathematical Induction and Program Logic

Given a program P, what can we say about its input/output behavior (without having any information about which values its variables will assume at run-time)? 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. We treat a simple imperative language with if-statements and while-loops. The bulk of program verification is to find invariants for while loops; such an invariant should have the property that (i) it holds after zero iterations of the loop; (ii) if it holds after n iterations, it also holds after n+1 iterations. This is a special case of the induction principle, ubiquitous in mathematics and computer science.
(Chapter 16 + additional material; 4-5 weeks.)

Grading and Exams

Homework

There will be approximately 11 homework assignments during the semester. There are two types of homework:

• those done with pencil and paper, to be graded manually by the TA and returned to you the following week;
• those submitted electronically to the Grade Grinder, from which you will receive automated feedback.

Late assignments will not be accepted except for medical or family emergencies.

Exams

In addition to the final, there will be two more tests during the semester. All tests are open-book.

Grades

Each of the three tests counts 25%, with the homework making up for the last 25%. There is no fixed scheme for the conversion of numerical scores to actual grades, but it is fair to say that if your total is less than 50% you shouldn't expect to pass (that is, get a C or better). On the other hand, even if your total score should end up being slightly below the borderline between two grades, a good final exam may have created a positive last impression that lands you above the line!

Grievances

If you think that the instructor or the TA has made an oversight when grading your test or your homework, you are of course very welcome to ask for clarification. But complaints about judgment calls, like how much credit to give for a partially correct solution, are not encouraged---it is like arguing balls and strikes. In particular this holds for homeworks (since each assignment carries so little weight towards the final grade).

General guidelines:

Please note that this course is time consuming. Practicing all exercises in each chapter of the text, whether or not assigned as homework, will be critical to assuring a good performance in the exams. If you have many other commitments (e.g., work, heavy course load, busy social life, etc.) it may be advisable to take this course in another semester.

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.

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.

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

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. The proper attitude might be summarized Do to others what you want others to do to you or Do not do to others what you do not want others to do to you (food for thought: are those two statements equivalent?)

For particular examples of unwanted conduct, see the University's Sexual and Racial Harassment policies. 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 at http://www.engg.ksu.edu/students/statement-harassment.htm.

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.

Acknowledgment and notice of copyright for course syllabus and lectures

This syllabus is adapted from the one taught by Michael Huth and later modified by Anindya Banerjee. 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.