This course introduces a selection of theories and practices 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.

• 01/30: Grade Report available.
• 01/08: only those topics marked with an * are in the scope of the final exam.
• 12/31: slides for Hoare Logic available.
• 12/24: slides for Logic, OCL, and Automata-Based Model Checking available.
• 12/03: slides for Web Application Security available.
• 11/27: slides for Design Document and an example available.
• 11/19: HW#3 due on 12/03.
• 11/19: slides for Design Patterns and some code examples available.
• 11/05: slides for Team Collaboration and for Bluemix available.
• 11/04: Term Project requirements finalized.
• 10/22: slides for UML Diagrams available.
• 10/15: slides for Domain Model and for Common Patterns available.
• 10/08: slides for Enterprise Data Modeling available.
• 10/06: slides for Web Application Development available.
• 10/01: HW#2 due on 10/14 (design document) and 10/15 (demo).
• 09/26: slides for Eclipse and EGit available.
• 09/24: slides for An Overview of UML available.
• 09/17: HW#1 due 09/23.
• 09/17: slides for Version Control with Git available.
• 09/16: slides for Course Introduction available.
• 09/15: this website is the sole source of all up to date course information and syllabus; there is 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).

Jeffrey CH Liu (劉智雄, IBM), Wen-Chun Ni (倪文君, 叡揚), Clement CW Su (蘇志文, IBM), Scar Su (蘇瑞亨, 叡揚), Chih-Pin Tai (戴智斌, 創炎/Traiwan出來玩), Ming-Hsien Tsai (蔡明憲, Academia Sinica), and Ching-Lin Yu (游景麟, Mozilla).

Wednesday 2:20-5:20PM, Room 204, College of Management, Building 2.

Wednesday 1:30-2:00PM, Room 1108, College of Management, Building 2, or by appointment.

張子建, 3366-1205, Xr03725007@ntu.edu.twX (between the enclosing pair of X's).

Object-Oriented Programming and Discrete Mathematics.

Class notes and selected readings.

After an overview of the typical software development process and relevant issues, we will study several software productivity tools, the UML, design patterns, and some fundamental elements of formal software modeling and verification. To practice applying these methods and tools, we will carry out a term project that involves the development of a large Web application.

• *Introduction (.5 week: 09/17a)
  Overview of software requirements, development process, design methods, and verification
  [slides]
• Productivity Tools: Version Control with Git (.5 week: 09/17b) [slides]
• *Software Modeling: An Overview of UML (.5 week: 09/24a)
  Introduction, basics of modeling, overview of the UML
  [slides]
• Productivity Tools: Eclipse and EGit (.5 week: 09/24b) [Tips for Using Eclipse, EGit: Git for Eclipse]
• Web Application Development (1 week: 10/01) [slides]
• *Data Modeling (2 weeks: 10/08, 10/15)
  Domain Model: What and How (Abstract Models, Notations and Constructs, Basic Business Logics, Crossing Domains, Layers of Abstraction), Common Patterns, with Group Exercises and Discussions
  [slides: Enterprise Data Modeling, Domain Model, Common Patterns]
• *Software Modeling: UML Diagrams (1 week: 10/22a, 10/29a)
  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]
• Term Project Discussions (.5 week: 10/22b)
  
• Term Project Discussions (.5 week: 10/29b)
  
• Software Development Practice: Team Collaboration (.5 week: 11/05a)
  Agile Development Process (Basic Ideas, Eclipse Way, OpenUp, Scrum), Team Collaboration (Version Control, Issues Tracking, Rational Team Concert), Continuous Integration (Basic Ideas, CruiseControl), IBM Experience
  [slides]
• Software Development Practice: Cloud Application Development with IBM Bluemix (.5 week: 11/05b)
  Overview of Open Source project CloudFoundry and IBM Bluemix, Rapid Cloud Application Development with Composable Cloud Services, Integration with JazzHub (A web-based IDE and Git-Based version control system), Demo – building scalable cloud applications in minutes
  [slides; websites: Bluemix, JazzHub, The Lean Startup; inspiring article: A Cambrian moment]
• *Design Patterns (2 weeks: 11/12, 11/19)
  Why design patterns, introduction to creational, structural, and behavioral patterns, GoF patterns
  [slides; code examples]
• Term Project Discussions (.5 week: 11/26a)
  
• Software Development Practice: Design Document (.5 week: 11/26b)
  High level design document, implementation level design document, user story (for Agile)
  [slides, notes: An Example Design Document]
• *Software Security: Web Application Security (1 week: 12/03)
  Dynamic Web pages, client-side scripts, security vulnerabilities, vulnerabilities detection and prevention
  [slides]
• *Software Modeling: Formal Logic and Correctness Requirements (.5 week: 12/10a)
  Propositions, proofs, theorems, predicates, models
  [slides]
• Software Modeling: OCL or Alloy (.5 week: 12/10b)
  Object Constraint Language (relation with UML models, values, types, expressions, objects, properties, collection operations)
  [slides; notes: OCL Examples]
  Software modeling, simulation, and checking
  [slides]
• Term Project Discussions (.5 week: 12/17a)
  
• Invited Talk (.5 week: 12/17b)
  
• *Software Verification: Model Checking (1 week: 12/24)
  Automata-based model checking, linear temporal logic, Spin (Promela, never-claims), Java PathFinder
  [slides: Automata-Based Model Checking, Temporal Logic and Automata]
• *Software Verification: Hoare-Style Verification (1 week: 12/31)
  Axiomatic semantics of programs (assertions, pre/post-conditions, invariants), partial and total correctness, Frama-C, VeriFast
  [slides; notes: Rules of Hoare Logic, Proofs with Hoare Logic]
• Term Project Presentations (2015/01/07)
• Final (2015/01/14)

Homework 10%, Term Project 50%, Final 30%, Attendance/Participation 10%.

1. Git.
2. Eclipse, The Eclipse Foundation open source community website.
3. PHP IDE for Eclipse.
4. JavaScript IDE for Eclipse.
5. Bluemix.
6. JazzHub.
7. The UML Resource, OMG.
8. The Unified Modeling Language User Guide, 2nd Edition, G. Booch, I. Jacobson, and J. Rumbaugh, Addison-Wesley, 2005.
9. Design Patterns: Elements of Reusable Object-Oriented Software, E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Addison-Wesley, 1995.
10. Android.
11. The OWASP Website. (Note: a website dedicated to Web application security.)
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.)
13. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
14. 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.)
15. Object Constraint Language, OMG Available Specification, Version 2.0, OMG.
16. Software Abstractions: Logic, Language, and Analysis, D. Jackson, MIT Press, 2006.
17. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer-Verlag, 1995.
18. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzman, Addison-Wesley, 2003.
19. Spin.
20. Java Pathfinder.
21. Verification of Sequential and Concurrent Programs, 3rd Edition, K.R. Apt, F.S. de Boer, and E.-R. Olderog, Springer, 2009.
22. Frama-C.
23. VeriFast.

[Midterm 2004, Solutions]
[Final 2004]
[Midterm 2006, Solutions]
[Final 2006]
[Midterm 2008]
[Midterm 2009]
[Midterm 2010]
[Midterm 2011]
[Midterm 2012]
[Final 2013]