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. Its goal 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. 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. 05: Grade Report available.
• Dec. 29: Tactics for Natural Deduction in Coq revised (again on Jan. 07).
• Dec. 28: three sample Coq files: exercise_prop.v, exercise_pred.v, exercise_group.v.
• Dec. 28: Tactics for Natural Deduction in Coq.
• Dec. 22: bring your notebook computer Dec. 29 with Coq installed.
• Dec. 22: slides for OCL revised (just one small change on Slide 6).
• Dec. 21: slides for Automata-Based Model Checking and for Temporal Logic and Automata available.
• Dec. 21: slides for OCL Examples and for Alloy available.
• Dec. 11: exercise problems for writing first-order formulae available as HW#3.
• Nov. 24: slides for OCL available.
• Nov. 18: Term Project formally announced.
• Nov. 16: slides for Formal Logic and a note on Natural Deduction available.
• Nov. 02: slides for Web Application Security available.
• Oct. 26: slides for Web Programming available.
• Oct. 20: HW#2 revised and due dates postponed to Nov. 7 (design document) and Nov. 10 (oral presentation and demo).
• Oct. 19: slides for Design Patterns and Enterprise Design Patterns available.
• Oct. 16: HW#2 due on Oct. 31 (design document) and Nov. 3 (oral presentation and demo).
• Oct. 05: slides for Team Collaboration and for UML Diagrams available.
• Sep. 29: HW#1 due on Oct. 5.
• Sep. 23: a Design Document Skeleton available.
• Sep. 22: slides for Design Documents available.
• Sep. 14: slides for Course Introduction and Overview of UML available.
• Sep. 12: this website is the sole source of all up to date course information and syllabus; there will be no separate PDF version.

Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)
Guest Lecturers: Jeffrey CH Liu, Clement CW Su, and Jim CL Yu, IBM

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

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

Chi-Shiang Liu (劉啟祥), 3366-1205, Xloftywind@gmail.comX (between the enclosing pair of X's)
Jing-Jei Lin (林靖婕), 3366-1205, Xgrace6349@gmail.comX (between the enclosing pair of X's)

Object-Oriented Programming and Discrete Mathematics

Class Notes and Selected Readings

After an overview of the subject matters, we will study in great detail several software productivity tools, the UML, design patterns, and some fundamental elements of formal software modeling, analysis, and verification.

• Introduction (.5 week: 09/15a)
  Overview of software requirements, development process, design methods, and testing/verification
  [slides]
• Software Modeling: An Overview of UML (.5 week: 09/15b)
  Introduction, basics of modeling, overview of the UML
  [slides]
• Software Development Practice: Design Document (.5 week: 09/22a)
  High level design document, implementation level design document, user story (for Agile)
  [slides, A Design Document Skeleton]
• Software Development Practice: Modeling Tools (.5 week: 09/22b)
  RSA, basic UML modeling, conversion between source code and model
• Software Development Practice: Team Collaboration (1 week: 09/29)
  • Agile Development Process: Scrum, the Eclipse way, OpenUp
  • Collaboration Tools
    Source Code Version Control: Subversion, Git
    Project Management, Todo, Issue Tracking: RTC, Trac
    Continuous Integration: RTC, CruiseControl
    [slides]
• Software Modeling: UML Diagrams (1 week: 10/06)
  Structural modeling (class diagrams, classifiers, interfaces, packages), behavioral modeling (interactions, use case diagrams, interaction diagrams, activity diagrams), architectural modeling (collaborations, deployment diagrams)
  advanced structural modeling (object diagrams, components), advanced behavioral modeling (events, state machines, processes and threads, timing constraints)
  [slides]
• Design Patterns (Part I) (1 week: 10/13)
  Why design patterns, introduction to creational, structural, and behavioral patterns, GoF patterns
  [slides]
• Design Patterns (Part II) (1 week: 10/20)
  Introduction to enterprise systems, enterprise/cloud computing patterns, concluding remarks
  [slides]
• Software Security: Web Application Security (1 week: 10/27)
  Dynamic Web pages, client-side scripts, security vulnerabilities, vulnerabilities detection and prevention
  [slides: Web Programming, Web Application Security]
• Formal Logic: A Pragmatic Introduction (.5 week: 11/03a)
  Propositions, proofs, predicates, models, theorems
  [slides; notes:Natural Deduction]
• Formal Logic: Propositional and First-Order Logics (1.5 weeks: 11/03b, 11/10)
  Satisfiability, tautologies, validity, deduction/proofs, soundness, completeness
  [slides:Propositional Logic, First-Order Logic; notes: Tactics for Natural Deduction in Coq, exercise_prop.v, exercise_pred.v, exercise_group.v]
• Software Modeling: OCL (1 week: 11/17)
  Object Constraint Language (relation with UML models, values, types, expressions, objects, properties, collection operations)
  [slides; notes: OCL Examples]
• Software Modeling: Alloy (1 week: 11/24)
  Software modeling, simulation, and checking
  [slides]
• Software Verification: Model Checking (1 week: 12/01)
  Automata, automata-based model checking, linear temporal logic
  [slides: Automata-Based Model Checking, Temporal Logic and Automata]
• Invited Industry Talk (1 week: 12/08)
• Midterm (2011/12/15)
• Software Verification: Model Checkers (1 week: 12/22)
  Spin (Promela, never-claims), JPF (Java PathFinder)
• Software Verification: Hoare Logic (1 week: 12/29)
  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]
• Term Project Presentations (2012/01/05)
• Software Verification: Hoare-Style Verifiers (1 week: 01/12)
  Frama-C, Spec#

Homework 15%, Midterm 35%, Term Project 40%, Participation 10%.

1. The UML Resource, OMG.
2. The Unified Modeling Language User Guide, 2nd Edition, G. Booch, I. Jacobson, and J. Rumbaugh, Addison-Wesley, 2005.
3. Design Patterns: Elements of Reusable Object-Oriented Software, E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Addison-Wesley, 1995.
4. The OWASP Website. (Note: a website dedicated to Web application security.)
5. Object Constraint Language, OMG Available Specification, Version 2.0, OMG.
6. Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
7. Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (Note: follow the link to author's free download site.)
8. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
9. Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
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]
[Midterm 2010]