CIS 301, Logical Foundations of Programming, Fall 2019
Summary
This course teaches the fundamentals of symbolic logic:
how to write proofs, and how to
reason semantically. The acquired
techniques will be used for the reasoning about
program behavior.
-
Credits: 3
-
Prerequisite:
CIS 200 (Fundamentals of Software Design and Implementation)
-
General advice:
Make sure to read the guidelines provided in the
file advice, uploaded on Canvas.
Logistics
Personnel
-
Instructor:
Torben Amtoft,
tamtoft hat ksu dot edu
-
Teaching Assistant:
George (Bud) LaVezzi, gblavezz1 hat ksu dot edu
-
Teaching Assistant:
Sarthak Khanal, sarthakk hat ksu dot edu
Schedule
Event | Place | Monday | Tuesday |
Wednesday | Thursday | Friday |
Classes | Durland 1073 | | 9:30- 10:45am |
| 9:30- 10:45am | |
Torben Office Hours |
Engineering 2179
|
|
1-2pm |
2-3pm |
3-4pm |
|
Bud Office Hours |
Engineering 1117 |
1-2pm |
|
4-5pm in 1116 |
|
8:30-9:30am |
Sarthak Office Hours |
Engineering 1116 |
3:30-4:30pm |
|
3:30-4:30pm |
|
3:30-4:30pm |
Communication
Use the email address
help-301@santoslab.org for all questions about lectures, homework, and appointments. Do not email the TAs or instructor directly (unless there is a very good reason),
and do not use Canvas messaging to contact us.
We make efforts to keep up with email (even though we may not check our inboxes all the time), and it is our goal that you should expect an email answer no later than on the next business day. So if you send an email on Friday, we will aim to get back to you the next day the university holds classes (which will typically be Monday), and often even earlier.
For questions (or comments) of general interest,
we encourage that you post in the Canvas discussion forum
so that also other students will benefit from the answers.
We even encourage you to answer questions from other students
(of course you should not give more hints towards solutions
than you would reasonably expect the instructor to give).
Course Material
Course Notes
The main course material is the notes Logika: Programming Logics,
available at
http://logika.sireum.org/dschmidt/ and developed by
David Schmidt,
later modified by Bud LaVezzi and John Hatcliff.
Other references may be provided as the course unfolds.
Software Tools
The main tool is Sireum Logika,
available at http://logika.sireum.org
and developed by
Robby.
Logika is a program verifier and a natural deduction proof checker for propositional, predicate, and programming logics. Logika is part of a much larger analysis and verification framework, called Sireum, developed by Robby.
It is crucial that you get set up to use Logika during the first week of class. We will use Logika every week in class, and almost all homework assignments will use it.
Logika can be used in a nice IntelliJ-based Integrated Verification Environment (Sireum/Logika IVE); this is what we recommend for doing all your classroom exercises and homework.
Objective and Topics
The first notions of formal logic were invented over 2000 years ago as philosophers attempted to develop systematic approaches for arriving at statements that were true. By the time we approach adulthood, we will have heard many people say (or we will have said ourselves): that seems logical, or you're being illogical. By this, we understand that (in the first case) sound reasoning principles have been used, whereas in the latter case someone may be stating a conclusion that cannot be justified by sound reasoning from an initial set of true facts. This "every day" notion of logic that manifests itself in the arguments that we make in natural language is sometimes referred to as informal logic.
In contrast, in this course, we will study concepts related to formal logics. In simple terms, a formal logic consists of some syntax for stating claims (properties that are either true or false) about the world (or some other more specialized domain in which we are interested), and rules for deriving claims that are guaranteed true.
Formal logic is deeply tied to computer science, because computers are great at "blindly following rules", and many interesting issues in computer science can be phrased as basic claims together with systems of rules. Formal logics can define and explain, for example, the basic gates and circuits from which computers are built, the behavior of our programs as they execute, the protocols that our computer systems use to communicate, the expert systems that provide automated assistance to professionals such as doctors or pilots. Formal logic thus
provides, which is very important, the basis for automated rule-based reasoning for these systems.
In this course, we will learn the basic elements found in a formal logic, including syntax for claims and rules for making deductions. We will also learn how to judge if our rules are suitable in the sense that they only lead us to claims that match the reality of the domain we are reasoning about.
Our focus will be on formal logics for reasoning about program behavior and for programming directly in terms of logic. We will see how tools based on logic are used to reason about safety and security critical software, network security, and security protocols.
Grading
-
Homework: 25% (your lowest homework score will be disregarded)
-
Exam 1 (Sep 24): 25%
-
Exam 2 (Nov 12): 25%
-
Final Exam (December 19): 25%
Final letter grades are not based on strict percentage cutoffs but are
"curved" by taking into account the difficulty of the exercises and
exams. As a rule of thumb, however,
you should expect that it requires
almost 90 % to earn an A,
a bit above 75 % to earn a B,
and somewhat more than 60 % to earn a C.
In general, my approach to grading is expressed well by
this
piece by S.A. Miller.
Homeworks
are due most weeks
and are to be submitted through Canvas.
Exams
will be closed-book and closed notes.
The final will be comprehensive,
but with emphasis on the latter part of the course.
Grievances
If you think the instructor or the TAs have made an error 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).
Academic Honesty
Kansas State University has an Honor and Integrity 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 and graduate students, by registration, acknowledge the jurisdiction of the Honor and Integrity System. The policies and procedures of the Honor and Integrity System apply to all full and part-time students enrolled in undergraduate and graduate courses on-campus, off-campus, and via distance learning.
A component vital to the Honor and Integrity System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by 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. The F indicates failure in the course; the X indicates the reason is an Honor Pledge violation.
You are very welcome to discuss the course material, as well as
specific questions, with your fellow students.
However, all submitted
answers must be your own work:
-
You are not allowed to consult previous model solutions that
may be around, or solicit the Internet for solutions to
specific homework problems (but you are very welcome
to search for general material that gives alternative presentations
of the topics of the course!)
-
You are not allowed to show your
answers to, or look at the answers of, any other student --- this of course
excludes any student that you have been allowed to team up with,
but in such a case each of you must be able to understand and explain
all parts of the submitted work.
If you are in doubt about what is permissible, please ask me.
I very much hope that it will not be
necessary to file any honor pledge violation reports during the
semester!
Other Administrative Issues
-
Lateness:
If you have a documented medical or family emergency,
or a certified excused absence for official university activities,
you should notify the instructor as soon as possible.
In such a case, you may be granted extensions for homework assignments.
For exams,
we do not offer make-ups, but will disregard that exam
(this is roughly equivalent to eventually
assigning you a score close to your average for
the other two exams).
If you do not have a valid excuse, you should not expect any points
for missed exams or late assignments, with the following exception:
if you submit
an assignment less than 12 hours after the deadline, we will grade it,
but afterwards subtract 20% of your score.
-
Drop Policy: It is your responsibility to drop the course if you are enrolled but decide not to complete the course; there are no "automatic" drops due to nonattendance.
-
Student with Disabilities
who need classroom accommodations, access to technology, or information about emergency building/campus evacuation processes should contact the Student Access Center and/or their instructor. Services are available to students with a wide range of disabilities including, but not limited to, physical disabilities, medical conditions, learning disabilities, attention deficit disorder, depression, and anxiety.
If you are a student enrolled in campus/online courses through the Manhattan or Olathe campuses, contact the
Student Access Center
at accesscenter@k-state.edu, 785-532-6441;
-
Incompleteness:
An incomplete (I) final grade will be given only by prior arrangement in
exceptional circumstances
in which the bulk of course work has been completed in passing fashion.
-
Expectations for Classroom Conduct:
All student activities in the University, including this course, are governed by the
Student Judicial Conduct Code
as outlined in the Student Governing Association By Laws, Article V, Section 3, number 2. Students who engage in behavior that disrupts the learning environment may be asked to leave the class.
-
Copyright 2019 (Torben Amtoft) as to 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. In addition, students in this class are not authorized to provide class notes or other class-related materials to any other person or entity, other than sharing them directly with another student taking the class for purposes of studying, without prior written permission from the professor teaching this course.
Acknowledgments
Most of the course material, including much of this syllabus,
is adapted from
previous courses
taught by
John Hatcliff
and
Robby
and (less recently)
David Schmidt
(the original creator of the lecture notes) and
Torben Amtoft.
Torben Amtoft