656/556 2003 1w 21 Final Outline
Comprehensive: Chapters 1,2,3,4, & 6.
Final 200 points. Answer 4 out of given 5 questions each worth 50 points.

Each question can have several parts.  The following skills may be tested
Qn 1. Propositions, Normal Forms & OBDDs
	Draw parse tree of a well-formed formula (wff)
	Convert wff into a truthtable/OBDD.
	Use a given CNF/truthtables/OBDD to verify that wff  is always true
			(or an argument valid).
	Use a given DNF/truthtables/OBDD/  to prove that wff can be satisfied.
	Convert OBDD to Boolean Expression/Proposition
	Draw the reduced Ordered Binary Decision Diagram of ....
	Use the reduce and apply algorithms in the book.
	Give reasons why OBDDs are an important technique for formal 
		methods people.
	Give examples of tools that use OBDDs.

Qn 2. Predicate Calculus
	Draw parse trees of given wffs of the Predicate Calculus:
	Prove a given theorem (with a short proof) from the Predicate Calculus.
	Translate of English to well-formed formulae of the Predicate Calculus
	Translate assumptions and prove a conclusions (when proof is simple)
	Explain what Prolog can be used for.

Qn 3. Model checking and CTL 
	Draw parse tree of well-formed formula of CTL. 
	Draw  a finite state model to fit a given description of states, 
			transitions etc..
	Unwind a finite state model into a tree
	Demonstrate how OBDDs can express a finite state model.
 	Calculate states in a model that do or do not satisfy a given CTL
		formulae
	Express common types of specification  in CTL.
	Explain what a model checking tool like SMV or Spin  can do for a 
		project reported in the literature.
.
Qn 4. Verification
	Push Assertions backwards though given assignments.
	Generate and verify assertions involving 'if's.
	Given loop invariants fill in and  verify assertions in code that 
		has a loop using Tableaux and proving partial correctness.
	Give an example of a common program structure missing in the
		texts "Core" language and show that this lets the books
		methods from applying to (say)C++.
	Explain when program verification can help a programmer/designer.

Qn. 5
	Write a 1 page essay describing the content of any presentation --
	but not one you gave.

Items covered next year
	Use Shannon's Expansion to generate an OBDD
	Use Boolean Algebra 01+*- to
		express a proposition,  argument, or theorem
  		transform <>  to Conjunctive Normal Form (CNF)
  		transform <> to Disjunctive Normal Form (DNF)
		Interpret resulting constant values of 0(inconsistent) 
			or 1(theorem/valid)
	Given loop invariants fill in and  verify assertions in code that
		has a loop using Tableaux and proving  total correctness.