CIS 301. Logical Foundations of Programming

Fall 2007 Syllabus


Course Home page

http://people.cis.ksu.edu/~tamtoft/CIS301/Fall07/index.html. The Captain's log gives up-to-date information about what has been covered so far and what is expected to happen in the near future.

We shall also use K-State Online, primarily to report grades but also for online quizzes etc. You must be enrolled in the course to access K-State Online.

There is a mailing list with the address cis301-l HAT listserv dot ksu dot edu for questions and issues of general interest (note that attachments to mails are not allowed).

Where, When, Who?

Classes

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

In addition, there are optional review sessions, with you setting the agenda, also in N122, on Wednesdays from 5:00pm (until 5:45pm, or until there are no more students or questions, whatever happens sooner).

Instructor

Torben Amtoft
Email
tamtoft HAT ksu dot edu
Home page URL
http://people.cis.ksu.edu/~tamtoft
Office and Phone
219C Nichols Hall, ph. 532-7917
Office Hours
Monday 3-4pm and Wednesday 3-4pm, and by appointment.
He will try to respond to emails at least within the next workday, but in most cases much sooner.

Teaching assistant

Michael Marlen
Email
msm6666 HAT ksu dot edu
Office
Nichols 19
Office Hours
Tuesday 3-4pm and Thursday 3-4pm, and by appointment.
He will try to respond to emails at least within the next workday, but in most cases much sooner.

Text

Jon Barwise and John Etchemendy, Language, Proof and Logic. CSLI Publications. ISBN 1-57586-374-X. This text is available in the KSU Union Bookstore. Please note that you need to buy a new copy, rather than a used, in order to be able to submit your homework!! The book is integrated with a software package and has a web page at http://www-csli.stanford.edu/LPL/. There is a very helpful Glossary at the end of the book.

Course objectives

We study the fundamentals of symbolic logic: how to write proofs and how to reason semantically. We aim at using those acquired techniques for the design and verification of algorithms. A more specific list of objectives can be found at http://people.cis.ksu.edu/~tamtoft/CIS301/Fall07/goals.html.

Prerequisites

CIS 200 (Fundamentals of Software Design and Implementation). Specifically, students are expected to have understanding of mathematical formalisms such as those used in algebra.

Other courses building on this material

CIS 505, CIS 560, CIS 570, CIS 575, CIS 705, CIS 706, CIS 761, CIS 762, CIS 770, CIS 775.

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. Also, the use of counterexamples to demonstrate that other inferences are not valid.
(Chapters 1-8)
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 (an extension of propositional logic with quantifiers). We study the syntax and semantics of this logic and discuss how it relates to English. We will also discuss its proof theory and prove important quantifier equivalences.
(Chapters 9-13)
Program Logic and Mathematical Induction
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)

Grading and Exams

Homework
There will be approximately 12 homework assignments during the semester. There are two types of homework questions:
Manual
These are to be done with pencil and paper (of course you can also type them!) and must be turned in before class. (You mail alternatively email them, but if you send attachments, you should do it directly to the TA, rather than to the mailing list given below.) Then they will be graded by the TA and returned to you the following week.
Electronic
These must be submitted to the Grade Grinder (again before class!) from which you will receive swift automated feedback. Two things to keep in mind:
  • When submitting, make sure that you ask that copies are sent to cis301instruct HAT listserv dot ksu dot edu (remember ticking "Instructor Too"!) whereas it does not matter what you write as "Instructor's Name". If possible, please try to avoid submitting files one at a time; it will be easier for the TA if you submit all files simultaneously.
    You may submit the electronic portion of your homework as many times as you wish until the deadline; only your most recent submission will be scored (please resubmit all of your files and not just the incorrect ones).
  • If mailing questions to the instructor, please do not attach files from the software package (as he is running Linux and therefore cannot read them) but instead try to communicate the problem using plain text.
In all cases, for each exercise you will receive a number of points. Feedback will be available (password protected) from the web page. Late assignments will not be accepted except for documented medical or family emergencies. (If you hand in your assignment to the front office, please make sure that they not only stamp the date but also indicate the time of day!)

In addition, there may be quizzes, posted on K-State Online.

Exams
There will be three tests during the semester, including the final exam. For each test, there will be emphasis on what was covered since the last test, but the final will still be comprehensive. All tests are open-book, but laptops or other computing devices are not permitted. Each of the first two tests will earn you a score between 0 and 20; the final exam will earn you a score between 0 and 35.
Grades
The final counts 35%, each of the two other tests counts 20%, with the homework (including the quizzes) making up for the last 25%. (Example: if you score 14 on the first test, 16 on the second, 27 on the final, and receive 900 out of 1500 possible points for your homework, your total numerical grade will be 14 + 16 + 27 + (900/1500)*25 = 72.) In addition, I reserve the right to award extra credit to students who make useful comments or suggestions, or who ask good questions.

There is no fixed scheme for the conversion of numerical grades to actual letter 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) except for an undeserved act of mercy ;) Also, 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!

In general, I my approach to grading is expressed well by this piece by S.A. Miller. Let me quote (encouraging you to read the whole thing!)

Test scores tend to be low in my classes. Nineties are rare. Class averages may be in the 60% range. I am not alarmed by apparently low numbers, but they do tend to worry conscientious students who are conditioned to think in terms of 90% = A, 80% = B, etc. This can undermine class morale, and low class morale can undermine student ability. That does concern me, so I offer some suggestions for dealing with these anxieties.

How to deal with the anxieties: Evaluate your standing in terms of what your class is doing. Where are you relative to the class mean? For example, if you have a 72% average, but the class average is 52%, you are doing better than your score might suggest to you. Adding 20 to each number would make the class average a traditional 72% and give you a very respectable 92%. This is a form of "curving" you can do for yourself with each examination. Simply look at the class mean (which is always presented) and adjust it to fall into the 70% range then apply the same correction factor to your score or cumulative average. You can do this in any of your classes if basic information is provided.

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 begin homework assignments ASAP. If you encounter any difficulties with the course material, please feel free to contact the TA or the instructor. You are welcome to discuss the course material with your fellow students. However, all submitted assignments must be your own work: you are not allowed to show your work to anyone else, or look at the work of any other student. Also observe that files submitted to the Grade Grinder must be created by yourself.

It is your responsibility to be up-to-date with current happenings in class, by keeping an eye on the Captain's log and by reading your email regularly. It is your responsibility to collect graded homework assignments and exams in case you are not there the day they are handed back.

Please note that this course is time consuming. Practicing all exercises 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. The following dates may be of interest (please double-check them yourselves!)
September 9
Last day for full refund
September 24
Last day to drop out without W being recorded
October 26
Last day to drop the course
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.

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, and also from the one taught by Rodney Howell. 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.


Torben Amtoft