CIS 301 Logical Foundations of Programming ------------------------------------------ 1. Prerequisites by topic: * college algebra * basic imperative programming skills * intuitive understanding of the semantics of simple imperative programs * an exposure to invariants of while-statements 2. Knowledge and skills acquired in this course: a. Mastery: * proving propositional logic sequents in the natural deduction calculus * understanding syntax and truth table semantics of propositional logic * developing the ability to apply mathematical induction * proving predicate logic sequents in the natural deduction calculus * understanding the syntax and semantics of predicate logic * understanding the syntax and semantics of computation tree logic (CTL) * verifying a CTL formula for simple models * verifying the partial, or total, correctness of Hoare triple over a simple imperative core language * computing insightful invariants for while-statements b. Familiarity: * converting a propositional logic formula into an equivalent formula in conjunctive normal form and appreciating its complexity * appreciating the concepts of "satisfiability" and "validity" of propositional logic and predicate logic formulas * realizing the significance of soundness and completeness of natural deduction for propositional logic and predicate logic * realizing the impact of the undecidability of validity and satisfiability in predicate logic * appreciating a labeling algorithm for model checking and the use of the SMV for symbolic model checking * being exposed to practical specification patterns expressed in CTL * understanding the importance of soundness and relative completeness of proof calculi for partial and total program correctness * realizing the significance of the undecidability of the Halting problem * being exposed to a case study of algorithm design and verification