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