Computing task abstraction levels

• a problem/solution domain

• an input/output relationship

• data structures and algorithms

• a Java program

• virtual machine instructions

• native machine instructions

• circuit activity

• behavior of silicon, phosphorous, ink, …

Model-oriented Descriptions

Model-oriented descriptions express new structures in terms of previously known structures. For instance, if the set structure (i.e., no order and no repetitions) and its associated operations are already perfectly known, we can use that to build a model of a "list" structure where order is significant and repetitions are permitted. A list could be a set with two elements, one of which is an item (the first item of the list) and the other another set (the rest of the list) – so list <a,b,a> is modeled as {a, {b, {a,{}}}}.

The operation of concatenating lists would have a rather involved formal set-oriented description – to concatenate {x, X} with {y, Y}, we would have to look within X for its set member, and if that is not {}, look again within it, etc., eventually finding and replacing {} by {y, Y}.

Once described this way, an implementation of lists that does not use sets and set operations as its underlying structure is difficult to reconcile with the description.

Property-oriented Descriptions

Property-oriented descriptions express only essential properties without imposing an underlying structure for the new objects. For instance lists might have operations:

nil = the empty list,

cons(item, list) = new list with 'item' first and 'list' as rest,

head(list) = first item of 'list',

tail(list) = new list consisting of 'list' with its first item deleted.

Then for formal description of these operations:

head(cons(x,xs)) = x

tail(cons(x,xs) = xs

cat(nil,ys) = ys

cat(cons(x,xs),ys) = cons(x, cat(xs,ys)).

Categorizing Description Mechanisms

Methods for expressing formal descriptions are commonly categorized according to whether their primary approach is model-oriented or property-oriented. Some well-known examples are:

Initial Readings

Background

Although the most relevant discrete structures topics will be covered in class, basic material is an assumed prerequisite. If your background is sketchy, you should do an early active review of this material. One of the advantages of the Diller text is that it covers this material extensively (see chaps. 2, 3, 5, 6, 7 & 8).

Formal Methods Goals

There are links to several motivational "vignettes" on the course Web page that include pointers to further reading

Algebraic Specification

One of the disadvantages of the Diller text is that it does not cover algebraic specification. Recommended alternative sources are:

• the Goguen Web paper "Hidden algebra for software engineering"(see course Web page)

• the Yeh book (on reserve), especially chapter 4 by Guttag, et al

• Wirsing’s chapter in Recent Trends in Data Type Specification (on reserve)

• on-line documentation for the Miranda ADT facilities (see course Web page)