Week 1: January 15 - 16

• Lectures:
  • Course Administration
• Laboratory:
  • No quiz
  • No exercises

Week 2: January 19 - 23

• Lectures:
  • Course Overview
  • Sets and Relations
• Laboratory:
  • Exercises: Sets and Relations
  • Quiz: Sets and Relations
• Reading:
  • Hints to Specifiers, Jeannette Wing, July, 1995.
  • Formal Specification: a Roadmap , by Axel van Lamsweerde, in Future of Software Engineering (Limerick, Ireland). June, 2000. ACM Press.

Week 3: January 26 - January 30

• Lectures:
  • Alloy Tour (part a)
  • Alloy Tour (part b)
  • Alloy Tour (part c)
• Laboratory:
  • Quiz: Alloy Tour (parts a,b,c)
• Reading:
  • Jackson, Chapter 2

Week 4: February 2 - 6

• Lectures:
  • Alloy Tour (part d)
  • Alloy Tour (part e)
• Laboratory:
  • Quiz: Alloy Tour (parts d, e)
• Reading:
  • Jackson, Chapter 2
• Homework:
  • Problem Description
    Solution

Week 5: February 9 - 13

• Lectures:
  • Alloy Logic (part b)
  • Alloy Logic (part c)
• Laboratory:
  • Quiz: Alloy Logic (parts b, c)
• Reading:
  • Jackson, Chapter 3

Week 6: February 16 - 20

• Lectures:
  • Alloy Logic (part c)
  • Alloy Logic (part d)
• Laboratory:
  • Homework Discussion
• Reading:
  • Jackson, Chapter 3
• Homework:
  • Problem Description
    Solution
    Josiah Dodds' Solution

Week 7: February 23 - 27

• Lectures:
  • No lectures
• Laboratory:
  • Quiz: Alloy Logic (c,d)
• Reading:
  • Jackson, Chapter 4

Week 8: March 2 - 6

• Lectures:
  • Introduction to UML/OCL
  • OCL Basics
• Laboratory:
  • Quiz: OCL Basics

Week 9: March 9 - 13

• Lectures:
  • More OCL
  • Advanced OCL Expressions
• Laboratory:
  • Mid-term Exam

Week A: March 16 - 20 (spring break)

• Lectures:
  • (none)
• Laboratory:
  • (none)

Week 10: March 23 - 27

• Lectures:
  • Mining OCL Invariants from UML
  • Pre/Post-conditions in OCL and USE
• Laboratory:
  • Discussion on Homework 2, Mid-term Exam, OCL Basics Quiz
• Homework:
  • Problem Description
    USE
    CMD

Week 11: March 30 - April 3

• Lectures:
  • Design by Contract
• Laboratory:
  • Quiz: More OCL, Advanced OCL, Mining OCL Invariants from UML, Pre/Post-condition in OCL and USE
    Solution
    Alternative Solution

Week 12: April 6 - 10

• Lectures:
  • Introduction to JML
  • Introduction to Kiasan
• Software:
  • Kiasan
• Laboratory:
  • Kiasan Demo: Installation (OS X 64-bit, Linux 32-bit, Windows 32-bit)
  • Kiasan Demo: Walkthrough

Week 13: April 13 - 17

• Lectures:
  • More on JML and Kiasan
• Laboratory:
  • Quiz: Introduction to JML and More on JML and Kiasan
    Solution
• Homework:
  • Problem Description
    Solution

Week 14: April 20 - 24

• Lectures:
  • Kiasan's Analysis Engine (a)
  • Kiasan's Analysis Engine (b)
• Laboratory:
  • Exercises

Week 15: April 27 - May 1

• No Lecture
• Laboratory:
  • Quiz: Kiasan's Analysis Engine parts (a) and (b)
    Solution #1
    Solution #2
    Alternative Solution #2

Week 16: May 4 - 8

• No Lecture
• Laboratory (moved to May 5, 9:30-10:45am, N 127):
  • Wrap-up and Final Exam Review

Week 17: May 11 - 15 (exam week)

• Final Exam:
  • 2 - 3:50pm on Tuesday, May 12 (KSU Exam Timetable)