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.

• Jan. 27: Grade Report available.
• Dec. 23: slides for Alloy available.
• Dec. 13: Solutions to HW#1 available.
• Dec. 09: HW#2 due on Dec. 16.
• Dec. 09: slides and notes for OCL available.
• Nov. 10: slides and notes for Hoare Logic available.
• Nov. 10: slides for Propositional Logic and First-Order Logic available.
• Nov. 10: slides for Behavioral Design Patterns available.
• Oct. 21: slides for Structural Design Patterns and Version Control available.
• Oct. 20: slides for Design Patterns Introduction and Creational Design Patterns available.
• Oct. 06: slides for Software Modeling: Advanced UML (UML Part II) and Web Application Security available.
• Sep. 30: slides for Introduction to RTC and Web Application Development and a design document sample available.
• Sep. 30: due dates of 1st Preliminary Design Document and 1st Prototype Demo extended to Oct. 20 and Nov. 04 respectively.
• Sep. 29: details of Term Project available.
• Sep. 23: slides for Software Modeling: Basic UML (UML Part I) available.
• Sep. 19: slides for Formal Logic: A Pragmatic Introduction revised.
• Sep. 16: slides for Introduction and Formal Logic: A Pragmatic Introduction and a note on Natural Deduction available.
• Sep. 10: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version (unlike in previous years).

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

Ming-Hsien Tsai (蔡明憲), 3366-1205, Xmhtsai208@gmail.comX (between the enclosing pair of X's)
Jen-Feng Shih (施任峰), 3366-1205, Xr98725050@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 overview of the subject matters and a brief glimpse of formal logic, we will study in great detail the UML, design patterns, and some fundamental elements of formal software modeling, verification, and analysis.

• Introduction (.5 week: 09/16a)
  overview of software requirements, development process, design methods, and testing/verification tools.
  [slides]
• Formal Logic: A Pragmatic Introduction (.5 week: 09/16b)
  propositions, proofs, predicates, models, theorems
  [slides; notes:Natural Deduction]
• Software Modeling: Basic UML (1 week: 09/23)
  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/Tools, Design Documents, Patterns for Web Programming (1 week: 09/30)
  Guest Lecturers: Jeffrey CH Liu, Clement CW Su, and Jim CL Yu, IBM
  [slides: Introduction to RTC; Web Application Development and Patterns; notes: Design Document Example]
• Software Modeling: Advanced UML (.5 week: 10/07a)
  advanced structural modeling (object diagrams, components), advanced behavioral modeling (events, state machines, processes and threads, timing constraints)
  [slides]
• Software Security (.5 week: 10/07b)
  dynamic Web pages, client-side scripts, frameworks, security vulnerabilities, vulnerabilities detection and prevention
  [slides]
• Design Patterns: Creational Patterns (1 week: 10/14)
  Guest Lecturer: Clement CW Su, IBM
  abstract factory, builder, factory method, prototype, singleton
  [slides: Introduction to Design Patterns; Creational Patterns]
• Design Patterns: Structural Patterns (1 week: 10/21)
  Guest Lecturer: Jeffrey CH Liu, IBM
  adapter, bridge, composite, flyweight, proxy, decorator, facade
  [slides: Structural Patterns; Version Control]
• Formal Logic: Propositional and First-Order Logics (1.5 weeks: 10/28, 11/11a)
  satisfiability, tautologies, validity, deduction/proofs, soundness, completeness
  [slides:Propositional Logic, First-Order Logic]
• Design Patterns: Behavioral Patterns (1 week: 11/04)
  Guest Lecturer: Jim CL Yu, IBM
  chain of responsibility, iterator, observer, mediator, command, memento, state, strategy, template method, interpreter, visitor
  [slides]
• Software Verification: Hoare Logic (1.5 weeks: 11/11b, 11/18)
  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]
• Software Modeling: OCL (1 week: 11/25)
  Object Constraint Language (relation with UML models, values, types, expressions, objects, properties, collection operations)
  [slides; notes: OCL Examples]
• Software Modeling: Alloy (1 week: 12/02)
  software modeling, simulation, and checking
  [slides]
• Software Modeling: Event-B (1 week: 12/09)
  Guest Lecturer: Prof. Jean-Raymond Abrial
  (cancelled)
• Midterm (2010/12/16)
• Software Verification: Hoare-Style Verifiers (2 weeks: 12/23, 12/30)
  Frama-C, Spec#
• Term Project Presentations (2011/01/06)
• Software Verification: Model Checkers (1 week: 01/13)
  linear-time model checking, Spin (Promela, never-claims), JPF (Java Pathfinder)
  [slides: Linear Temporal Logic, Automata-Based Model Checking]

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. Modeling in Event-B: System and Software Engineering, J.-R. Abrial, Cambridge University Press, 2010.
10. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzman, Addison-Wesley, 2003.
11. Spin - Formal Verification Page: http://spinroot.com/.
12. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer-Verlag, 1995.
13. 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]
[Midterm 2009]