CMU 15-671Models of Software SystemsFall 1995
Seq Satisfies Set
Garlan & Wing Handout 11 9 October 1995
The motivation for this example is show you that when you do ``object-oriented'' programming, you are really identifying certain abstract objects (better known an data abstractions or abstract data types) like sets, stacks, queues, symbol tables, etc.. You eventually have to realize (i.e., implement) these objects in a real programming language in terms of either other abstract objects or the language's built-in data objects like sequences, arrays, records, linked lists, etc. After you write your (concrete) implementation you are then faced with proving it correct with respect to the (abstract) specification.
Not surprisingly, these data objects (abstract or built-in) can themselves be viewed as little state machines. So, to show the correctness of an implementation of an abstract object is very much like showing that one state machine (the concrete one) satisfies another (the abstract one).
There are other proof techniques used to prove the correctness of the implementations of abstract data types. You may see them in the Methods Course (when you learn about object-oriented programming) and/or the Analysis course (when you learn about program verification).