CIS 301. Logical Foundations of Programming
Fall 2002 Syllabus
-
Where, When, Who?
- Location and Time: 122 Nichols Hall,
MWF 10:30-11:20 A.M.
- Instructor and E-Mail:
- Torben Amtoft tamtoft@cis.ksu.edu
Office and Phone: 216 Nichols Hall, ph. 532-6350
Homepage URL: www.cis.ksu.edu/~tamtoft
Help Sessions:
Wednesdays, 5:00-6:00 P.M. in N127.
Office Hours:
Mondays and Wednesdays 1:00-2:00 P.M. and by appointment. My office is
located in N216.
-
Teaching Assistant:
-
Srinivas Kolluri kolluri@cis.ksu.edu
Homepage URL: www.cis.ksu.edu/~kolluri
Office Hours: Tuesdays and Thursdays 11:00-12:00 A.M. and by
appointment, at N019K.
-
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 has a
web page
(including errata files) and
is supported by a
worldwide
web tutor.
Course Home page: http://www.cis.ksu.edu/~tamtoft/CIS301/Fall02/index.html
Course objectives
We study the fundamentals of symbolic logic: how to write proofs and how to
reason semantically. We use those acquired techniques for the design and
verification of algorithms. We might further use them to check whether models
of computer systems satisfy specified properties.
Prerequisites
CIS 200, and recursively, all prerequisites thereof. If you have not taken CIS
200, 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.
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.
(Chapter 1; 3-4 weeks.)
- Predicate 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 predicate logic. Data
abstraction mechanisms in programming languages (e.g., modules/packages)
are often understood in terms of foundational concepts from predicate
logic. We study the syntax and semantics of this logic and understand how
to evaluate (i.e., give meanings to) formulas over their corresponding
notion of models. We will also discuss its proof theory and prove
important quantifier equivalences.
(Chapter 2; 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. We treat a simple
imperative language with if-statements and while-loops.
(Chapter 4; 4-5 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 sketch an
automated verification algorithm which takes a description of a system and
a formula as input and checks whether that system enjoys that property.
(Chapter 3; rest of course, time permitting).
Grading and Exams
- Homework: 25%
- Homeworks will be pencil and paper exercises. Late assignments will not
be accepted except for medical or family emergencies.
- Exams: 75%
- There will be three open-book exams,
the first on Wednesday, October 16th, 2002.
Each exam counts for 25% of the
final grade. None of the exams will be comprehensive; they will cover only
relevant parts of the syllabus.
To pass the course, a student must score at least 50% of all possible
points in the course. Failure to achieve this will automatically result in
an F.
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. From past experience,
students who repeatedly miss classes have done poorly in exams. So do attend
lectures regularly! It is your responsibility to obtain class notes in case
you miss a lecture. It is your responsibility to collect graded homework
assignments and exams. I will correspond with the class frequently by e-mail,
so it is your responsibility to be up-to-date with current happenings in
class.
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 here.
- 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 and course is (heavily) adapted from the one
taught by Michael Huth and
later modified
by Anindya Banerjee. Please see
the Copyright notice in the
first document. Beyond this, all lectures in the course are Copyright
2001, 2002 (Anindya Banerjee & Torben Amtoft). 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
|