George Mason University
DEPARTMENT OF COMPUTER SCIENCE
CS330 - Formal Methods and Models - Spring 2015
Monday, Wednesday
1:30 – 2:45pm, Innovation Hall 136
This page last
updated on 1/20/2015
Prof.
Alexander Brodsky
703-993-1529
brodsky@gmu.edu
(Please prefix
the subject of your email with CS330.)
Office
hours: Thursday 3:30 – 5:00 pm
Engineering
Bldg 4418
PREREQUISITES :
CS211 and Math
125 (C or better in both).
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 provide practical experience with some theoretical
topics.
OUTCOMES :
Will
understand the concepts and relevance of logic, formal languages and automata
theory, and computability .
Will be able
to able to do mechanical formal proofs, program correctness proofs and solve
problems in first-order logic.
Will be able
to solve problems in elementary machine models: designing finite-state,
pushdown and turing machines.
Will be able
to solve problems in formal languages: writing regular expressions, regular
grammars, and context-free grammars.
READINGS:
(available as a packet at the
bookstore) (soon)
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:
Relational Calculus
and
Datalog
5-6 Lecture Notes
Exam
#1
7
Finite
Automata, Regular Expressios 7-9 7-9
AWK:
Regular Expression Application 10
B
Context-Free
Grammars & PDAs
11-12
10-11
Turing
Machines & Computability
13-14
12
GRADING :
Quizzes -- 20%
Programming
Assignments -- 20%
Exams -- 60%
The two exams,
including the final, each cover about a half of the semester; the final is not
cumulative.
Of these exams
the highest score will count 35%, and the lowest 25%.
Homework is
ungraded.
Quizzes will
test homework, typically every other class class.
The lowest
quiz grades will be dropped.
There will be
small programming assignments in Relational Calculus/ Datalog and AWK.
All testing is
closed book.
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/wiki/pmwiki.php/HonorCode for the GMU and Computer Science
guidelines.)
It is a
departmental requirement that students in CS330 must see their advisor and discuss their degree progress. Students not fulfilling this
requirement will receive an Incomplete grade. (Non-majors and graduate students
are not included.) The visit
must be documented by a signed note or email from your advisor.
LATENESS:
Programming
assignments will be marked down 25% each class they are late; in particular, it
is marked down 25% after the due date.
TA:
Ivan Avromovic, iavramo2@gmu.edu,
hours TBA
NO LAPTOP USAGE during class (If you NEED a laptop for
note-taking then speak to me.)