Formal Methods -- SE304/CS407

"But what good are formal methods? You know, in many cases, formal methods are just rubbish. Sometimes one gains more from simply having a friendly chat. Oh, the formal methods will always be with us, sir, you may be assured of that; but what good are they, in the last analysis, I ask you?"
-- Porfiry Petrovich (a character in "Crime and Punishment" by Fyodor Dostoyevsky).

Overview DBC CafeOBJ Links Software

Note for repeat exam

If you are repeating this exam in Autumn 2005, this is my advice. Work through the sample paper, and January's paper. All of the answers are available in the lecture notes (linked below). If you have worked through the lecture notes and still cannot find the answer to a question, email me at

mmcgaleycs.nuim.ie

Sample and Past Paper

Sample paper (.doc format)
January 2005 paper (.doc format)

Overview

The whole point of formal methods is to improve software quality. By carefully specifying what a piece of software should do before thinking about how it should do it, and by using mathematics to ensure that that specification is unambiguous, complete and consistent, we can avoid many of the most common software development errors.

This course aims to teach the basic concepts behind formal methods through Design by Contract in Java with JML and algebraic specification in CafeOBJ. The website for last year's course is still available.

All labs are compulsory, and contribute towards your continuous assessment mark.

The lecture slides will be available here after each lecture. Note that these slides are notes only, and do not necessarily contain everything you need to konw for the course.

Introduction

• Lecture 1 - Introduction

Design By Contract, JML

CafeOBJ

Links

• Introduction
  • The Therac-25 disaster, an example of just how bad software is, and how dangerous it can be.
• Design by Contract
  • Design by Contract in Java - Raymond Shanley
  • Thinking in Java Bruce Eckel
  • Design by Contract with JML - by Gary T. Leavens and Yoonsik Cheon
• The Irish Electoral System
  • Mathematical Aspects of Irish Elections
• Formal Specification, and CafeOBJ
  • The Construction of Formal Specifications: An Introduction to the Model-Based and Algebraic Approaches J.L. TURNER & T.L. McCLUSKEY

Software

• CafeOBJ for windows

Home