COMP 723 Course Syllabus

UNC-CH COMP 723

SOFTWARE DESIGN AND IMPLEMENTATION

PREREQUISITES

Undergraduate programming languages class, like COMP 524.
Exposure to basic software engineering concepts and practices as taught in COMP 523.
Mathematical maturity, familiarity with mathematical logic, predicate calculus.

COURSE GOALS

The overall goal of this course is to learn software engineering methods, both formal and informal, and to practice their use in designing, building, and validating (verifying, testing) practical software systems.

An auxilliary goal is to give the student a working knowledge of major ideas and concepts from the history of programming languages and software development, and to give some exposure to current topics in these research areas.

By the end of the semester, students will:

be conversant in the language of program design patterns
demonstrated a working knowledge of the the object-oriented paradigm for software design and implementation
demonstrate programming competence in either C++ or Java
learn and apply methods of systematic testing
demonstrate a working knowledge of the functional paradigm for software design and implementation.
acquire a working knowledge of the programming language ML
have exposure to programming in aspect-oriented languages
demonstrate an understanding of several formalisms and formal methods used in software engineering, including temporal logic and algebraic specification of ADTs
demonstrate an understanding of analysis via model checking and have implemented a model checker for a simple temporal logic
demonstrate a working knowledge of the foundations of programming language semantics (axiomatic and denotational)
have the academic background to follow current literature in PL/SE, design patterns, and formal methods

TEXTS

required (buy from Amazon, Barnesandnoble, booksamillion)
1. Design Patterns: Elements of Reusable Object-Oriented Software, Gamma, Helm, Johnson, and Vlissides; Addison-Wesley, 1995
interesting, perhaps useful, reading (but not required) ):
1. Elements of ML Programming, Ullman. Prentice Hall, 1994.

COURSE RATIONALE

This class is designed to teach the disciplined process of software development, from formal specification through to working systems. The student will learn graduate level material that presumes an undergraduate preparation in programming languages and software engineering. The material, therefore, is heavy on formal methods for supporting software development, which are founded on formal semantics of programming languages. While we are leaving a deep treatment of formal language semantics for advanced courses, we will introduce some semantics and verification in support of commonly used specification methods. It also presents disciplined engineering practices such as design and testing, and developing system architecture via design patterns.

The "software" part of the class covers specifications, design, coding, testing methods, and a look at methods for continuous improvement of the software development process. The overall goal is to give a broad introduction to SE techniques used in practice, along with an introduction to formal methods in SE and their current limitations.

The "languages" part of the class gives practical experience with module-level coding in different language paradigms, covering modern object-oriented languages (like C++ and Java) and modern functional languages (like ML or Haskell).

COURSE FORMAT

This course combines "pencil pushing" exercises with practical software construction. The class will have a midterm exam and a final exam. Your grade will be based on your scores on these exams, as well as your successful completion of homework assignments and programming projects. You will be given the requirements for various software projects. You will write specifications for the software in one or more specification notations, and will implement the projects. Coding will be in an object-oriented language for some of the programs, and in a functional language for others. You will organize into small study groups (2 students per group) for learning and practicing the methods we cover. Homework assignments will be submitted from each study group, but your exams will be done individually. Your programming projects will also be done individually unless specifically indicated as a group effort.

OUTLINE OF TOPICS

Below is outdated but i did not yet want to remove it from the info

This is intended as a rough guide; actual topics covered and order of presentation may vary.


1 week
   class goals, overview, summary of OO and functional methods
   software engineering, formal methods, and the development process

2 weeks
   intro to a significant formal spec language (like Z)
   expressing a significant design as formal specs


(A) 6 weeks (overlap)
   realizing a design in an OO language (like C++)
   design patterns
   large system design issues
   language run-time issues
   issues in systematic testing of OO programs (e.g., using axiomatic specs)

(A) 6 weeks (overlap)
   formal axiomatic specs (predicate logic, Hoare triples, WP)
   axiomatic verification
   Abstract Data Types (ADTs)
   axiomatic definition of ADTs
   canonical forms
   implementation of ADTs
   proof of ADT correctness/consistency
   use of ADT axioms in axiomatic verification


(B) 4 weeks  (overlap)
   realizing a design in a functional language (like ML)
   language run-time issues
   issues in testing functional programs

(B) 4 weeks (overlap)
   lambda calculus
   denotational semantics (Mill's specs/verification) 
   type theory


1 week
   others topics, as time permits and/or instructor chooses
     -- temporal logic and model checking
     -- trace specs
     -- statistical methods and the Cleanroom development process
     -- mutation testing