Spring 2012 Semester

Logical Foundations of Computing

Lectures: MWF 10:30am, Nichols Hall, room 019

Instructor: David Schmidt (das @ksu .edu, phone: 532-7912, 219A Nichols Hall)     

Teaching assistant: Hao Qian (hqian @ksu .edu, 16A Nichols Hall)

Announcements (last updated April 13) | Lectures | Exercises

Syllabus | Course Text (see below) | Software Support (see below)

Office hours:
Schmidt: Monday, Tuesday, Thursday, Friday, 12:45-1:30pm, Nichols 219A
Qian: Monday and Wednesday, 3:30-4:40pm, Nichols 16A

You are always welcome to send email to schedule meetings with the instructors.

No class the week of April 16; lectures resume April 23

Course Text

We will use an on-line text I have written, found at the Lectures page on this site. The text isn't perfect, but I am saving you $100 this way....

Software Support

  1. Proof checker for Floyd-Hoare program logic: We will develop correctness proofs for programs with the assistance of a checker tool that I have written:
    • The checker runs on top of Python. Please read Installing Python to learn how to check for Python on your machine, install it if needed, and later use it to develop software.
    • Download the checker tool to your computer: cis301.zip. It holds the checker. Read the installation guide to learn how to install the checker.
      If it is impossible for you to unzip cis301.zip, here is the link to the cis301 folder. Download from here as a last resort.
    • Next, read the beginner's guide to using the checker. This should be enough to get you started.
    • There's more, if you're curious: Here is the README file that is contained in the zip file. There is also a DOC.txt file that defines precisely the language understood by the checker. The DOC file also includes a series of progressively more fiendish examples that the checker will analyze and approve.

  2. Python: Python is a nice complement to Java, C#, etc., because it is a dynamically typed and structured language rather than a static one, and it naturally supports recursive programming rather than iterative. For this reason, we will do at least one exercise with it. If you have never programmed in Python before, you can relax --- it looks like Visual Basic or Javascript or any other baby assignment language. But it has powerful dynamic data structures (lists and dictionaries). Here are some samples of Python code. (Here is a zipped folder of the samples.) Try these with your implementation.

    Some other materials:

    * a terse language summary and terse notes on lists and dictionaries, the two most important data structures in Python. Here is a complete tutorial, from the days when I taught CIS200.
    * The language's website is at http://www.python.org/, where you will find a useful library reference page.
    * This nice on-line book, The Python Standard Libary, shows you how to use Python to do clever systems hacking and gluing, the sort of stuff that is not normally taught in courses but is hugely useful in practice.

  3. Symbolic-logic proof checker: When we study Chapters 5 and 6 of the on-line text, we will use a tool developed in-house by Mr. Brian Mulanda, Dr. Rod Howell, and Mr. James Thompson for checking logic proofs. The tool runs on top of Java. If you have Java installed on your computer (very likely), then you can download the tool to your Desktop and double-click to start it:

  4. Prolog: At the end of the course, we will take a quick look at the Prolog programming language. There is a good, easy-to-install implementation at www.swi-prolog.org.