This course introduces a selection of theories, practices, and tools that, we believe, will enhance the student's ability in developing correct and high quality software. The view taken here is that of an engineer (programmer, software engineer, or software architect) and hence the focus of the course is primarily on the technical aspects of software development process.

• Feb. 03: Grade Report available.
• Jan. 15: slides for Linear Temporal Logic available.
• Dec. 24: slides for Automata-Based Model Checking available.
• Dec. 18: slides for Alloy available.
• Dec. 08: old exams and solutions available.
• Dec. 03: slides for UML Part II: Advanced Modeling available.
• Dec. 03: slides for UML Part I and for UML Part II: OCL updated.
• Nov. 26: A note with Example OCL Specifications available.
• Nov. 25: slides for Web Programming and Software Security and for OCL available.
• Nov. 22: slides for Prof. Orna Grumberg's lecture on Model Checking available.
• Nov. 17: slides for Design Patterns available.
• Oct. 22: HW#3 due on Oct. 29.
• Oct. 15: HW#2 due on Oct. 22.
• Oct. 15: slides for UML Part I available.
• Oct. 1: Term Project announced.
• Oct. 1: slides for Hoare Logic and notes on Rules of Hoare Logic and Proofs with Hoare Logic available.
• Sep. 24: HW#1 due on Oct. 1.
• Sep. 24: slides for First-Order Logic and notes on System LK, Example Proofs, and Natural Deduction available for download.
• Sep. 17: HW#0 due on Sep. 24.
• Sep. 17: PDF version of this page; slides for Introduction and Propositional Logic available for download.

Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)

Thursday 9:10-12:10, Room 101, College of Management, Building I

Wednesday 1:30-2:30PM or by appointment

Yi-Wen Chang (常怡文), 3366-1205, Xr97725004@ntu.edu.twX (between the enclosing pair of X's)

Object-Oriented Programming and Discrete Mathematics

Class Notes and Selected Readings

The goal of this course is to acquaint the students with some of the well-used methods and tools for practical software development as well as some fundamentals of software verification, so as to prepare them for a career in software development. After an introduction of the subject matters and a brief glimpse of formal logic and program correctness, we will study in great detail the UML, design patterns, and some fundamental elements of formal software verification and analysis.

• Introduction (.5 week: 09/17a)
  overview of software requirements, development process, design methods, and testing/verification tools.
  [slides:Introduction]
• Formal Logic (1.5 weeks: 09/17b, 09/24)
  propositional logic (satisfiability, tautologies, deduction/proofs), first-order logic (validity, deduction/proofs, soundness, completeness)
  [slides:Propositional Logic, First-Order Logic; notes: System LK, Example Proofs, Natural Deduction]
• Program Correctness (1 week: 10/01)
  axiomatic semantics of programs (assertions, pre/post-conditions, invariants), partial and total correctness
  [slides: Hoare Logic; notes: Rules of Hoare Logic, Proofs with Hoare Logic]
• Model Checking (1 week: 10/08)
  Guest Lecturer: Orna Grumberg, Technion, Israel
  [slides]
• UML - Part I (1 week: 10/15)
  introduction, basics of modeling, overview of the UML, structural modeling (class diagrams, classifiers, interfaces, packages), behavioral modeling (interactions, use case diagrams, interaction diagrams, activity diagrams), architectural modeling (collaborations, deployment diagrams)
  [slides]
• Design Patterns (4 weeks: 10/22, 10/29, 11/05, 11/12)
  Guest Lecturers: Jeffrey CH Liu, Clement CW Su, and Jim CL Yu, IBM
  1. introduction (design document, use case, development tool)
     [slides: Version Control; notes: Design Document Example]
  2. creational patterns (abstract factory, builder, factory method, prototype, singleton)
     [slides:Creational Patterns]
  3. structural patterns (adapter, bridge, composite, flyweight, proxy, decorator, facade)
     [slides:Structural Patterns]
  4. behavioral patterns (chain of responsibility, iterator, observer, mediator, command, memento, state, strategy, template method, interpreter, visitor)
     [slides:Behavioral Patterns]
• Web Programming and Software Security (1 week: 11/19)
  dynamic Web pages, client-side scripts, patterns, frameworks, security vulnerabilities, vulnerabilities detection and prevention
  [slides:Patterns for Web Programming, Web Application Security]
• UML - Part II (2 weeks: 11/26, 12/03)
  advanced structural modeling (object diagrams, components), advanced behavioral modeling (events, state machines, processes and threads, timing constraints), Object Constraint Language (OCL)
  [slides: Advanced Modeling,OCL; notes: OCL Examples]
• Software Modeling Tools (1 week: 12/10)
  Alloy (software modeling, simulation, and checking)
  [slides]
• Midterm (2009/12/17)
• Software Model Checking (2 weeks: 12/24, 12/31)
  linear-time model checking (Kripke structure, linear temporal logic, Büchi automata, automata-theoretic algorithms), Spin (Promela, never-claims), JPF (Java Pathfinder)
  [slides: Automata-Based Model Checking, Linear Temporal Logic]
• Term Project Presentations (2010/01/07)
• Program Verification Tools (1 week: 01/14)
  Spec#, JML tools (Common JML Tools, ESC/Java2)

Homework 20%, Midterm 40%, Term Project 40%.

1. Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (free!)
2. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
3. Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
4. The UML Resource Page: http://www.uml.org/, OMG.
5. The Unified Modeling Language User Guide, 2nd Edition, G. Booch, I. Jacobson, and J. Rumbaugh, Addison-Wesley, 2005.
6. Object Constraint Language, OMG Available Specification, Version 2.0, OMG.
7. Design Patterns: Elements of Reusable Object-Oriented Software, E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Addison-Wesley, 1995.
8. Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
9. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzman, Addison-Wesley, 2003.
10. Spin - Formal Verification Page: http://spinroot.com/.
11. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer-Verlag, 1995.
12. The Formal Methods Page: http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.)

[Midterm 2004, Solutions]
[Final 2004]
[Midterm 2006, Solutions]
[Final 2006]
[Midterm 2008]