This page presents the material for CIS 771 lectures including lecture video, slides, examples, and answers to lecture exercises. For instructions on how to view lecture videos, see the Getting Started page.

Course Admistration and Overview

Course Administration

• Video: podcast
• Slides: .pdf

Course Overview

• Video: Flash, .mp4
• Slides: .pdf

Sets and Relations

• Video: Flash, .mp4
• Slides: .pdf

Alloy

Alloy Tour (part a)

Part A of a series of lectures covering the Alloy Whirlwind Tour chapter of Jackson's "Software Abstractions" book.

• Video: podcast
• Slides: .pdf

Alloy Tour (part b)

Part B of a series of lectures covering the Alloy Whirlwind Tour chapter of Jackson's "Software Abstractions" book.

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • alloy-tour-addressBook-b.als
• For You To Do:
  • 01-alloy-tour-b-fytd-1.als

Alloy Tour (part c)

Part C of a series of lectures covering the Alloy Whirlwind Tour chapter of Jackson's "Software Abstractions" book.

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • alloy-tour-addressBook-c.als
• For You To Do:
  • 01-alloy-tour-c-fytd-2.als

Alloy Tour (part d)

Part D of a series of lectures covering the Alloy Whirlwind Tour chapter of Jackson's "Software Abstractions" book.

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • alloy-tour-addressBook-d-1.als
  • alloy-tour-addressBook-d-2.als
• For You To Do:
  • 01-alloy-tour-d-fytd-1.als

Alloy Tour (part e)

Part E of a series of lectures covering the Alloy Whirlwind Tour chapter of Jackson's "Software Abstractions" book.

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • alloy-tour-addressBook-e-1.als
  • alloy-tour-addressBook-e-2.als
• For You To Do:
  • 01-alloy-tour-e-fytd-1.als
  • 01-alloy-tour-e-fytd-2.als

Alloy Logic (part b)

Part B of a series of lectures covering the Alloy Logic chapter of Jackson's "Software Abstractions" book.

• Video: Flash, .mp4
• Slides: .pdf

Alloy Logic (part c)

Part C of a series of lectures covering the Alloy Logic chapter of Jackson's "Software Abstractions" book.

• Video: podcast (watch in Quick Time Viewer, image view does not work in iTunes)
• Slides: .pdf

Alloy Logic (part d)

Part D of a series of lectures covering the Alloy Logic chapter of Jackson's "Software Abstractions" book.

• Video: podcast
• Slides: .pdf
• For You To Do:
  • 02-alloy-logic-d-fytd-1.als

USE/OCL

Background Reading

• OCL Specification: (pdf)
• USE Documentation: (pdf)

Introduction to UML/OCL

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • family-1.use
  • family-2.use
  • family-3.use

OCL Basics

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • academia-1.use
  • academia-2.use
  • academia-3.use
  • academia-basic-instantiation.cmd

More OCL

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • academia-4.use
  • academia-5.use
  • academia-extension1-instantiation.cmd

Advanced OCL Expressions

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • transitive-closure-1.use
  • transitive-closure-instantiation-1.cmd
  • transitive-closure-2.use
  • transitive-closure-instantiation-2.cmd
  • academia-7.use

Mining OCL Invariants from UML Class Diagrams

• Video: Flash, .mp4
• Slides: .pdf

Pre/Post-conditions in OCL and USE

• Video: Flash, .mp4
• Slides: .pdf
• Examples:
  • academia-9.use
  • academia-extension4-instantiation.cmd

JML and Kiasan

Background Reading

• JML Reference Manual
• Sireum/Kiasan for Java Manual
• Xianghua Deng, Robby, John Hatcliff. Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs (extended version). SEFM 2007: 273-282.

Recommended Reading

• John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson. Behavioral Interface Specification Languages. School of EECS, University of Central Florida, CS-TR-09-01, March 2009 (jmlspecs.org papers section)

Design by Contract

• Video: Flash, .mp4
• Slides: .pdf

Introduction to JML

• Video: .mov
• Slides: .pdf

Introduction to Kiasan

• Video: .mov
• Slides: .pdf

Kiasan Demo

• Videos:
  • Installation (OS X 64-bit, Linux 32-bit, Windows 32-bit): .mov
  • Walkthrough: .mov

More on JML and Kiasan

• Video: .mov
• Slides: .pdf

Kiasan's Analysis Engine

• Videos: Part A .mov, Part B.mov
• Slides: Part A .pdf, Part B .pdf