CS330 - Formal Methods and Models -- Fall 2002 -- Richards

George Mason University
DEPARTMENT OF COMPUTER SCIENCE

CS330 - Formal Methods and Models - Fall 2002

Professor Dana Richards
703-993-1545
richards@cs.gmu.edu
(Please prefix the subject of your email with CS330.)

Course office hours: Monday-Wednesday 11:00-12:00 or by appt.
Sci&Tech II Room 425

PREREQUISITES :

CS211 and Math 125 (C or better in both).
The exposure to Discrete Mathematics (in Math 125 or a similar course) for most students has been important for success in this course.

DESCRIPTION :

This course is an introduction to two kinds of formal systems - languages and logics - with important applications to computer science. The study of formal languages underlies important aspects of compilers and other language processing systems, as well as the theory of computation. Various systems of logic and automatic reasoning are put to use in artificial intelligence, database theory and software engineering. The entire course will give you practice in precise thinking and proof methods that play a role in the analysis of algorithms. The programming assignments in Lex and Prolog provide practical experience with some theoretical topics.

READINGS:

Logic and Languages Models for Computer Science, by Hamburger and Richards.

SYLLABUS:

The pace is approximate. Later chapters will not be covered as completely.

  Topic                                 Week        Part/Chapters

  Introduction                           1          1
  Propositional Logic and Proofs         1-2        2-3
  Predicate Logic and Proofs             3-4        4-5
  Applications: Prolog and Verification  5-6        6-7
  Exam #1                                6
  Finite Automata, Regular Expressios    7-9        8-10
  Lex: a Regular Expression Language     10         11
  Exam #2                                10
  Context-Free Grammars & Applications   11-12      12-13
  Turing Machines & Solvability          13-14      14

GRADING :

Quizzes -- 20%
Programs -- 25%
Exams -- 55%

The three exams, including the final, each cover about a third of the semester; the final is not cumulative. Of these exams the highest score will count 20%, the next 20%, and the lowest 15%.

Homework is ungraded.
Quizzes will test homework, typically each Thursday.
The two lowest quiz grades will be dropped.
There will be programming assignments in Lex and in Prolog.

All testing is closed book, but limited notes are permitted, as follows for exams (but not for quizzes). One sheet of notes (8.5 by 11 inches, 1 side only). NO COPYING is allowed. That means no photocopying of anything, even the textbook, though you may write out material from it verbatim. It also means no copying of anyone else's notes, even by hand. You may use a computer for editing your own notes. The sheet must be turned in with your exam. Violations of these rules for creating the notes is considered a violation of the Honor Code.

There is to be NO group work on the programs. Receiving direct contributions to the code that is submitted is considered a violation of the Honor Code. (See cs.gmu.edu/students/hnr_cds.html for the GMU and Computer Science guidelines.)

LATENESS:

Programs will be marked down 25% each week they are late; for example it marked down 25% the first 7 days after the due date.

TA:

Yuelan Li. yli8@gmu.edu
(Office hours: Tuesday 3:00-4:00 and Wednesday 2:00-4:00, room 365, S&T II.)