PSU CS 251: Discrete Structures II

Spring 2016

Instructor: Bart Massey <bart@cs.pdx.edu>
Time: Tuesday/Thursday 16:40-18:30 (4:40-6:30 PM)
Place: FAB 40-06
CRN: 60904 (sec 5)
URL: http://moodle.svcs.cs.pdx.edu/cs251

TA: Hao Wu <wuhao@pdx.edu>
TA office hour: Wednesday 12:00pm-1:30pm @ fishbowl

As always, this is a tentative syllabus. Everything here is subject to vast change with little notice.

About This Course Offering

This section of this course is the second part of a special offering of CS 250 / CS 251! The course is being taught with a highly non-standard textbook and syllabus. Unless you completed the corresponding section of CS 250 , you may not continue with this section of CS 251: you will be administratively dropped from the course.

About This Course

The catalog says "Continuation of CS 250", and then goes on to give a long list of tools and methods.

CS 251 is a second course in "Discrete Structures". This is essentially mathematical modeling for computer science. The focus of the course is on aplying standard mathematical / logical tools in describing and understanding algorithms and data.

This is not a software engineering course: there is little computational content. The focus is on skills that will be needed to solve problems.

Course Goals

The catalog says:

The main goal of the sequence is that students obtain those skills in discrete mathematics and logic that are used in the study and practice of computer science.

The catalog's list of course goals for this course are that students be able to:

• Apply the properties of propositional calculus to: determine whether a wff is a tautology, a contradiction, or a contingency by truth tables and by Quine's method; construct equivalence proofs; and transform truth functions and wffs into conjunctive or disjunctive normal form.

• Describe the basic inference rules and use them to write formal proofs in propositional calculus.

• Apply the properties of first-order predicate calculus to: determine whether a wff is valid, invalid, satisfiable, or unsatisfiable; construct equivalence proofs; and transform first-order wffs into prenex conjunctive or disjunctive normal form.

• Describe the rules of inference for quantifiers and use them along with the basic inference rules to write formal proofs in first-order predicate calculus.

• Write formal proofs in first-order predicate calculus with equality.

• Construct partial correctness proofs of simple imperative programs and construct termination proofs for simple loops.

• Transform first-order wffs into clausal form; and unify atoms from a set of clauses.

• Describe the resolution inference rule; use it to write formal proofs in first-order logic; and describe how resolution is used to execute a logic program.

• Transform simple English sentences into formal logic (propositional, first-order, or higher-order).

• Apply appropriate algebraic properties to: simplify Boolean expressions; simplify regular expressions; write recursive definitions for simple functions in terms of operations for abstract data types; write expressions to represent relations constructed in terms of operations for relational databases; and work with congruences.

This is ridiculous amount of material for 10 weeks. We will cover whatever we can get to, relying on the fact that we covered some of this in CS 251: please see the opening section of this syllabus for why this will work for us.

Approach: The Z Specification Notation

In this course, we will tackle the material in a unique way: by learning to use and apply the Z specification notation (pronounced "zed" because of its British ancestry). This notation, developed in the 1970s, is a particular syntax for first-order logic with finite and integral "sorts" (types).

The Z notation has a tiny bit of extra syntax and semantics that makes it easier to apply it to the specification of software. There are also a number of software tools for formatting, checking and proving Z specifications, some of which we will learn to use in this course.

Course Mechanics

This course is a high-effort essential part of the PSU undergraduate CS curriculum. There will be lectures, quizzes, examinations and homework. Anonymous peer review will be a part of the course activity.

Communication

The course website (see above) will be the focus of communication. Please use the website forum as a first resource for discussion and questions: your classmates are most likely the quickest source of best help. Students are encouraged to contact the instructor any time by email for an appointment if there are things that seem worth discussing. The instructor will run office hours as need warrants.

Lectures

The course lectures will cover a variety of topics. Please attend them all; they are required and should be useful.

Readings

The course textbooks are

The Way Of Z
Jonathan Jacky, Cambridge Press 1997

Using Z: Specification, Refinement and Proof
Jim Woodcock and Jim Davies, University of Oxford
Prentice-Hall 1996

You can get a free PDF of the second text from the authors here if you prefer not to buy a copy.

There will also be other reading provided as needed.

Coursework

There will be some in-class assignments. You need to be in class every session. If you cannot make it to class, please contact me in advance of the class meeting. I will advise you on how to deal with the situation.

There will be regular homeworks and a final project.

Grading

• Homework: 60%
• Final Project: 40%

Due to the size of the course and the volume of material to be covered, late assignments will not be accepted. A grade of 0 may be given to any assignment not turned in on time; failing any one assignment is grounds for failure in the course.

Anonymous peer evaluation will be a component of assignment grading. A student will be graded both on the assignment itself and on the student's grading of the assignment of others.

Academic Honesty

If you do something that violates the University's or the Department's Student Conduct code, there will be the most severe penalties I can manage. In particular, if you plagiarize (use other people's ideas, text, or code without acknowledgment) I will do what I legally and ethically can to end your academic career. If you have questions, please contact me for clarification.