mit :: lcs :: tr :: MIT-LCS-TR-202

m

*

,,->.>= _ *< M , *. , - -

LABORATORY FOR
COMPUTER SCIENCE

MASSACHUSETTS
INSTITUTE OF
TECHNOLOGY

6

^

MIT/LCS/

D

m-202 /

A FORMALIZATION OF THE STATE MACHINE
SPECIFICATION TECHNIQUE

Robert N. Principato, Jr.

VS

545 TECHNOLOGY SQUARE, CAMBRIDGE, MASSACHUSETTS 02139

V

This blank page was inserted to preserve pagination.

MIT/LCS/TR-202

A Formalization of the State Machine Specification Technique

by
Robert Nelson Principato, Jr.

May 1978 "

. ■_•'■.-... ■:#%,■:,■•■■■ ■■•'■;. . •■'

.This research was supported in part by the National Science Foundation under grant
MCS74-21892 A01.

© 1978 Massachusetts Institute of Technology

Massachusetts Institute of Technology
Laboratory for Computer Science

Cambridge Massachusetts 02139

2-

A Formalization of the State Maohino Spootfioatton Toohniquo

Robert Nelson Princtpftto, Jr.

Submitted to the Department of Electrical Engineering and Computer Science

on May 16, i§78 m partial fulfillment of the lecuii e m s nu for (he

degrees of Master of Science and Electrical Engineer

Abstraot

This thesis develops the state machine specification Sschnique, a formal specification
technique for data abstractions based on Fames' work on speUffing software modules.
When using the state machine technique, each data object is Tiewfcd as the state of an
abstract (and not necessard* finite) state machine and, in the state maehine, this state set is
implicitly defined. The bask ilea is to separate IM operations of the data abstraction into
two distinct groups; those which do not change dw state but aNow some aspect of the stale m
be observed, the value returning or V -functions, and those which change the stale, the
operation or O-f unctions. The specifications are then written by stating die effect of each
O-functibn on the result of each V -function. This imphcttty defines the smartest ait of itiftfft
f&essary to dtstifftitsh thivl^tiblis^ the resoles ortM j V>fUiH|iift. H aho determines
the transitions among these states caused by the O-foncaon*.

An abstract model for the semantics of state machine specifications is presented Anal
then used to formalise the semantics of a concrete specification language. Furthermore, a
methodology for proving the correctness of an I mpl e m e ntation of a data abstraction specified
by a state rri&chlne is discussed and illustrated.

Key Words and Phrases: state maehine specifications, data iljrtiilh w is. formal specification
technique, proofs of correctness

Name and Title of Thetis Supervisor: Barbara H. Uskov

■ Aw>ctatg ProfeisereTCaanputer Science ar^

Acknowledgements

T wish to express my thanks to all the people who helped and encouraged this work:
to Professor Barbara Liskov who patiently read my many drafts and helped me clarify my
ideas; to Deepak Kapur who took the time to read several drafts of this thesis and made so
many valuable suggestions; to Bob Scheifler who taught me how to use ITS and wrote R
macros for me; and finally to Bart DeWolf and Frank Bamberger who helped me in the
early phases of this work.

4-

CONTENTS

o
Abstract • • **

Acknowledgements • **

Table of Contents 4

Table of Figures • 6

1. Introduction '

1.1 Motivation 7

1.2 Parnas's Approach to Specification 10

1.3 State Machine Specifications 13

1.4 Uses of State Machines 16

1.5 The Outline of the Thesis 16

2. A Model for State Machines * 8

2.1 The Basic Components of a State Machine 18

2.1.1 V-functions 19

2.1.1.1 Non-derived and Hidden V-functions 19

2.1.1.2 Derived V-functions 21

2.1.2 O-f unctions 22

2.2 The Semantics of a State Machine •••••• 23

2.2.1 The State Set of a State Machine 23

2.2.2 The Semantics of V-functions and O-functlons 25

2.2.3 An Induction Principle 27

2.2.4 Proving Properties of State Machines 28

3. A Language for State Machine Specifications . 32

3.1 The Syntax of ALMS 33

3.1.1 The Defining Abstractions 35

3.1.2 The Interface Description • 36

3.1.3 V-functions 36

3.1.3.1 Non-derived V-functions , 37

3.1.3.2 Hidden V-functibns ••••• 39

-5-

3.1.3.3 Derived V-f unctions 40

3.1.4 O-functions , 41

3.2 The Semantics of ALMS 43

*?•*£,• I. | "V vlfllv OOl t««««*a»«««^*#^«^««p««^«««cctttt««*«*e*««*«««««»**s«»«ese**«»*seeea Q>9

3.2.2 The Semantics of V-f unctkms and O-ftmcttens 01

3.3 An Example ........... 62

4. An Implementation Language fee* State Machine* . 57

*»• i An example ••••.•••••.••••.•.«•.••*• •••.•..^•. n .... a ....... ......... ..».•• .....••.«• SB

5 . Proving an Implementation Correot • ........... 05

5.1 The Concrete Representation ,..,..,,..«,.,..,,.„,..,,,... „ $6

5:2 The Ab*trsct Objects ^ ......,.^.,........ f .....!....,............„............ §7

6.3 The Nemomorpttlsm Property TO

©. An Extended Modal for State Maahine* ....... 73

6.1 Extensions to the Basic Components ««i*i,...». ..«..<*..».,«. ¥6

6.1.1.1 Non-derived nd Midden V-funcSion* ^„.. M . ? ,*.....„,...**B

6.1.1.2 Derived V-f unctions ....» 76

6.1.2 O-furicttdrts t......lf...^.................,...;.. 77

6.2 The Semantics of a Stater Machine ........i«...,^....;.;,«............ 76

6.2.1 Th« Stats Set of a 8taU MecMne :.^»^4^a^*,^....«^....^..«... 78

6.2.2 The Semantics of Vffunctions oad O- f uagt to ns ............... 7*

7* Conclusions 82

7.1 Evaluation ......,., ,. 82

7;2 Topics for Furtherftesearch U^...:i.....«.....^..J. 86

Appendix I. Undeoidable Properties of State Machines . 87

Appendix II. Proofs 93

References •• IOO

W* **/«£„,-,■,;. z4x.**> ^-*"* , »?' ■■

6-

FIOURES

Figure 1* Top and Push ».*•»...••».•••••••••••••• *2

Figure 2. Bounded Integer Stack 14

Figure 3. Non-derived or hidden Vrfunetten v ... 19

Figure 4. Derived V-f unction v 21

Figure 5. ©Hf unotldn o ........... . . . ■ ■ • ■ • • ....... 22

Figure 6. Symbol Table 34

Figure 7. Syntax of' a 'NftnHlii4t4||^ m . . ... 38

FigureS, Syntax of a HUdon V- f H netM n ........ 99

Figure 9. Syntax of a Derived V-funotion 40

Figure 10. Syntax of an 0*#un*%ta&i ........ . 41

Figure 11. Effects Function 48

Figure 12. Queue ................................. 53

Figure 13. Specif ieation of Finite Integer Set ... 59
Figure 14. Implementation df finite lnie)|er set .60
Figure 15. Variable •••••••••*»* • • ■ ■ ...*•* * • . • . . • • . OT

Figure 16. Array ............... .................. 94

-Figure 17. Specification of integer Set ......... . '74

Figure 18. ffeir^Hirrvee) eW- Hidden WWWtiim'v • • 75

Figure 19. Derived V-funotion v . . ... . . . . . ... . . . . • 70

Figure 20. O-funotlon o . . . .... . . . . . . ... .... ...... 77

figure 21. Turing^maohine^Vl^Jl ................ 89

Figure 22. Turing_^aohine_J*LJfc ............... 91

-7-
1. Introduction
1.1 Motivation

In the development of our understanding of complex phenom ena, the most powerful
tool available to enhance our comprehension is abstraction. Abstraction arises from tHe
recognition of similarities between certain objects or processes, and the decision to concentrate
on these correspondences and to ignore, for the present; their differences XHoare 72M. In
focusing on similarities, one tends to regard them as fundamental and imrhttic, and to Wew
the differences as trivial.

One of the earliest recognized and most useful aids to abstraction m programming Is
the self-contained subroutine or procedure. Procedures appeared as early as 1945 m Zuse's
programming language, Plancakulus [Knuth 761. Besides, earrf developers of programming
languages recognized the utility of the concept of a procedure. Curry, in I960, described the
advantages of including procedures in the programming languages being developed at that
time by pointing out that the decomposition nwchanism provkled by a procedure would aHow
keener Insight into a problem by permitting consideration of Its separate, distinct parts
[Curry 503.

The existence of procedures goes quite far toward capturing the meaning of
abstraction tLiskov and Zilles 741. At the point of Its invocation, a procedure may be treated
as a "black box", that performs a specific function by means of an unprescrtbed algorithm.
Thus, at the level of Its Invocation, a procedure separates the relevant detail of what It
accomplishes from the irrelevant detail of how it Is implemented. Furthermore, at the level
of its implementation, a procedure facilitates understanding of how it accomplishes Its task

by freeing the programmer from considering why it is invoked.

However, procedures alone do not provide a sufficiently rkh vocabulary of
abstractions CLiskov and Ziltes 753. Procedures, while well suited to the description of
abstract processes or event*, do riot accommodate the description of abstract objects. To
alleviate this problem, the concept of a data abstraction was introduced. This comprises a
group of related functions or operations which act upon a particular class of objects with the
constraint that objects in thij class can only be obterved or modified by the application of its
related operations (Liskov and Ziltes 75).

A typical example of a data abstraction is an Integer push demn stack. Here, the
class of objects consists of alt possible stacks and the cottectton of related operations includes
the usual stack operations, like push and pep t an .CfiqWBnn to ■■$**$* ;»** ***** ■«** ■■**
operation, top, to return the integer on top of the stack.

The set of operations associated with m.i^jt^m^^^-I^.W^ 1 *^ .if«*>^|
operations to create objects of the data abstraction, ,ef>ej»|ipjp§. mjm0kf,pfc&m<* $$■■#*&;.
abstraction and operations to obtain information about the structure or contents of objects of
the data abstraction. The first two categories of operations, which Include $#h and pap* jftpf
the constructors of the data abstraction. Operations in the last category are Jnfittry
operations as they provide information about the data abstraction. Top belongs to this
category.

Constructors can be further classified into two different groups; information adding
operations and information removing operations. Information adding operations place new
information in the data abstraction. For example, push if an information adding operation
for integer push down stack. Its complement, pop. is an information removing operation.

-9-

This type of operation removes information from an object of the data abstraction and
results in a new object of the data abstraction whose information content is a subset of *h*
information content of the original object [Kapur 783.

A data abstraction provides the same aid* to abstraction as a procedure and allows
one to separate the implementation details of a data abstraction f row its behavior. The
behavior of a data abstraction can be described by a sptdflattUm. A specif tcation of a data
abstraction specifies the names and defines the abstract meaning of the associated operations
of the data abstraction. It describes what the data abstraction does but not how it is done.
This latter task is accomplished by an InpUmentatton. An - im p lem entation of a data
abstraction describes the representation of objects of ihe data abstraction and the
implementation of the operations that act upon these objects. Though thtse different
attributes of specification and implementation are, in practice, highly Int e r d e pe ndent, they
represent logically independent concepts tGottag 751.

The main concern of this thesis is the speeMtjMto* of data abstractions.
Specification is important because it describes die abstract object which has been conceived
in someone's mind. It can be used as a communication medium among designers and
implementors to insure that an Implementor understands the designer's intentions about the
data abstraction he is coding [Liskov and Zilles 751.

Moreover, if a formal specification technique, one with an explicitly and precisely
defined syntax and semantics, is used, even further benefits can be derived. Formal
specifications can be studied mathematically so that questions, such as the equivalence of two
different specifications, may be posed and rigorously answered. Also, formal, specifications
can serve as the basis for proofs of correctness of programs. If a programming language's

semantics are defined fermaMy [Milne and Str&chey 763, properties of a program written tot
thts language can be f ormatty proved. T<MK0»fMMit!lCl^#i , «i^WjB9il **•» be proved
by establishing the equivalence of these pfopefttes and tmi specif fcattan. Finally,, formal
specif tcstkwu can be meaningfully processed byt a c om p uter LLiskov and ZiRes 1% tLftkov
and Berlins 77]. Since this processing can be dene in ad?aoce ef implementation. It can
provide design and configuration guidelines during preg*tm Juite p m iw L

1.2 Pnrnas's Approach to Speoifioatlon

The information contained in the specification of a data, ab*U*ctton can de divided
into a syntactic part and a semantic part LUskev and Z*8e* 75J. Tjbe syntactic part provides
a vocabulary of terms or syrobob that are used by the leaantk part to express the actual
meaning or behavior of the data abstraction. Two different approache* arc mod Mi
capturing this meaning; either an explicit, abstract model » i na g lUrt for the ctew of objtets
and its associated operations are defined in terms of this joodal, or the class of objects is
defined impncitly via descriptions of theoperattwIUstw aodZiJunTM-

Parnas tPawas 723 has developed a technjoue and notation for writing
specifications based on the impNeit approach. Hit ipecif s ta tion Kbame wet devised with the
following goats in mind [Parnas 72):

1) The specification must provide to the intended user
atl the Information that he will need tocotvotda-tise
the object specified, and nothing mere*

11

2) The specification must provide to the Implements* all
the information about the intended use of the object
specified that he needs to implement the specification,
and no additional InfornMition:

3) The specif icatton should discuss thi object specif led
in the terms normally used by user and implementor alike
rather than in some other arcs ©Y discourse.

When using Parnas's technique, each data object is viewed as the state of an
abstract (and not necessarily finite) state machine and, in Parnas's specifications, this state set
is implicitly defined. The basic idea is to separate the operations of the data abstraction Into
two distinct groups; those which do not change the; state oot a*** some aspect of the state to
be observed, the value returning or V-functUms, and those which change th* Wtti, the
operation or Of unctions. The specifications are then wften by stating the effect of each
O-f unction on the result of each V-functlon. This impHcftlr defines the smallest set of
states necessary to distinguish the variations in the results" of tne V-fonetkms f Liskov and
Zilles 751 It also determines the transitions among thele states caused by the O-Ponetlons.

Returning to the integer pushdown ^* exainplept^ &f '****

push. Top H a V-function that is defined as long *s the sfcefc h not' empty, and push it mn
O-f unction that effects the result of top. These dpeta^sW^ne specif led as hi Figure 1,
where depth is another V-function whose definition Is not shown hefe. out reflects the
number of integers in the stack. Quotes around a V-fn»ctsoaafe used to Indicate its vibe
after the O-f unction is executed. 1

A problem with this approach is that certain <3Nf unctions may have delayed effects

I. This interpretation of quotes differs from that in tParnas 72, 7H.

Figure 1. top and Push

top - V-f tmctJorrf ) ret*** VMptf

Applicability CendrtkWfc depth *

Hirnw »«•"■• 99SBB
•tKl top ...

push p OrfMnefoj**;* , t

Atfrffeabifrty emimm depth < Kw

Ef f «CU See*** lb* 1 * a
'dtpth' - depth + 1
end push

on the V-f unctions, to other word*. im^^I!!*!^.^.^^.^^ ctjtenred be *
V-f unction only after some Q-functien has been wed. For eaampai, push has a delayed
effect on <** in the sense thet after a new rtihieat baabewi pushed on the stack, the fawner
top of the stack element Is no longer observable by *e* but it W4* be. Jf Jef : is used.

Parnas used, en informs! ltnsj*efe W express these delated effects (Parnas 1*,m
in his spetff teat**.*, he included * »*c*», ceiled «**W **^^ fe* d**i«Jtoht.*a*eie*
ef/ects in English, at times interlaced »fth rtmpte mtt t>W»<etMi fernwrtae tParnas m Fat
example, to specify the Interaction of #mA end ^on » stack, Paroe* used the phrase "The
science PUrsH<aM»Ol> has, no net effect rf no enWf#«^€|nir"r^i»^7ll.

One method to fortnaHy describe delayed effect* h to inboduce hidden V-functtons
tP*ke 73) to represent aspects of the state which tie ndt km«^^ t ^m^^ «****"
V -functions are not operations associated with the data abstraction being ; defined. They a*e
tetrddoced to store values of other V-func#em and to ## ibanher thee sett* *ae
representational problems caused by defaced effects. Since they are not operations of the

- 13 -

data abstraction, users of the abstraction should not. be able to us* them. Aran example, In
the specification of a push down stack, one could introduce a hidden V-f unction stack to
store the former top of the stack element.

This approach has been followed by researcher! at the Stanford Research Institute
[Robinson 77], [Spitzen 763. However, their main concern with Parnas's approach to
specification is its use in a general methodology for the design, implementation and proof of
large software systems [Robinson 75), [Neumann 743. With this goal in mind, they have
designed a specification language, called SPECIAL, for describing Parnas-type specifications
[Roubine 76). But, no formal semantics have been provided for SPECIAL.

1.3 State Machine Specifications

This thesis develops a formal specif ication technique based on Parnas' Ideas. The
specifications written using this technique are called state mfklne specifications and employ
hidden V-f unctions. The specification technique described in this thesis is similar to work
being done at the Stanford Research Institute. No attempt is made to formalize Parftas'
notion of a modular properties section.

An example of a state machine specification is given below in Figure 2. Here, the
data abstraction defined is a bounded Integer stack with the following operations. Top is a
V -function that is defined as long as the stack is hot empty and returtis the top of the Stack.
Depth is another V-f unction that reflects the number of integers fn the stack. Ptish *nd pop
are O-f unctions that insert and delete, respectively, Integers from the top of the stack.

Notice that there are three different types of V-f unctions Included In the
specification. The hidden V-f unctions are used to represent aspects of the state that are *ot

-14

Figure 2, Bounded Integer Stack

bounded .stack - state machine It push, pop, tap, depth

depth - non-dertved V-# une«©n< ) return* Integer

Initial Vehie:
end depth

stack - hidden V-f ui>c«w^Wnte^er) re$vnf Integer
Appl. Cone*.: 1 s 1 s depth
Initial VeJur. u n de flaea; ,
end stack

top - derived V-func«io«( > return* integer
Appl. Qond.. ^deptb -Q).
Derivation: top - stadUdepth)
end top

pop - O-f unotion( )

Appl. Cond.: ~<depth - 0)
Effectf; 'depih' -^ep|h - 1
end pop

push - O-f «ne«h»h(45M«^»f^

AppU COjtd« depth < .Mp

''i^Hh:W*eP»i
'stack^epth + 1> - i
end push

end bounded jUck

immediately observable. Recall the delayed effect of jmsk on f»f. When a new element is
puahed on the stack, theformer top of stack element U no longer observable by top but it wHI
be If /*>/> is used. This value is stored in the hidden V -function rt«*. Hidden V-fujictiom
are not directly accessible to users of the data abstraction, but Hmlted access to them is
provided by the derived V -functions, which are defined in terms of the hidden and

- 15 -

non-derived V-functions. Non-derived V -function* are also accessible to users of the data
abstraction- They are inquiry operations that reveal intrinsic aspect* of the data abstraction
defined by the specif ication.

Note that the specification in Figure 2 uses two data abstractions, namely the
integers and Booleans, which are distinct from the data abstraction defined by the machine.
These data abstractions are called the defining abitractUms. They are not restricted to
contain only the integers and Booleans and can consist of an entire collection of data
abstractions. The defining abstractions are usually Jimple abstractions that are used to
construct more complicated state ; .machine specifications.

The defining abstractions are used in tbf domain and .range of the V-f unctions and
O-f unctions. They constitute the information that the O-f unctions, the constructors, add or
remove from the data abstraction. They are also the results that the V-f unctions, the inquiry
operations, return. The defining abstractions are assumed tajte defined elsewhere either by
state machines or schtw other forrnal specification technique.

The semantics of a state machine can be defined by giving the following
interpretation to the V-functions and O-functions. In every state of the machine, some
mapping is associated with each V-f unction. These mappings characterize the state. Th%
represent the information that the V-functioJW,reyeal about each , state,. In fact, since the
derived V-functions are defioed.in terim pT^

state of a state machine is completely characterited by ^jpa|pings of the non-derived ^and
hidden V-functions. The O-f unctions change the state of the machine by redefining these
mappings.

-16

| .4 Uses of State Machines

As was previously discussed, formal speclficatiom can ** studied matbematkalty.
So, state machine specifications can be used to prove properties of data abstractions or the
equivalence of different specif IcatlOM. Furtnewofe, they can be used as an unambiguous
communications medium among programmers due to their precisely drfh*d semantics. But
one of their most important Uses will be to serve as the balls for proofs of program

correctness.

Establishing program correctness can be described at a two step process with the
overall goal of showing that a program correctly implement* a concept that exists in
someone's mind. First, a formal description of the concept Is needed, this can be done by a
formal specification. Then, the program is proved eoOlvafcnt *o ibe specification by formal.
analytic means. tHoare 72al has described a method to accomplish this latter tas*.

However, Hoare's method requires some adaptations to meet the special needs •/
state machines. Accordingly, this thesis also discuss*) these changes and how to -fram*
proofs of correctness using state machines.

%J$ The Outline of the Thesis

Chapter 2 presents a model for the semantics of stale machine specifications. flfeat,
the basic components that every state machine must contaht are discussed. Then thwe basic
components are used to develop a model for the semantics of a stite machine. The
discussion in this chapter is abstract, presenting only the objects that the bask oanipomnt* of
any state machine must specify but not discussing an actual language to specify these object*.

-17-

Hence, the model developed is quite general and not tied to a particular specification
language. However, this model is restricted to state machines that only contain unary
operations on the data abstraction defined by the machine.

Chapter 3 details an actual specification language for state machines. It is a
complement to the abstract discussion in Chapter 2 and uses the model developed in Chapter
2 to formalize the semantics of this concrete specification language.

Chapters 4 and 5 discuss and illustrate a method to prove the correctness of an
implementation of a data abstraction specified by a state machine.

Chapter 6 extends the model for the semantics of state machines described In
Chapter 2 by lifting the restriction to unary operations.

Chapter 7 concludes this thesis with an evaluation of the work presented and some
suggestions for extensions to the state machine specification technique.

-18-
2. A Model for State Machines

Tlils chapter presents a model for the semantics of state machine specifications. In
Section 2.1, the basic components that every state machine spedffcatton must contain act
discussed. Section 2.1 only defines the syntactic constraints that a state machine sfjecsfieatfbn
most satisfy. Semantic issues concerning whether the machine is wefl-deftoed or consistent
are discussed in Section 2.2, wnkh shows how these baste co mpone nt s can be used to develop
a model for the semantics of a state machine, tim, each machine is modeMed by a set of
states, where each state is modelled by a set of functions correspondirtf to the hidden and
non-derived V -functions; O-f unctions drf^ne transitions between States.

The discussion here is abstract, presenting only the objects that the basic compo n ents
of any state machine must specify but not discussing »e "tettial language used to specify
these objects. Hence, the model developed fare is Ojuke genera) arid appikabfc to any state
machine specified using a combination of V -functions and O-functions. It is not, however,
applicable to state machines specified using something similar to Parnas's modular properties
section.

24 The Basic Components of a State Maehltie

The state machines considered here are specified using V-f unction* tUd
O-functions. In principle, one could define a state machine without any V-fimetlont. Sued
a specification, however, would be singularly uninteresting. Without V -functions there
would be no way to observe the state of the machine and, hence, ho way to distinguish one
member of the data abstraction defined by the machine from any other member. So, we

-19-

shall assume all state machines have one or more V-functions.

Furthermore, most interesting state machine specifications wiH contain one or mow
O-f unctions since, without O-f unctions, a state machine can only specify a data abstraction
containing exactly one element.

2.1.1 V-funotions

As was discussed in Chapter 1, there are three types of V-f unctions; the non-derived
V-f unctions and the hidden V-functions, which are primitive, and the derived V-functtona,
which are not primitive but are defined in terms of the other two.

2.1.1.1 Non-derived and Hidden V-f unction*

Non-derived and hidden V-functions are specif ied analogously. Each non-derived
or hidden V-f unction v has three sections in Its definition: a mapping description, an
applicability condition and an initial value section.

Figure 3. Non-derived or hidden V-f unction v

Mapcrmo Description: Dyi R v

Applicability Condition: % y : 8xD y -» Boolean

mitiai Value: injt v c{D v -» R v 3

First, let t A -> B3 denote the set of partial functions from the set A to the set B. In
each state S of the state machine, some particular mapping v$ from CD V _ -* R V J will be
associated with v, where D v and R v are specified by the V-function's mapping dtscription.

-20-

This mapping, of course, varies with the state of the machine. In general, the mapping
associated with v witt not be total As an example, hi Figure 2 of Chapter t, any mapping
associated with stack is a member of [integer -» integer!.

The sets I> v and R v ateo carry the following tt i puh i rton regarding the data
abstraction defined by the machine. In general, they wi* be the cartesian product
G| x ... x G n of a group of sets. But the C t are restricted so tlhi^fio elwient of thrdata
abstraction defined by the machine may he an element of any of die G|. This restriction
only allows the definition of unary operations on the data abstraction ipecifed by the
machine, For example, in the definition of the data abstraction **&§* M, it is not possible;
to define a function which computes the union of two sets. But, it is possible to define the
unary operation, has, which determine* if a -mrt^S^Uf^^Mli^.

Now, since the state of the machine is characterised by a set of mappings associated
with each non-derived and hidden V-functton, we can - v*bj* the state set S$ as a subset of

CD V , -♦ R v 3 x ... x (D v -♦ R-J * $

where ( v { v„> is the set of non-derived and hidden V -functions of the machine, to most

cases, M is a proper subset of $. This occurs when an n-tupta of $ contains, as an element,
a function that can never be associated with a non-derived or hidden V-f unction, iejr-
example, in the boundtd stack example of Chapter 1; a MiMtiitleji from the Integers into
the integers can never be associated with statk,

The applicability condition of a V-f unction governs when a call of that function bf
a user of the machine succeeds. This section specifies a partial function l v from $ x 0^
into the Boolean*. Hence, the success of a call depends on the state of the machine. For any
xcD v and St 56, W y (S,x) must evaluate to true for the V-f unction to return the value v$<X>.

- 21 -

where v s denotes the mapping associated with v in state S. When W v <S,x> equals falsa, v
returns an error condition.

The initial value section of a non-derived or hidden V-function v defines the
mapping associated with v in the initial state of the machine. This section specifies owe
member, denoted ini| y , of CD V -> R v l. In practice, for non-derived V-functions, )nlt y Is
usually a constant, total function.

2.1.1.2 Derived V-functions

A derived V-function v also has three sections in Its definition: a mapping
description, an applicability condition and a derivation section. The mapping description and
applicability condition are defined in the same manner and have the same interpretation as
the mapping description and applicabilty section of a non-derived or hidden V-functton.
The derivation section is unique to this type of function.

Figure 4. Derived V-function v

Mapping Description: D y ; R y

Applicability Condition: tf y :S x D y -♦ Boolean

Derivation: djr v such that <de£ v s >c[D v -» R V J for states S

The derivation section specifies the mapping associated with v in terms of the
mappings associated with the hidden and non-derived V-f unctions. This section defines a
function schema, denoted der v, expressed as the composition of the non-derived and hidden

- 22 -

V-f unctions of the machine and other functions associated with the elements of D v . The
particular mapping associated with the schema, denoted < der vg>, (iepends on the state S of
the machine, which contains an interpretation for the non-derived and hidden V-functtefis.
As an example, consider the derivation section of top in Figure 2 of Chapter 1. In any state
S, top returns the value stacHdtpth). This value is, of course, d e pend ent on the mappings
associated with stack and dtpth in state S.

2.1.2 O -functions

O-f unctions too have three sections in their definition. They are a mapping
description, an applicability condition and an effects section.

Figure 6. O-functton o

Mapping Oeac ri pU o n. D p

.AopMcjaJpttlty JCfJHnHlMk Mj 3? X .H* ■* JfflBlSWl
Effects Section: t^lx D *♦ $

In a given state, each O-fwnction Q ts a roen*er of ID, -♦ Ml, where D is given
by the mapping description and "SB is the state set of the machine. As wsth V -functions, B^
will, in general, equal the cartesian product of a group of sett G| x ... x G m which a*e
constrained so that no element of the data abstraction defined by the machine may- be an
element of any of the Gj. The range of the O-functton is net specified by the mapping
description since it is understood that the range of aH O-f unctions js the state set

-23-

The applicability condition of an O-function determines when the O-function
changes the state of the machine. As for V-f unctions, this section defines a partial function
W Q from $ x D Q into the Booleans. tf must evaluate to true for the. function to change
the state of the machine. Otherwise, an error condition is raised and the state remains
unchanged. For example, the applicability condition of pop Jn Figure 2 of Chapter 1
prohibits its execution when the stack is empty.

The effects section of an O-f unction specifies how the function changes the state of
the machine. This section defines a partial function Z Q from txD Into $.

2.2 The Semantics of a State Machine

2.2.1 The State Set of a State Machine

As was previously mentioned, a state of a state machine is modelled by mappings

associated with each non-derived and hidden V -function of the machine. Hence, we view

the state set, SS, of a state machine in the following manner:

SB c [D„ -» R„ 1 x ... x CD W -> R„ J - $
y l v l y n T n

where (vj v n J is the set of non-derived and hidden V -functions of the machine. 1 Note

that D v and R v are specified by Vj's mapping description.

Our purpose in this section is to define SB. Here, a constructive approach will be
used. Note that the initial state of a state machine is explicitly defined by the initial value
sections of the non-derived and hidden V -functions. '11 te, Q,, can generate the

state set by means of the following construction:

1. Recall [A -» B) - {f I f is a partial function from A to B)

-24

1) QJs an element of SB.

2> If S is an element of * and o i» an O-fupcUon call,

then the state S* obtained by applying o to S is an element of ft .

3) These are the only members of ft.

So, to define ft, it suffices to define the initial state of the machine and then to describe the

state changes caused by O-function calls or, Jn general, how an 6-fiiflcttan caN maps one

member of $ into another.

The initial state O. is the tuple <inj£ v ....JnJ&y > containing the mappings derived
from the initial value section of each of the non-derived and hidden V -functions (V|„..,v n }.

Furthermore, the next state function ha* the /oJJo*<ng del tnWOA.

Definition

Let o be an O-function with mapping V in its applicability condition

and mapping % in its effects section.

Let a<D n and'R<$.

'O

Then,

$ (R*> if f^R^-trua

NEXT(R,oa) -

tt%$B*k**fr*

Thus, the state set is generated as follows.

V Qcft

2) If R c $» and o is an O-f unction, then if NEXTlRjo*) Is defined,
NEXTMAahft wherea«D .

3) These are the only elements of SB.

-25-

In other words, the state set SB Is the closure of Q, under the state transition function
associated with the O-f unctions. Note that In 2) above NEXT<RAa> may be undefined.
This depends on the functions % and K Q .

Recall that £ Q is a partial function. So. it U pou&fc for some state 5 and x«D
that 5t (S,x> is undefined. Then, if « (S,x)-tru«, NEXT(Sax) would be undefined. TAtts
situation is undesirable since when W (S^)-tru«, a state change should occu«. Furthermore,
W is also a partial function. Here, it is possible for some state S* and n'tD^ that ■MjpijtV
is undefined, again making N EX T(S 'ax •> undefined. These two cotutderatiom lead us to
the notion of a well-defined state machine.

Definition

A state machine is well-defined if for any Si SB and O-f unction o

NEXT<S,d.a> is defined where acDg,

This definition guarantees that in a well-defined slate machine., for every

O-function o, V is a total function from SB x D Q into the Boolean* and % Q I* a total

function from {<S.a)cJp>.x D JV Q (S^)} into j£. This can be seen by inspection of the
definition of NEXT.

2.2.2 The Semantics of V-funotions and O -functions

With this definition of the state set SB of a state machine specification, it Is possible
to formally define the meaning of the O-functions and V-functions. This will be done by
defining mappings V-Eval for V-functions and O-Eval for O-functions such that

-26-

Y-Eval:* x NV -» [A -» R)
and

6-Eval:* x NO -» [A -♦ »

where NV is the set of V-ftmcrton names, A is the set of arguments, R U the set of results
and NO is the set of O-f tmcttoo names.

First, ft is necessary to destl with some rotational detail*. Here, the notation "%-*x,y m
has the value x if I is true and the vaftfc y if 1 Is fate, 't^h W^f w|* 6e used to raise
en error c©ffditton when a function's apptka&IWty cottdtoon it rtor satisfied.

O-Eval will be defined first. Now, given a state S and an O-f unction o, O-Eval
returns a function from D Q into SB U ( error} . So, using lambda notation,

0-EvaKS,o> - *aI« <S,a> -♦ NEXT<S.o»> .error3

O-EvaKS.o) is not necessarily total since either t 9 &*> or NEXT(S^a) can be
undef ined. However, O-EtaKS^ is always a total function in a wafl-defwed state machine.

For any V-f unction v and state $, V-Eval #HI return a function from D v Into
R v U ( error ). First, for a non-derived or hidden V -function v and a state S, recall that v§
denotes the function associated with v in state S. •Fheu for any non-derived or hidden
V -function v with applicability condition M y ,

V-EvaKS,v) - *a.[H' v <S,a> -» v s <a>. error3

-27-
Finally, for a derived V-f unction v with applicability condition tt y and derivation

der v.

V-EvaKS^v) - XalW v <S,a> ■* (der v s )(a) jrror]

Note that V-Eval(S.v) is not necessarily defined over the entire set D v since V y (S,a)
can be undefined or, depending on the type of V-function, v s <a) or < der v s Ma) can be
undefined when If v <S,aMrue. When this is not the case, we say the state machine Is
consistent.

Definition

A state machine is consistent if V-EvaKS,v) is a total function from D v

into R v U { error} for every state St g and V-f unction v.

In a consistent state machine, H v ' is always a total function from SB x D v into the
Booleans and v s or (der v s > is always a tout function from (xcD y I * v (S,xH into R y .

2.2.3 An Indttotion Prlnoipiei

Since any state of a state machine is generated by zero or more O-f unction calls, the
structural induction principle CBursUH 693 hokH here. In structural induction, proofs
proceed by course of values induction on the complexity of the structure, 2 which, for state
machines, means that to prove the data abstraction defined by the machine has property P.
one must prove that the initial state has property P, and rbat if all states produced by xero
through n-l O-function calls have P, the P is true after n O-function calls. This is one

2. The general schema of course of values induction on the natural numbers is:
P(0>, Vj(Vi«i<i a P(l» -» P<j» f- VkP(k)

- 28 -
advantage of the generative approach used in this model to define the state set.

2.2.4 Proving Properties of State Maekinon

Although it is not pest*>te to establish format? that a slate m a ch i ne specification it
correct with respect to our intuition, there are certain properties that a spectficaUon should
satisfy to enhance our confidence in its correctness. Two important properties of a stole
machine are whether or not it is well-defined or consistent m a w eti d e f ined machine, the
O-f unctions behave properly, either changing the state or Informing the user of an error. In
a consistent machine, the same is true of the V-f unction*. They either return a value or rait*
an error condition.

A state machine i» wehVdef Ined when NEXT J* a tota* function. This occurs when,
for every O-f unction o, * is a total function from * x D Q into the Boafeans and Z & is a
total function from «S^)c » x D 1 %J$#n into *.

Since & is defined generatively, a state machine can be proved to bo well-defined
by using structural induction. As outlined in Section 2»^S, tmV involves first showing that
NEXT(Q,,o,a> is defined for all O-f unctions o and a«D and then assuming

is defined for all a |C D , n*2 and then proving that

r*EXT<...r4EXT(r«XT(0.^»a 1 » 1 o^,.^a n r

is defined for all a ( cD . In practice, however, it may be necessary to straighten the
inductive hypothesis to simplify the proof.

-29-

A state machine is consistent when, for every V-f unction v, W v is a total function
from S5 x D v into the Boolean* and, for every non-derived or hidden V-functton v and
state Se5S, v s is a total function from (a I f P ¥ and * v <S,a>} into R v and for every derived
V-function v, <der v s ) is a total function from {a I at D v and W y (S,a>} into R v . All these
properties can be established by using structural induction in the manner outlined above.

In general, for most practical specif fcations, the task of proving ?hat a state machine
is well-defined or consistent is not extremely (tlfflcufl but rather tedious due to the many
cases that must be verified. The hardest step In a proof Usually Involves discovering an
inductive hypothesis that allows the proof to follow readily. These comment* are illustrated
by the example in Section 3.3 of Chapter 3 where a specification of a queue is shown to be
well-defined and consistent.

Note, however, that both the problems Of determining whether or not an arbitrary
state machine is well-defined and determining whether or not an arbitrary state machine is
consistent are undectdable. This situation arises since both problems can be reduced to the
halting problem for Turing machines CHennle 771. These tw results are established for the
specification language of Chapter 3 in Appendix I. However, they are not language
dependent.

The reductions for both problems are similar. Below, the reduction for the question
of determining whether or not a state machine is well-defined Is sketched. Here, we shall
actually reduce this problem to the blank tape halting problem whkh Is. In turn, reducible to
the halting problem for Turing machines [Hennie 773. So, consider a deterministic, one-tape,
one- head Turing machine T. T's computation on blank tape can be simulated by the
following state machine TUR.

-»-

TUR comtttt of the following functions:

taped) a Bon-derived V-f imct*9n to «0« Jth« cootenti

of ri wor* tape. foinalH;. the tap is entirety
Wsnlu

state a non-derived V -function te record Tt JPte.

aWOW w^» iHRHN SUnO Of- I •

htm *mMOM ■tyitiitilMU WkM tut 0mm or

Tsfn«d,ojN.toi^k'|pf,

move an O-ftmetten to earn ; out amjm)nTicqrtq$/ttkQ.

« stsjr m rm hhsvhir oaoaaae or wnwnsj ■ syuwoi

SjOUUj IB U Ww SBNC

AW of these foncttom's sp pnci b fflt v conditions c o nsi s t of a constant, total function
that returns the feoofcen value Iruu. ' Wow" reca* that a lu i ri e ^t t JIs a si of a tutihg machine
hafts when It reaches a state and input symbb? for wfcic* At function Is undefined.

'The function m move's effete section shai be undefined for iWf such pair. It wit! be
defined for every pair which continues 1*s cowputitl en. TtjR ttwuiitti T by having; a state
that corre sp on ds to each step in T$ computation. * '*

If T's computation when started on Manx tape hate, #uaVT wilt eventually reach a
state and input symbol for which its next state '''tiAtkim H undefined, .60, in TVR's
simulation of T, a state S of tt/R will be reached that co r tesp oO ds to this situation. Then,
by construction, MXT(S,move) is undefined so f UR is not w el l d e fi ned. On the other
hand, if Tttii is not welMefhted, the f tnict^
for some state $ since the function In move's apptteabmty amdloon is total fcy construction,

-31-

this corresponds to T halting. Thus, TUR is well-defined if and only if T does not halt
when started on blank tape.

-32-
3. A Language for State Machine Specifications

This chapter presents the syntax and semantics of a specification language for state
machines called ALMS (A Language for Machine Specifications). Section S.l describes the
syntax of ALMS and Section 3.2 discusses its semantics.

The discussion here is concrete, dealing with a specific language and its semantics.
This chapter is a complement to the abstract discussion In Chapter t. ft «ho#s how an actual
language can be used to specify state machines and how its semantics can be defined using
the model in Chapter 2 as a guide. The chapter concludes with an example discussing a
proof that a particular machine is weU-def teed and consistent.

ALMS is similar in spirit and approach to SPECIAL CRoubine 763, SRfs
specification language based on Parna*' approach. Howe***, there are significant
differences between the two languages. ALMS was developed setey to Illustrate how to use
the model In Chapter 2 to define the semantics of a state machine specfkJatton language. It
is a simple language and does not have the features nor the expressive power that would be
found in a specification language intended for use in the development of software systems.
For example, when using ALMS to specify a symbol table for a block structured language,
one can not define a V-function that returns the attributes associated with art Identifier in
the most local scope in which it occurs. This happens since ALMS contains no iteration or
recursion constructs. ALMS can be extended to have these features but this would be
beyond the intent of this chapter.

SPECIAL, however, was designed explicitly for specifying software systems. It is
intended to be used in conjunction with a methodology for the design, implementation and

-33-

proof of computer systems [Roubine 761. It naturally contains more features than ALMS. In
SPECIAL, there are more constructs for defining the effects section of O-f unctions and the
derivation section of derived V-f unctions. Furthermore, SPECIAL permits the definition of
greater than unary operations on the data abstraction defined by the machine.

3.1 The Syntax of ALMS

An example of a state machine specif teation, descrioed uimg ALMS, is given below
in Figure 6. Here, the data abstraction defined is a symbol table for use in a block
structured language. It has the following operations. Add it a O-f unction that places an
identifier and its attributes into the symbol table at the current scoping level. We assume
her* that an identifierjind Its. attributes. are character strings and denote this type by string.
The current scoping level is given by the non^derived Vrf unction lewl. It can be
incremented and decremented by the O-funcoons incjml and dtcjevel, respectively.
Retrieve is a derived V-f unction that returns the attributes of an Identifier in a given level
of the table and present? is another derived V-ftmctkm that Indicates whether or not an
identifier has already been placed into a given scoping level of the table. The functions Pj
and P 2 used in these two derived V -functions'! derivations are projection functions that
return the first and second components, respectively, of an ordered pair. They simply permit
one hidden V-f unction instead of two. Finally, tabtt_jtorag« is a hidden V-f unction used
for storage purposes.

This specification illustrates the three major components of a state machine
described using ALMS: the defining abstractions, the interface description and the
definitions of the V-f unctions and O-functions. The interface description provides a very

-34-
Flgure 6. Symbol Table

symboljable - state machine is add, Incjevel, dec Jevel, retried present?, level

level - non-derived V-f unction< ) return* integer
Afiph Cond.! true
Initial Value:
end level

table_storage - hidden V-function(a:integer4atring) regime string x Booleans
Appl. Cond.: true
Initial VatUK (don't <are,f*i*e)
end tablcjstorage

retrieve - derived V-f unction<a:integer4:string> returne string
AppJi Cond.: ^tae*jutt*j*4e%#*
Derivation: retrieve^) - Pj<table_Moraje(»4»
end retrieve"

present? - derived V-f unctkm(a:triteger4string) return* Boolean
Appl. Cond.: true

Derivation: present**,!) - P 2 <table_»torage<a4»
end present?

add - O-f unction(i,j:string)

Appl. Cond.: ~P2 (tab,e - storz S c(,eve M)>
Effects: 'table jtorage'|level4| ? -UAMIrt
end add

incjevel - O-f unction< )
Appl. Cond.: true
Effects: level* - level ♦ 1
end incjevel

decjpvel w O-f unction( )

Appl. Cond.: level >
Effects: 'level' - level - 1
end decjevel

end symbol Jable

-35-

brief description of the V-f unctions and CKfuncttom that users of the machine may employ.
These functions, along with the hidden V -functions, are fully defined in the body of the
machine. In these definitions, the defining abstractions are used. Here, they compose the
domain and range of the V-f unctions and O-f unctions and, further, through their
associated functions, help specify the meaning of the V -functions and O-functions.

3.1.1 The Defining Abstractions

As was discussed in Chapter 1, a state machine uses data abstractions that are
distinct from the data abstraction defined by the machine. These abstractions are called the
defining abstractions. They are assumed to be defined elsewhere.

In the remainder of this thesis, we shall use the integers, character strings and
Booleans as defining abstractions and associate the usual operations with them.
Furthermore, the set {*), where X is the empty string, will be used as the domain of nullary
V -functions and O-functions.

ALMS can, of course, have other defining abstractions besides these three. We will,
however, leave the actual collection of defining abstractions unspecified and only assume that
it at least contains the integers, character strings and Booleans.

Note also that the collection of defining abstractions can be augmented dynamically
in the sense that once a data abstraction is specified in ALMS, such as bounded attack in
Chapter 1, it can be used as a defining abstraction in other specifications. So, the
specification of a symbol table for a block structured language could use bounded attack in its
specification. We however chose not to do this for the symbol table in Figure 6.

-36-
3.1.2 The Intcrffto© Description

In ALMS, the interface description of a state machine provides a very brief
description of the interface that the machine presents to the outside environment It consists
of the name of the data abstraction defined by the machine and a Hst of the functions that
users of the machine may employ:

symboljabfe - etato machine la add. l«:Jev«id»«j\Jajifl # f(BWe*« p*«ie*t?, level
The list of functions contains the name of every non-derived V~f unction, derived
V-function and O-function in the machine. The names of hidden V-functions may not
appear in the interface description as they are not available outside the machine.

3.1.3 V-funotions

This section specifies the syntax for the three types of V-f unctions of a state
machine, the non-derived, hidden and derived V-fimctions. In the next section, the syntax
of O-functions is given. Recall that non-derived V-functions are primitive aspects of the
data abstraction defined by the machine. Hidden V-funettons are used to represent aspects
of the state that are not immediately observable and are inaccessible to users of the machine.
However, limited access to them is provided by the derived V-functions, which are defined
in terms of the non-derived and hidden V-functions.

Throughout this section and the next, it wiH be necessary to use expressions. An
expression is formed through the composition of the non-derived and hidden V-functions
of the machine and the functions associated with the defining abstractions. It may also
contain elements of the defining abstractions and formal arguments. The formal arguments

-37-

serve at place holders in the expression.

We now turn to th« definition of an
though all expressions were written f(...) although w* .^W,
infixes such as + in examples.

1) An element of a defining abstraction or a fonwrtsNfMnent is an expreiiion

2) If e,, .... e^ are expressions and f .J* a iisf^rtffd V-f ufKOian Of SM, a hidden
V-f unction of S*£ or a fimction associated w^^ ^ f
requires n arguments, then f^..^ [}* an expression.

Wi shall also refer to expressions by the type of value they return upon evaluation.
For example, a Boolean expression evaluates to either troo or 'IfoJoo. ' Note that this
definition excludes derived V-f unctions from spewing in an expression. This rettrktion Is
made to simplify the semantic definition In Section 12. In {srlnds^ there Is no difficulty In

a Ito wing derived V-f unctions to appear in expressions.

3.1 .3.1 Non-derived V-f unction*

f he gerieral scnema for defining non-derived V-fuoctions is given beta* In
Figure 7.

the mapping dtstrtptUm df a non-derived V-functJon specific* tu name, domain
and range, phis the fact that it ii a non-derived V-f unctton. Its syhtax is
nam - non-derived V-fimottoof ) retufnet,.

-38-

Rgure 7. Syntax of a Non-derived V-f unction

nam - ff&r*o^fi^V*fiiM<^
Appl. Cond.: Boolean exf
WM»alVf*ia:fntt
•nd n««*

where t r and t, are nanws of defining abstract torn and iw

•—T"

for nuilary V -functions such as level in Figure 8 and

name - nbn^d^^tff-fiiineMtx^^x,,^) #§*!**• tf
for n-ary non-derrVed V-f unctions such as has in Figure ft or* Chapter 4.

Here, t r the name of one of ftSi defining «b*racflons, U the equivalent of i v of
Section 2.1.1. It is sometimes referred to as the type of the V -function ^Tb* Xj |re the /ormo/
arguments of the Y-f unction. They must be distinct. Abo, t 4> again the name of a defining
abstraction, is called the type of the formal argumernxj.

For a miliary non-derived V -function, p^.i^J^^^^n^Tj^i^j^i^
V-functkm v, Dy is tj x ... x t n . ^ i

For example, consider the mapping description of level in Figure 6.
level -non-derived V-f imctlonX ) rohsrn* integer
Here, D leve , - {*> and R teye< - hrteger and. hi toy state, the fuoctlon associated with level
is a member of t(X) -* integer!!.

The applicability condition of a non-derived yJwt&^, x .0mfa*.-.-f Boolean
expression that determines the success of a call to the function- Tb^t, ex||fe*«fc*» 7 n*Mt Jie tfpe
correct. This means that whenever an object is uaa|Jn;the expression, its type must be

-39-

compatible with the type expected at that location. Furthermore, this expression must only
contain formal arguments that appear in the V -function's mapping description.

The initial value section of a non-derived V -function specifies one element of R y or
contains the special symbol undefined. This restricts the mapping associated with the
V -function in the initial state of the machine to be either a constant, total function or a
totally undefined function. The latter case Is specified by undefined.

3.1.3.2 Hidden V-f unctions

Hidden V-f unctions are specified in an analogous manner to non-derived
V-f unctions. The only difference occurs In the syrttax of the mapping description which
contains the special symbol hidden instead of n on e eilved .

Figure 8. Syntax of ■ Hidden V-f unction

name - hidden V-functlon<xj:ti;...;x r| :t t| > returns t,.
-■■ *p&. M^vWbae&ikxpriistoi y -- :U -
Initiel Value: init

■ eno nonu -

where t r and tj are the names of defining abstractions and intatj U ( undefined)

-40-

343.$ I) wived V-funotions

The three sections in the definition of a derived V-funetidh ire defined as foftows.
the mapping description only differs from the mapping description of a non-derived or
hidden V -function by use of the special symbol non-derived. The appitcabiitty condition
exactly follows the syntax of the applicability condition of a non-derived or hidden
V-f unction. The derivation section is unique for this type of function.

Figure 9. Syntax c»f a Derived V-function

name ~ derived \! -f uncttonf* jrt^^x^,,) roturo* t r
Appl. Cond.: Boolean expression
Derivation: def tiNng cfcuae
end name

where t f and t { are names of defining abstractions.

The derivation section of a derived V -function ...a *4#fMt ji *§*»* that defines v In
terms of the other non-derived and hidden V-f unctions in tea m a chine . Its syntax Is
described as follows.

If a derived V-function v has formal arguments xj, .-, X n and ty>e t r , then the
derivation section of v is of the form

Derivation: v(xj,...,x n > - e|
or

Derivation: if b then v(x| x n > - e t etee v(xj,...,x n > - e 2

Here, & is a boolean expression and e t and t% * T * expressions of type t r Again,

- 41 -
these expressions must be type correct and only use formal arguments of v.
3.1.4 O-f unctions

The general method of specifying an O-f unction is shown below in Figure 10.

Figure 10. Syntax of an O-f unction

name - 0-functlon<Xj:t|;...;x n :t n )

Appl. Cond.: Boolean expression
Ef facts: equaUonj

equation m
end name

where tj is the name of a defining abstraction.

The mapping description specifies the domain of the O-functton and Identifies the
particular function as an O-f unction. Its syntax is

name - O-f unction( )
for nullary O-f unctions such as pop in Figure 2 of Chapter 1 and

name » 0-fttnctfon(xj:t|;...;x n :t n )
for n-ary O-functtons such as srfrf in Figure ft* He** tjpJa the name of a defining
abstraction and the Xj are the formal arguments of toe O^functtoa. They must be distinct
Also, tj is the type of the formal argument X|.

For a nullary O-f unction, D Q is M. For an n-ary O-function o, D Q is t| x ... x t,,.

-42-

Thc range of the O-f unction is not specified fey the mapping ....description since te is
understood that the range of any O-f unction is the state set of the Hate mtmlMm.

The applicability condition of an O-f unction contains a Boolean expression.
Naturally, this expression must fee type correct and only COtttam fojv^ atfuments from the
O-f unction's mapping description.

The effects section tit an O-f unction contains a group 0,:^0^^ : ^%f0^$t hew
the mappings associated with the non-derived and hidden V-functions are changed fey an
O-function call. There are two types of equation*; stntpst equations and conditional
equations. A simple equation in a state machine SM is dieted » follows.

1) Let v be a nullary non-derived or hidden V-f unct i on Of *M having type t and
let e be an expression of type t. Then,

V-e

is a simple equation.

2> Let v be a n-ary <n>0) non-derived V-functkm or hidden V-function of SM
having type t with former arguments Xj of type t|. New let e fee an expression of type t and
ej be expressions of type tj. Then,

•vHej^.^) - e
is a simple equation.

The quotes are used to represent the result returned fef the V-functton sifter
completion of the Of unction call. An unquoted V- f u mU on ■ d enotes the value returned
before the O-f unction call.

-43-

A conditional equation employs simple equations in its definition. Let eqj and ecg
be simple equations and let * be a Bootean expression. Then,

if b theneqj
and

if * then eq t e4»e eq 2
are tondltterM equations. Note that tbte defmttton prohibits nested conditional equations and
blocks of equations following the fftn or Ww/ These wstrkrtons were made onh; to slmpHfy
the semantic definition in 5ectk>n S.2. No problems would arts* if the restriction* were lifted.
Finally, the effects section of an O-f unction contains a Hsttng of conditional and
simple equations. Its syntax is
Effects: eqj

«»m
The ordering is immaterial. Of course, all expressions in the effects section must be type

correct and contain only formal arguments of the O-f unction.

3J2 The Semantics pf ALMS

3.2.1 The State Set

As was previously mentioned in Chapter 2, a state of a state machine is completely
specified when the mapping aswdated withes^ nor^CTlved and hidden V -function of tie
machine is given. Hence, we view the state set, M, of a atale machine in the following
manner:

-44

SSc [D Vi -♦ R v .l X ... x ID- -♦ R-J> &
where {V|,...,v n } is the set of non-derived and hidden V -function*. Note that D yj and R^
are defined in Sections 3.1.3.1 and 3.1 3:2.

Our purpose in this section is to defme #: Hire, we shall use the same approach
outlined in Section 2.2.1, taking the transitive closure of *he Initial Mate Q, under the stale
transition function. So, to define J5, it suffices to define the initial state of the machine and
then to describe the state change caused by an O-f unction call.

The initial state Q, is the n-tupte ( inity r . Jnit T > where {v,,...,v n } is the set of
non-derived and hidden V-f unctions of the machine and

4> «f v,V initial value section

contains the viprd undefined

in it

v l

{(a,b) I ac D v ) if v,'» initial value

contains be R v

Here, <V is the null set. Note that functions are represented as sets Of ordered pairs.

To define the next state function of a Jta*e machine, K is neceisarj to define, hi
general, how an O-f unction call maps one member of $ into another. This mapping is done
by the O-f unction's effects section and we now turn to describing {he meaning of this
section.

The basic components of an O-f unction's effetts section are the expressions that are
used to buHd the simple equations and the conditional equations. These expressions are
formed by composing the functions associated with the defining abstractions and the

- 45 -

non-derived and hidden V-functibns of the machine. So, (he "'first step in defining the next
state mapping h to specif y the meaning of nSete expressions. This will be done by defining
a function t» that evaluates an expression. "T^nln^ using ; j^ #wttTbe possible to describe the
effect of a single equation. This will be done in the definition of a function E that specifies
how arr equation changes the mapping associated with a V-TOncflon. Finally, the total effect
of the effects section will be specified by a function TE which, using E, combines the effect
of each equation in the effects section.

The meaning of an expression is dependent on ; two items, first, if depends on tin*
particular O -function or V-function caH since, in cnifral, the expressions wilt contain formal
arguments from the function's definition. AtM^jhM*^^

arguments. Second, the meaning of the expressions deDends on the, member Rt,% since ,R
gives an interpretation to the non-derived ami hWden V-functions. Note that tint functions
associated with the defining abstractions have a constant fixed interpretation and are
independent of members of %

So, let Re $ and let w be an O-f unction or V-f unction with expression E appearing
in «'s definition. ' Finally, let <a|,...,a n >€D # . Then to find the meaning of expression E, we
can proceed as follows.

1) First, substitute aj for every occurrence of its corresponding formal argument in
E, obtaining E*. Note, if D m - M, this step if unnecessary since •» has no formal
arguments.

2) Now, to evaluate E*. we shall view R as an interpretation or environment that
specifies, for each symbol A, the value A R of A in R. If A is an element of a defining

- 46 -

abstraction or one of their associated fuftctiofts, then A D is simply A. If A U a non-derived
or hidden V -function, then A R is the function associated with A JH K. Tht vahie of
E* - AiEi^E^) in R, following [Pratt 773, wilt be denoted br R ► E* and l» defined by

R ► A<Ej... ( E k ) - A^(R ► Ij^R J» Ejj)
Since the non-derived and hidden V -functions may not be assocteted With total functions In
R, it is possible that R * E* is undefined.

Thus, as outlined above, we can define a semantic ftmctten |*<R r E,«,a> for Re 56,
expression* E th *#*s definition and a«U # such that

*<R,E,w,a> - R> E*
We rnehide the O-f unction or V-f imctkm name • « i parameter to gaf since it describes how
to substitute the actual arguments for the formal argument.
Now, let Rf^aMconsWer the simpfe equation

v<#> - (f
appearing in an O-f unction o's effects section. Then any cat! of a) of o, where ai^ ******
change v R & tftefuhctfdn

w(RjAa) if x - !**,*&*#

v R *(x) -

v R (x) If x x 0&jk#tf

Here, a new value is returned for the argument piRjKfl*) and, otherwise, the old value is
returned.

-47- .

To help indicate such a function, we shall use the notation "V»x,y" developed in
Chapter 2. Recall this notation 4tas tht value* if Hs true and value y if fc to false. So,
for v R * above, we have

v R * - Xx.[(x-i«(R,a,o,a)) -♦ p(RJJ,o^),v R (x)]

Using this notation, we define in Figure 11 an effect! function

E(R,o3,Eq)
that specifies the change caused by an equation £q on a V-f unction. E returns the new
mapping associated with the V-f unction. It shows the effect of a single equation and not the
entire effects section. So, in general, E can not be observed outside the machine.

The definition of E characterizes the expressive power of the effects section. If one
wished to increase the expressive power of ALMS by adding constructs such as a wKUt or for
all statement, the definition of £ would have to be extended. In fact, this is the only
definition that would, require modification. Both p and TE would remain unchanged.
This new definition of E could use the definition in Figure 11 as its basis. Th* effect of the
new constructs could be defined in terms of the effects of their simpler parts in much the
same manner as the effect of the lf-thtn-elst statement in Figure 11 to given in terms of the
first two clauses of the definition.

To define the next state function, we must combine the effect of all the equations in
the effects section. This can be done by calculating EfR.o.a.Eq) for every equation in the
effects section and then combining these mappings into a new state.

-48-

Ffgure 1 1 . Effects Function

Definition

Given a state machine specif fcallon S*f aAd Rt$,

let o be an O-f unction of SM with Eq appearing in o's effects section and acD„.

Then E(R,o,a ( EqHi defined as follows;
i) If Eq is a simple equation of the form V - e where v is a parameter-less V-function,

E(R,o,a,Eq> - {(X.i^Raoa))}
ii> If Eq is a simple equation of the form Vfw) - t , then

E<R,o,a,Eq> - XxI<x«t*(R,w,o,a)) -* |t<R,«,o,a),Vn(x)3
Hi) If Eq is a conditional equation of the form i/c then s where s is V - « or V(«) - «,

EtRAaj) if 1 tt(R^A*> - tros

E(R,o,a,Eq) - ^-, ,jk " >;-.

v R if tf(R,CAa> - f also

iv) If Eq is a conditional equatiotipf thtform? #,ff*iji s^«ip^p#|tn .n - .

E<R,(vu/) if ttCRiAa) - tru*

E(R,oa,Eq) -

E(R,o,a r i2 ) tf fsJR^/Oi*) - f«la«

-* ... . . i ii i ' in i i m ■■!■! ii ■nan n mi i iiiii^i^miii^iiii iMiiiim iiTT-in— r-TT-n 1 '

First, define the function

(a (n , ?l a k |,c,a b (»~^yf, s If tetsn.

t/ n «a, a n ),i,c) -

(a, a B ) if i^Oor i>n

where i is an integer and (a, a„) is an n-tuple. This function changes the lib component

r^^r-^-H'---

-49-

of the n-tuple to c.

Now, let o be an O-function with equations E^ rt JE^ In its effects section and let
a€D Q . Furthermore, assume

Rc$-[D V -» R v ] x ... x [D„ -♦ R w ].

Finally, let/j - E(R,o,a,Eq,) and let

k if E(R,o^,Eqj) changes V-function v^'s mapping

Ji-

n+1 . if E(RAa^) doesn't change any V-f unction's mapping

Then the total effect of the effects section it given by

TE<R A a ( Eq 1 ,..,Eq <n > - u .W&J*4kW4tM-*b*fnt

Note that a V-funcMon not effected toy ah equation Eq, retains the previous
mapping asociated with it. TEcR.o^^.-.^Eq^) corraporKl* to & <R,a> In Chapter 2. So,
we can define the next state function as follows.

Definition

Let o be an O-functton with Boolean expre ss ion t in Its applicability condition

and equations Eq|,...,Eq fT1 in its effects section.

Let a<D and R<$.
Then,

TE(R^a,Eq 1 ^^q (n ) if f«<R,taa>-tru«

NEXT<Rmi> -

R if »t(R,fcAa>-f«ta»

So, the state set can be generated as in Chapter 2.

50-

1) <i««.

2> If Rf * tnd o is an O-f mwttao. rtwnlf NEXT(R^) Is defined,
NEXT(R,o,a><# where at D Q .

3) These are the only elements of ft.

Again, we must consider the question of whether or not N£Xf is well-defined.
This is dependent on * and TE. Recall that at is not Mcessaritf a total function. So, it is
possible for some state S and x« D that tf$M*) "* undefined. Also, T*£ b not necessarily
total so we can encounter a similar situation. These two cases co r r e spo nd to the problem,
discussed in Chapter 2, when V ($,je) and St^fSMe* ere undefined.

Besides the totality of TE, there U a further p*oMm* that we mtt* consider. We
have defined the ordering of the equations Eq lt ...,Eq m as immaterial. However, ft is possible
for some state S and a€D Q that Tf&Aa.Eq,,...,^) * ttOg^^^i^^ where #
is a permutation from il,...jml onto iK.j&. mm mm, Y&w«tt*sT be ftoodeterministic or
not uniqyeiy defined in the sense, that its value depend* •* the choree of the order of the
equations Eq^..,Eq m .

To handle these situations, we must introduce the notion of a weH-deflrted state
machine. Due to the last case, the definition diff«is-«hghtl|t from tNattrf Chapter 2 since vre
must explicitly guarantee that TE is uniquely defined whereas in Chapter 2 this war
unnecessary since by definition % Q was a function.

-51-

Definitton

A state machine SM is well-defined if for any Si SB, O-f unction o

and ae D Q

both 1) NEXT<S,o,a) is defined

and 2> TRSAiXq!^. J% 1 > - TE<SAaJEVl>-"*W

where equations Eq^-.E^ appm m oY effects section

and w is any permutation from il r ..jm) onto {l„./n}.

3.2.2 The Semantics of V-f unctions and O-funotions

With this definition of the state set SB of a state machine specification, it is now
possible to formally define the meaning of the O-f unctions and V -functions. As in
Chapter 2, this will be done by defining mappings V-Eva! for V-f unctions and O-Eval for
O-f unctions.

O-Eval will be defined first. Now, given a state S and an O-function o with
Boolean expression ft in its applicability condition, O-Eval returns a function from D into
% U ( error ). So, using lambda notation,

Q-EvaKS,o) - Xa.t|t(S,ft,oa) -♦ NEXT<S^a) J crror]

Again 0-EvaKS,o> is not necessarily total but m a well-defined state machine this is
always the case.

For any V-function v and state S, V-Eval wiN return a function from D v Into
R v U {error). First, for a non-derived or hidden V-function v and a state S, recall that v s
denotes the function associated with v In state S. Then for any non-derived or hidden
V-function v with expression ft in its applicability condition,

V-EvaKS,v) ■ Xa.tit<S,ft,v,a) -> v $ (a).error]

-52-

Flnaliy, for a derived V-f unction v with expression I In Its ■f^MAMhV condition,
there are two cases.

i) If v's derivation section contain* **,,.,,*„)« «, then

V-£vaKS,v) - >aIst<S,i,v,a> -♦ n(Sur.v.a) jerrori

li) If v's derivation section contains tf c then Mx t ,...,x n ) - * f *f*» af*;,...^,,) - *%,
then

V-EvaKS,v> - Xa,[|t(S,*,v#) .-» Css<&c,**> ^ *»#W>4*flb*f»»*H*fflatl

As whs mentioned m Chapter 2, V-EviKs\v> * he* MMHMH^ i «MM fahttloh froth
D v into ft t U ( error) . When this is not the case, wt say Hie Kate machine it consistent. , t he
definition Is the same as in Chapter 2.

3.3 An Example

In this section, we outHne a proof that a partfctffcr state machine Is well-defined and
consistent. The full details of the proof are contained hi Ap p end!* 2. Othr examp*
specification Is illustrated in Figure 12. This data abstraction is a queue with three
operations; tnmt which adds an integer to the rear of die queue; etttf* whkh removes the
integer at tr»e front of the queue and first tlmtnt which returns the integer at this front of
the queue. The hidden V-f unction storage is used to store the ehtitwnu of the queue. From
and fcrcfc point, respectively, to the beginning and end of the queue. Note that this queue can
hold an arbitrary number of integers.

-53

Fhjttre 12. Queue

queue - state machine is insert, delete, firstjelement

f irst_element * derived V-functton< ) returns integer
Appl. Cond.: «(f ront - back - 1)
Derivation: firstjelement - storageff ront)
end f irstjstertwnt , ^

front - hidden V-f unctiont) returns integer
Appl. Cond.: true
Initial Value: -1
end front

back - hidden V-f unetionC) returtw Integer
Appl. Cond.: true
Initial Value:
end back

storage - hidden V-f unctiorrfhJnteger) returns Integer
Appl. ContM ftsent fc i £ back
Initial Value: undefined
end storage

insert - 0-function(i:integer>
Appi. Cond.: true
Ef foots: 'storage'<back - 1> - I
"back' - back - 1
end insert

delete - O-f unction< )

Appl. Cond.: "(front - back - 1)
Effects: 'front' « front - 1
end delete

end queue

-54-

We shaW first stow that the specification to weH-defmeA Tbi* wiN be doe* by
proving a lemma that capture* the key prepeftle* mania re to insure that the
machine is weft-defined. Informally, the lemma states tettfimt and iwm aiwayt return aw
integer vahm With the afct of that tawi w ta, we "will d h saUfr eaaaStbh thai the spoclfteatson to
wen defined.

Lemma For amy $*M, backgtfifc) -» totegeri and frent$cf (X) '-* integer} and
back s * e> * f rotrtfr al i am dJde Mwr mm--n(R

This lemma can be estabftshed using the fttdueftre method outlined m Section 2.2.4;
The basis of the mdocttcer an i la a > fl d tow i st nw j»^ and mV» •rrnefmed to return -I and
0, respectively, jr» the mfthtf stote of the iwMthwtMl Tin* IWhMt i i i May t» also readily apparent.
For any state, Aiserf decrements ftoc* by I and leaves /hwtf unchang e d ; F uithermore, defefV
leaves b*ck unchanged amt only liun a wfaa l i ^enf By y ft m applicability condition it
satisfied.

We can now prove that the machine a a v JP a lfmitf uwng W * above temma. Thai
lemma is helpf nfr because both yhasf* and hw* most* be evameted in insrfs and definV*
applicability condition and effects section. The famma g u arante es that thst evaluation can be
done.

To prove that the machine Is welMef hied, three properties must be established i)
the applicability conditions of the O-f unctions insert and dafafe are defined; M> tbo next stato>
function is defined for both Instrt and deleft; and; ftnefly t lii) the ordering of the equation*
in both insert's and delete' s effects sections is immaterial. Note that iti) is trivially
established since <feta< has only one equation in It* effects section and tho two equations in

-55-

insert's effects section modify different V -functions. Thus, it is only necessary to deal with
i) and ii). We now complete the proof .

Since insert's applicability condition is a constant and delete* s applicability condition
only involves front and back, which were shown by the lemma always to return an integer
value, i) is established. The second part of the proof is ado established by appealing to the
lemma. Since insert's and delete' s effects sections only evaluate front and back, it is clear that
the next stpte function is defined for both these O-functions.

We will now show that the specification is consistent. This involves proving that
the four V-f unctions are total. First note that the lemma guarantees that front and back are
total. Storage and first .element, however, require more attention. Again, we must introduce a
lemma and then prove the desired results directly from the lemma. The lemma shows that
storage's applicability condition accurately describes its domain.

Lemma

For any $t$&, if frontg t k * backg, then storageg(k) is defined.

This lemma can also be established by the inductive approach outlined in Section
2.2.4. The basis is vacuously true since, in the initial state, back is greater than front. Now
assume the lemma is true for any state S. We must consider the effect of inserfrknd delete on
S. Since delete decreases front by 1, the result immediately follows from the inductive
hypothesis. Now let S* - NEXT(S,insert,x>. There are two cases. Either frontg. - backg.,
in which case storageg.(frontg.) evaluates to x, or frontg* * backg.. In the latter case,
frontg. > backg. and frontg. - frontg and backg. - backg -I. So for
frontg. ik& backg. 4 1, storageg.(k) ^is defined by the inductive hypothesis. Also,

storages>(ba€k$ J evaluates to x.

Thte lemma kmiM^ wttMlrtfct* tfrat V-Ev«l rf,« a ufrt te to** In any rtate S.
To see that V-EvaKS/ trst.ekmcwt) i* total in »ny tfate S, w*e that there at* two case*. First.
ftrst 0t*Mmt's *|ayhjMhWry conditi o * em «•!■» to triWf •» *hlifc fP» fc* qi#ei*l «P*Ni
error fa returned. Otherwise, to a|Mi»»M»f c o rrt l Ho a Wtf i rtW tt «W» <W* ^***IS * back ^
So, hy the mmm, siaeayeaftvoM^* ■ oa»aMO oas wo peow oj *^^^^^*

if^^gXr- fi&v&fr**-.:- '..^^^m^^-^V:^^

v^fs^^fts:?! ^t'K*'s.;«SsS'r' 1 '-

-57-
4. An Implementation Language for State Machines

Chapters 2 and S have focused on formataing the semantics of state machine
specifications. The work accomplished in these two chapter altows e?»e to write precise and
unambiguous specifications *f data abstractions using state machines. But these abstractions
are only mathematical objects. They can not toe wed directly as objects m any programming
language. They, must first be implemented. Thus, an important aspect in any formaliration
is to be able to describe formally whan a data ibrtraction, specified by a state Inlchine, is
properly implemented in some programming lang o ige. Developing this definition involves
the following. First, a programming language for implementing state machines must be
described. This topic is discussed in this chapter. Then, a method of proving the
correctness of an implementation must be fined. This topic isolated in the next chapter.

In thU chapter, the general properties of awf programming language fer
Implementing state machine specifications are described; in particular, the basic data
abstractions to represent the speetf Jed objects and the control constructs to implement the
V-f unctions and O-functiom. This approach of iHustrttmg program correctness is valid
since any programming language for imptementmg state machines must include these
features. The actual implementation of these data abstractions and control constructs is
unimportant here. Accordingly, this detail 4* tetatty suppressed in this chapter. Rather
control constructs to be used with state machine spedficartom are Introduced. So,
implementations of state machine specifications wtH be written in terms of other, simpler state
machine specifications. For instance, a speclfiatibh Of a stack could be implemented using
state machine specifications of variables and arrays to represent elements of the data

-58-

abstraction and the control constructs to realize the V-f unctions and O-f unctions.

To develop a definition of program correctness, it is only necessary to define the
relation between the objects of the specification and the objects of the Implementation.
Hence, since this chapter contains a general discussion of the objects of an implementation, it
is possible in Chapter 5 to give a general definition of program correctness. To prove that
this definition holds requires involvement with the semantics of the programming language
and identifying correspondences between objects of the language and terms used in the
definition. But these issues are not a major concern for only stating the definition of a
correct program that involves state machines.

4.1 An Example

An example state machine specification and its corresponding implementation are
given in Figures 13 and 14, respectively. The data abstraction specified in Figure 13 is a
finite integer set. Insert and remove are O-functions that insert and remove, respectively,
integers from the set. Cardinality is a V-f unction that returns the number of integers in the
set. Has is another V-f unction that determines whether or not a given integer is in the set.

Figure 14 contains an implementation of finitejntegerjet The set is stored as an
ordered sequence of integers in the array A. INSERT, REMOVE, CARDINALITY and
HAS are the corresponding implementations of insert, remove, cardinality and has} Each of
these operations uses SEARCH, which performs a binary search on the array A. SEARCH

1. Throughout this thesis, lower case letters will be used in the names of V -functions and
O-functions of a state machine specification. Capital letters will represent their
corresponding implementation.

-59-

Flgure 13. Specification of Finite Integer Set

finite_jnteger_set - state machine l« cardinality, has, remove, insert

cardinality - non-dertyed V-f *nct»eo( > returns integer
Appl. Cond.i tMM
Initial Value;
end cardinality

has - non-derived V-f unctton(i:integer> returns Boolean
Appl. Cond.: true
Initial Value: false
end has

insert - 0-functkm(i:integer)

Appl. Cond.: cardinaUty<100

Ef f ect«: 'has'(i) - true

If ~has<i) then 'cardinality' - cardinality ♦ 1

end insert

remove - O-f unctipnU;imef«r)
Appl. C ....

Effects: •h««(|j .false
if has(i> then •cardinaMty' - cardinality - 1
end remove

end f inite Jnteger jset

- 60 -

Figure 14. Implementation of finite integer set

FINITEJNTEGER.SET - Implementation is INSERT, REMOVE, HAS. CARDINALITY

A: array of integers initially undefined
COUNT: integer variable initially

SEARCH - procedure(a,f ,k:integer> return* integer
Wf-k

then return k

else If a£*.readU<f+k)/2J>

then return fE f 2J>

else return SEARCH W

end SEARCH

INSERT - procedure(i:integer)
If COUNT.read-0
then begin
Axhange(0,i);
COUNTxhangeU)
end

else If COUNT.read<100
the*

If COUNT.read - SEARCH«i0JCOtJHT.read)
then begin

Axhange<SEARCH(iACbl«srr.jf|adVj>;
COUNTxhangefe6UNT.rwd*l>
end

else if A.read(SE ARCr^,0^6UNT.read)>-l
then return
else begin
for j:«COUNT.read step -I y»#SEA!tCr«iJ^COUNT.read) do

if j>l then Axhange<JAread<J-l»;
Axhange<SEARCH<iACX)UNT.raadM>;
COUNTxhange<COUNT.r*ad+l>;
end
else signal error
end INSERT

"■'H •".

- Si-

ft EMOVE - procedure(i:integer)
If COUNT.read-0
then return
else

If A.read<SEARCH(i,0,COUNT.read»-I
then begin
for j :- SEARCH<i.0,COUNT.read> until COUNT.readr2 do

A.change(j,A.re*d<j+l»;
COUNT.change(COUNT.read-l>
e "d

else return
end REMOVE

CARDINALITY - procedure^ > returns Integer
return COUNT.read
end CARDINALITY

HAS - procedure(i:integer> returns Boolean
If COUNT.read-0

then return false

else if A.read<$EARCH<fACQUNTj>eaa>M
then return true
else return false
end HAS

end FINITEJNTEGER.SET

returns the index where the binary search stops.

An implementation consists of three parts: an Interface description, an object

■#■■■
description and operation definitions.

The interface description of an implementation provides a very brief description of
the interface that the implementation presents to the outside environment. It consists of the
name of the data abstraction being implemented and a list of the operations that users of the
implementation may employ.

-62-

FINITE JNTEGER JSET - Implementation Is INSERT, REMOVE, HAS, CARDINALITY
Operations such as SEARCH whose names do not appear In tfci*^& ttoktlpUon should
not be accessible by users of the t tw ptero e nt atlon.

The object description consists of the dedan^eTd«S| aha rr aoHon i that are need to
represent the object being tmpteme a ted . ■ Their datt abetract io m aw used as the concrete
representation of the specified abstraction. Here, each of Ifctoe da* abstractions w*H be
specified as a state machine and ALMS wHI be used for tiki oppose alheMfh any
specif kation language could be used.

In the example, the object description consists of . ,

A: array of integers mKia<y uodafln ad
COUNT: integer variable tnfthdly

tissfoon mtilt's'' ■■-':}^ t : ^ ■:■*''.*■.;.■ ---i

These phrases are syntactic sugar for the shite machine aumtf KMfoni of a variable and an

r s*«r> trmim r-»3t

array given in Figures l»'in* i*/r*p1&^ A are used to

represent the data abstraction. COUNT reflic^ the nim^ber k Inttgejs hi, the set Thee*
integers are stored as an ordered sequence m the art*? Wtmi^t&fa&^&^W^l.

The body of th^ Hnpbmmtatien cbiisiitt
provide implementations of the permissibte o o eratton i an the data abstraction; the
O-f unctions and the non-derived and derived V-f unctions. It is not necessary to Implement
the hidden V -functions since they are unknown to users. An o ae ral l on def i nition should be
given for every operation that appears in the interface description.

In our examples, operation definitions *rttt be written using V -functions and
O-f unctions grouped together by the usual control constructs that would be found In, say,
ALGOL 60 or PASCAL. These V -function and O-ftmcuon cats should be interpreted as

-65-
Figure 16. Variable

X: tjptj variable initially a is eottivatent to

X - etata machine t» X. read, X. change

X.r«d-non-<lw1V^V-fimctto«fVrat«Tnatyp«_t
Appff. @oajafrfraj#' : "
. Initial VaUiini
•nd X.read

X .change - 0-ftmfct*onC|*ype J)

Eftdotct *% ,Mfr* i
•nd Xxhange

andX

where typej it the natne of a defmmg abstraction of ALMS
and a is an element of typejt or uodefatrtd. f *

fellows. Assume that the implementation maintains a record of the current state of the
machines hi the object description; For wampte, rf no O-functtons have been catted, the
implementation wouk) view each state machine as being in Its Initial state. Now, each
V -function call v<a) should be interpreted as

V-EvaKS.vMa) .
where S, remembered by the implementation, is the current state of the V -function's
machine. An O-f unction call o(a) is interpreted as

0-EvaK5,oKa> - S*

-64-
Flgure 18. Array

X: type J array initially a is equivalent to

X - state machine 4s X.read, Xxhaajge

X.read - non-darfred V-f unctlotit fctatcger) return* tvpejt
ApnL Cond.: true
Initial Value: a
end X.read

X .change - 0-function( j^vteferMype-t)
Aoat. Cond,: tru*
Ef f eeta: Xreadt| « i
end X. change

endX

where typej is the name of a defining abstraction, of AUifS
and a is an element of type J or

where S is as before. Furthermore, the implementation now updates S to $* and maintains
S* as the current state of dV machine until another O-functten of «h« mac Wrie is cawed.

-65-

5. Proving an Implementation Correct

To formally establish the correctness of a program, one must prove that the program
Is equivalent to a specification of its intended behavior by formal, analytic means. This
chapter is concerned with this process, discussing how to prove the correctness of programs
that implement data abstractions specified by state machines.

Here, the homomorphism property win" be used In the proofs. In general, this
involves showing the following tHoare 72al Assume there is a class of abstract objects K
with abstract operations. Furthermore, suppose that x* is the concrete object representing an
abstract object belonging to ft Let Ct be the collection of aN such x*. Finally, suppose that
o» c is a concrete operation that purports to be an Implementation of an abstract operation e> a .
Then, the homomorphism property involves def filing an abstraction function. A. mapping
from C onto ft and showing for every operation that

• a (i4<x*» - >«« c <x*».

Before attempting such a proof, three steps must be performed. First, the concrete
objects used to represent the elements of a data abstraction must be characterized. This is
discussed in Section 5.1. Then the class of abstract objects R must be identified. This is
done in Section 5.1 Finally, the abstraction function must be described. Section 53 Is
concerned with this issue and the problem of adapting the homomorphism property to the
particular needs of state machine specif (cations.

86-

5.1 The Concrete Ropresontation

A concrete implementation of a data abstraction sp«^d by a state machine win"
usually consist of a collection of objects to represent the state set and ■ group of operations
that purport to implement the various functions of the machine. ^Some ,ef **«*• oj****** ***
will implement O-f unctions and others wM Implement derived and non-derived
V-f unctions. Note that it is unnecessary to implement Woden V -functions since they are
inaccessible and not an Intrinsic part of the data a*se«edein.

All of these operations wiH access or modify the concrete objects that are used to
represent the state set of the suite machine. We shall denote the m0J^ t tmfM : ^^Kl»
by C. If a concrete operation implements an O-functton », then we view the operation,
denoted « c , as a mapping from CxD f into C. ft* it Implements a V-f unction e», then It is
a mapping from C x D w Into R # . By adopting this view, we t «r*. making C att.expitctt
parameter of each operation. This may differ from the actual syntax of the implementation
language but clarifies the operation of procedures that operate through side effects or by
accessing global variables. For example, in the yt*«r ,..!■£!*& _«• ^fM^^^P
Chapter 5, INSERT would be viewed as mapping from C x integer Into C. Here, C
corresponds to the states of A and CX>UNT rem e mbe red be thf *^larfl|ijottion.

We shall now describe C in more detail. In general, C is « |n$f* «f ,» *»rge
collection of objects. For example, in tht finite inttgtr get example of , Chapter 4,.

C c » A x *cOUNT
A set such as IS A x * COUNT ,s t 00 br S e to »«* ** Ctie domatln of the abstraction function
since it usually contains elements that do not correspond to any element of the data

«!■ j.sfctiw* .

-67-

abstractton being Implemented. So, it is necessary to describe C explicitly.

The standard way to dd this is to use a concrete Invariant, I c . This is a predicate
defining some relationship between the concrete variables and thus placing a constraint on
the possible combination* of values that they may take. Then,

C-{xif c *x».
For the finite integer set implementation, I c is

sCOUNT.rewf $ WO a <¥i jK0^ij<COUNT.reid -♦ A.read<i><A.read<j>]
This predicate states that the implementation of flnUtJnttftr^it contains at most 100
integers and that the elements between and C00NT in the array A are all distinct and
ordered. This latter condition is necessary to insure the correctness of SEARCH. The
ordered pair

<*<(X.0>» « * A x *cOUNT
satisfies I c above. This ordered pair corresponds to both machines A and COUNT being in
their initial states.

5.2 The Abstract Objects

The elements of the concrete representation C should implement or represent the
entire state set of a state machine specification. However, a concrete object need not
represent a single state but rather a set of states. This occurs because certain states may have
no observable differences. When this happens, we say the states are equivalent. So, a
concrete object actually implements the equivalence class of a state and we identify the class
of abstract objects HwHh the set of equivalence dassef of the state set.

For example, consider the specification of bounded jtack In Chapter 1. Its state set is

-68

a subset of tD stack -♦ K sta &} x tD^ epth -♦ Kfagfal Now consider the Wo states

S t - <4,{<X,0H>
and

S 2 - <(<U>M<XJ*»

Here, d> is the null set. The first, stale S, cor re»|KWHU to <^, the in*tt«l s«ate of krtuwftrrf _jract,

so *fac* is totally undefined and de^f* returns 0. <Re*aH our previous convention that the

domain of nulla ry functions is (X).) The second «t*t< S^cpfieapands to »tatk(t> returning the

value 1 and for x*l, stack(x) is undefined. . AHf Mi %, ofr^riMjtnji tf*e vatot «. Thus 5 2 -

NEXT<NEXT<a.pusM>W.*> where Q, to the initial state o( htund M l attack. These two

states, S| and S 2 , are equivalent as far as a user of the machine Is conce r n e d since stntk is

hidden from a user and depth returns in either state. /

Equivalent states are defined below. Intuitively, two states are equivalent when tt is

impossible for a user of the specification to determine any d*ffereme between them.

Definition

Two states S] and S 2 of a state machine specification SM are eqitH/aUnt

if for any

Sj* - 0-EvaK...O-EvaKO-EvaKSj, o 1 )(a,))^ 2 )(i 2 »r.-,)o n (a n ))

S 2 * - O-EvaK...O-EvaKO-EvaKS2>^^^B^Ia^ P ^0 r| (a f| >)
where Oj is an O-f unction of SM, a 4 « D and ni0

either

Sj* - S 2 * - error
or i

both Sj* and Sjj* are undefined
of'

V-Eval<Sj*,v> - V-Evaf $%**)
for any non-derived or derived V-fuhction v of SM.

This definition guarantees that if a series of O-f unctions , ant applied ..to- two equivalent
states, then two new states are obtained wrtere the non-derived and derived V-f unctions

- S9 -

behave identically. Furthermore by applying a series of O-f unctions to the two states, we
make certain that all delayed effects become apparent We shall denote the equivalence class
of a states by CS1.

For example, for a state S of finite Integer _set in Chapter 4, (SI simply contains the

state S. For the initial state Q,of bounded stack,

t<y.{(F,{(x,o)}) t * boundedJtack }

where F is a mapping associated with the hidden V-f unction stack. In other word*. CQJ is
the set of all states where depth returns the value 0. Note that COjl ii Infinite. This occurs
since the data abstraction Integers used in bounded _st*ck contains infinitely many elements.
If bounded Mack used a data abstraction for the integers that had a bound on the number of
elements (such as the integers used in programming languages), then IQJI and all the other
equivalence classes of bounded ^stack would be finite. Furthermore, bounded ^stack's state set
would be finite.

The equivalence classes of the state set can be enumerated by using a normal form
generation of a state as the representative of each equivalence class. A normal form
generation or a state is either Q. , the initial state, or generated from Q, by only using
information adding O-functions. Recall that an information removing O-functton deletes
information that was previously added by an information adding O-functton. The same
effect can be achieved by initially not adding this information. Thus, this representation is
valid since every state either equals a normal form generation or Is equivalent to a normal
form generation. For example, in finite Jnteger^set,

NEXT(Q,,insert,l> - S
is a normal form generation but

70-

is not. However, it is equivalent to 5.

5.3 The Homomorphism Property

It is now possible to state what the correctness of an IroptetnentaUon means.
Informally, the implementation of a data abstraction Is correct when the operations of the
Implementation and of its corresponding specification behave identically and there is at least
one object of the implementation cor r e spo n di ng to every object, of the data .abatrai*ion. This
is the usual meaning of a homomorphtsm to rnathemetic* (Fnltefh 67).

Formally, to prove the correctness of an Impternentati on, one must first define an
abstraction function A from C onto the equivalence classes of M, the state set of the sute
machine being implemented. A simple and natural way to do this is to first define a
function f from C Into M (eg. into the normal forms m 0) and that define the abstraction
function as A(x) - Cf(x)l. A must map onto the abstract objects rt, the equivalertce classes of
SB. This property guarantees that every state is Impl e m e nt ed. pMoever, A need not be a
one-to-one mapping from C onto the equivalence classes of M. So, many concrete objects
can represent one abstract object.

Now, after defining A, one must show for every CcC and O-function •»,
IO-EvaKf<C>,w><x>J - CAw^C*))! 1
where x« D w and for every non-derived or derived V-f unction w
V-EvaKf<C),#)<x) - w c <C,x>

1. This is a slight abuse of notation. We assume t error! - error.

« ; 1^..;*<^.fsSJjf%...'

- 71 -

i " "

where x«D w .

The above definition assumes that an Implementation of a V-f unction does not
modify the concrete representation. If it does, we must add the condition

This could occur in an implementation of flidtijni<pr_s« where W/tf reorders the elements

of A. ■■" ■ --*■•'■"■ -■'' -■.■''-■'■ '

We shall illustrate these ideas using the example m Chapter 5. Again we assume

C c* A x* COUNT
and.

*integer_set c tD has "* "has 3 x [D cardinaHty "• "cardinality 1 -
First, let (C^cC. So C, is a state of the array A and C2 U a state of the variable
COUNT. It is helpful to define the predicate INKC,,^), which is true if the integer I is a
member of the concrete set, as follows:

IN(C 1( C 2 ,i) = (3j)(V-EvaKCi,A.readMJ) - i a Qsj<V-EvaKC2,COUNT.read>].
Informally, this predicate is true if there exists an integer J such that in the state Cj of A,
A.read(j) returns I and j is greater than or equal to zero and less than the value returned by
COUNT.read in state C 2 of COUNT. Then
f(<Cj,C 2 >) •

<{<i,truo> I IN(C ll C 2 ,i)> U {(i.falea) | ~IN<C| l C*0> , {(X,V-EvaKC 2 ,COUNT.read»)
Now to establish the correctness of the implementation it is necessary to show that A
is onto ft. This can be established by showing for every S« * that there exists a CeC such
that Cf(OJ - ESI. Then one must prove that

1. EO-EvaKf<C),insert)<x)l - E«INSERT<Qx)J

-72-

2. EO-Ev«Kf<C>.removeJl - CfdtEMOVEfO]
S. V-Eva¥f<Cr,hasXx> - rto&C,?)

4. V-Ev»Kf(a/af#»||jr)-Q^«»*^UPrV«*»
Consider proving S. Here, It is nececwj s to store**** *f an integ e r x tow is not In
the set, then HAS, respectively, returns true or foioo. Thli a^ano*^ iiwVibo shown by first
proving a lemma Hating that SEARCH<x,0,COUNTjead) afeays returns the mdex where x
should appear in the array A. This lemma wqwM aiifch^ li l rfa* In iWhbh i hw I g 1. and 2.
Furthermore, in proving 1. and 2., it would be neojssart to Jhow that both preserve the
concrete invariant since ^'s domain is :C.

-73-
6. An Extended Model for State Machines

The model of a state machine developed in Chapter 2 does not allow the
specification of V-f unctions or O-f unctions tha* operate on two or more elements of the data
abstraction defined by the machine. In this chapter, this restriction is lifted and the model is
extended to allow f the specification of these greater than unary operations.

To specify greater than unary operations, the definitions of the O-f unctions and
V-f unctions must first be extended. O-functions and derived V-functions wilt now be
allowed to have more than one argument of the data abstraction specified by the machine.
For example, this allows the definition of an O-f unction, union, which computes the union
of two sets, or the definition of a derived V-f unction, «mwwn_Wm#n/ J. whkh returns true
or f alas if two sets have or do not have, respective*?, any common elements.

O-functions will still retain their interpretation of changing the state of the machine
but now this state change can be dependent on more than one state. Derived V-f unctions
will also have their previous interpretation expanded. Now, instead of allowing the user
limited access to only one state, they will permit simultaneous access to more than one state.

Non-derived V-functions and hidden V-functions wM, however, stilt be restricted
to their previous interpretation. So, they can only specify unary operations on the data
abstraction specified by the machine. This conforms to their Interpretation as fully
characterizing a single state of the machine.

An example of a state machine specification with greater than unary operations Is
given in Figure 17. This is the specification of an integtr stt that can contain an arbitrary
number of integers. The specif icatton defines the usual operations tnstrt, rtmovt and kas as

-74-
Flgure 1 7. Specification of Integer Sot

integer jet - state machine Is hat, remove, Insert, union, aanmonyeiementj?

has - non-derived V-f unctforrfiatate.lrmteger) ntlmm Boolean

Initial Vahie: fetae
end has

amwriomjetement.? - derived V-furwttenCsj^sysM^ re«irwe Boolean
Appt. Cond.: hue
Pertva tk m; comnwn.rtemenrj - <3lKha*<*j,i> a harts^))

eno common_eiemem._r

insert • 0-functton(s:$tate,i:tnteger)
nppt, GnMt! IrVC
Effect*: fiasco - tree
end Insert

remove - 0-tunctkm<5:state,i:int*ger>
Appfc Cond.: tree
Effect* 'hMts.tf - fated
end remove

union - O-functtentsj^state)
Appl. Cohd.j.;tree

Effects: (VWChasis^) - hajfs^tH y h*sgi$t»)
end union

end integer _set

well, as the operations union and common jettmmt J described above. Union's effects section
defines the mapping of each non-derived V-f unction in the new state that it creates. Note
that a for all statement has been added for this purpose. Any greater than unary O-f unction
must define the mapping associated with every rwe-derlved or hidden V-f unction hi the
new state that it creates so that this new state is fotb; characterized.

-75-

We shall now formalize this type of specification by making a few extensions to the
model in Chapter 2. As hr that chapter, each machine is modelled by a set of states, where
each state is modelled by a set of functions correspomifng to the hidden and non-derived
V-f unctions; O-functions define transitions between states. t

6.1 Extensions to the Basio Components

6.1»1 V-ftmotions

6.1.1.1 Non-derived and Hidden V-f unctions

Non-derived and hidden V-functtons are specified as in Figure 18. Note that $ Is
now included in the mapping dejcription to tndfcaje that the V-function is a unary
operation on the data abitraclion d^iTMed ^ the definition

is defined in the same manner and retains the same interpretation a* in Section 2.L1A of
Chapter 2.

Figure 18. Non-derived or hidden V-f unction v

WfcpplnB Description: % TS y ; R y

AppMcaiMHty qan^lllpn, g yt t xD y -* Boolean
Initial Value: Jnjt^ttDy -♦ R y J

So, the sets D y and R y -«v the V-funetfcm's mapping description may hot contain
any element of the data abstraction defined by me marine. And as before, since the *»ate
of the machine is characterized by a set of mappings associated with each non-derived and

-76-
hidden V-f unction, we view the state set SB as a subs* of

where {vj,...,v n } is the set of non-derived and hidden V-f auction* of the machine.
6.1.1.2 Derived V-funotions

A derived V -function v also retains the three sections in its definition. However,
these sections' definitions and meanings are not the same as in Season U&A3 l»f tShaptir 2.

Figure 19. Derived V-f unction v

Mapping Description: $"; D y ; R v
Api>nc«Wttty CcmdKhm: tf v *« X O v -» Boolean
Derivation: der v such that (der v s »)t[D T -» R y ] for states S"

■ " »■■■■!■■. - . '1 ■■ I ■■ I ' ll l 11.11 1 t 1 11 II I II .. ..1.1,1,!,., IM I IIIMH— W^^^Mi— — ■— HiMI^— p W w'l M II I P — ^— — ■

, As before, the derivation section defines a function schema, denoted der v, expressed
as the composition Of the non-derived and hidden V -functions of the machine and other
functions associated with the elements of t> v . But, if v is a greater than unary operation,
der v also specifies the state in which each non-derived or hidden V-f unction should be
interpreted. For any states S", the mapping ass oci at e d with the schema is denoted by
(der Vgn).

As an example, consider the derivation section of common Jttewtnt J M Figure 17.
For any two states S t and S^ cmmim_st*mmJ returns the vshfe

<3i)[ba*(sj,i> A hasttgjtt.

:;.;■ . ^*S5f^^?v?K?E^

-77-

This vsrtue is, of course, dependent on the mappings associated with has in state Sj and has
in state So.

Now, for any states S", the mar^mg^ associated with Jejr ,jr is a rnembef of
[D v -» R v ] where D v and R v are specified by v's mapping description . These sets D v and
R v can not contain any elements of the data abstraction defined by the machine.

Finally, the applicability condition spectf iej a partial function % from^* 1 x D v into
the Booleans.

6.1.2 O -functions

O-f unctions too have the meaning and interpretation of the three sections in their
definition changed.

Figure 20. O-f unction o

Mapping Description: $ n ; D„

Applicability Condition: V Q : 8«xD -* Boolean

Effects Section: X^ t»xD -» %

As with derived V -functions, the mapping description now contains $" and D to
reflect the O-functions' extended capability. Furthermore, D is constrained so that it
contains no elements of the data abstraction defined by the machine. The applicability
condition and effects section are also extended to reflect the O-functions' new interpretation.
The applicability condition of an O-function how defines a partial function « from

- 78 -

D n x D Q into the Booteans. Similarly, $* tfftcts item <* #» O-funcMon now defines a
partial function £ Q from $" x D Q into %.

6.2 The Semantics of a State Machine

6.2.1 The State Sot of a State Mao

Our purpose in this section is to define SB. Here, we shall use the same approach
outlined in Section 2.2.1, taking the transitive closure of the initial state Q, under the state
transition function. The initial state Q,is the tuple (Init y -. Jn^ , ) containing the mappings
derived from the initial value section of each of the non-derived and hidden V -functions
( v 1 ,...,v n }. Furthermore, the next slate function has the following definition.

Definition

Let o be an O-f unction with mapping description $"; D^

mapping <f Q in its applicability condition and mapping E e it Its effects section.

Let acD and R<$".

Then,

* <R,a) if » (R^i)-tnie

NEXT<R,o,a> -

R if I (R^)-*«4«e

Thus, the state set is generated as follows.

-79

2) If © is an O-f unction with mapping description $* D Q and S"e *",

then if NEXT(S",o,a> p defj|nfd^ N^J(S^)c|| where aftD^. ls

3) These are the only elements of J8.

Note that in 2> above NEXT(S n ,oa) may be undefined. As was explained In Chapter 2, this
depends on the partial functions % and U Q . To guarantee that NEXT is always defined,
we introduce the notion of a Well-defined state machine.

Definition ,,. f *

A state machine is well-defined if for any O-f unction o with mapping description

3> n ; D and for any S\ SB", NtyJ$j^£M*plltol& a^^

This definition guarantees that in a well-defnied; state machine, for every
O-f unction o with mapping description $"; D^ W„ is a total function from ** X D into
the Booleans and % Q is a total function from {<&"**«*" X %[ ty$ m *M *«*> S.

6,8.2 The Semantics of V-funotions stnd O-funotlons

With this definition of the state set 55 of a state machine specification, it is possible
to formally define the meaning of the 0-fun<$0J*s and V-fuoeeotis, Jhi* wiH be done by
defining mappings V-Eval for V-f unctions and O-Eval for O-f unctions such that
V-Eval^B n xNV-»[A-»RJ
and

0-Eval:»" x NO -> CA -» £H
where NV is the set of V-function names, A is the set of argument*, R U the set of results
and NO is the set of O-f unction names. Note that the domains of V-Eval and O^Eval

-80-

have been changed to reflect the extensions made to the V-f unctfin* and O-f unctions.

O-Eval will be defined firrt. Now, given an Q*f unction o with mapping
description $*; t) Q arid applicability cbhdfftibn *^ for any «•«#*, O-Eval returns a
function from D Q into * U (enort/Sb, ui^lln^of notation,

O-Evaf&'Vb) - XaI* (S",a> -♦ NtkT^*Aa)«mi

O-EvaKS",0> js not necessarily total since either * <S*\a> or J4EXT<$"*,*> can be
undefined. However, 0-EvaKS",o) is always a total function in a weft-defined state
machine.

For any non-derived or hidden :V-^func#i»rt yibirf ' iOtik'ty ^-EviA will return a
function from D y into R v U ( error) . So for any non-derived or hidden V-functton v with
applicability condition V v ,

V-Eva*S.v) » Xaliy(sta>-» v|t ilM;

Finally, for a derived V -function v wfth rrappmg dekrtfftioh iK'W^i applicability
condition tf v and derivation der v.

v-EvaKs*.v> - xM r tg?jd -» cdtt ^wipjiNiai

where S n «S5 n .

Note that the function that V-Eval evaluates to is not necessarily defined over the
entire set D v since the applicability condition can be undefined or, depending on the type of
V -function, v s <a) or (der v s «Ma> can be undefined When the applicability condition
evaluates to true. When this i% not the case, we say the state machine is consistent.

81-

Definitton

A state machine is consistent if,

for every state Si SB and non-derived or hidden V -function v,

V-Ev»KS,v) is : rtipri function from D y Into R y U (error)
and if,

for every derived V-f unction v with mapping description $"; D y and S"c$B"

V-EvaKS» 4s a total function f rom D T into R v U t error) .

In a consistent state machine, for non-derived and hidden V-functtons, v§ is always
a total function from UcD v I * y <S,x» into R v and, for derived V-f unctions, (jjer v s *) to
always a total function from (x«D y m v (S"^» into R y .

-82-
7. Conclusions

The aim of this thesis has been the development of a f ormai specification technique
for data abstractions based on Parnas' ideas. First, a f^^lftsgMX%^,^^nmt^ics of a
state machine specif ication wai developed. Thfc model gave an effective construction for the
state set of a state machine and then used the suite set to formaMie the semantics of the
V -functions and the O-f unctions. Also, the notions of a well-defined and of a consistent
state machine were introduced. Next this abstract model was used to formalise the semantics
of a concrete specification language for state machines. This language was used to specify a
number or data abstractions and also to illustrate how to prove a particular state machine is
well-defined and consistent. Then a proof met hodol o g y to use with state machine
specifications was discussed and illustrated. . This methodology e mpl oye d the homomorphism
property to establish the correctness of an Implementation of a state machine specification.
Finally the model for the semantics of a state machine specf teation was extended. This new
model allowed the specification of a greater class of date abstractions than the previous one.

In this final chapter, the usefulness of the state machine specification technique is
evaluated and reviewed. This evaluation Is then followed by some suggestions for further
research on state machine specifications.

7.1 Evaluation

The state machine specification technique is best suited for the specification of data
abstractions. Its conceptual basis of a group of functions operating on a state set matches
quite well the notion of a data abstraction where a group of functions operate on a collection

■.fs^mn'if^PS

■ -8S- .'■■■•

of objects. To construct a state machine specification of a data abstraction, one must model
the objects of the data abstraction using the V-f unctions of the machine. In a sense, this
corresponds to modelling" the objects of the data abstraction by using infinite arrays. So the
state machine technique is a variant of the abstract model approach [Berlins 78 J, CYonezawa
771 where one is restricted to modelling objects of the data abstraction by using infinite
arrays.

In the abstract model approach, the objects of a data abstraction are represented in
terms of other data abstractions with known properties established by formal specifications
given in advance. Then the operations of the data abstraction being defined can be
specified in terms of the operations of the known abstractions selected as the representation.
So, a model for the data abstraction is developed. This differs from axiomatic specifications
CZittes 74), [Goguen 753, CGuttag 751 where the behavior of a data abstraction is given by
axioms relating its operations. Currently research is being done on both these techniques.
Since any comparison made between abstract model and axiomatic specifications will apply to
state machine specifications, we shall limit the following discussion to a comparison of the
abstract model and state machine techniques.

In using the abstract model approach one is free to choose the data abstractions used
to represent the specified objects. Thus it appears that abstract model specifications would
be easier to construct than state machine specifications. In fact, one can encounter difficulty
in using the state machine technique to specify an abstraction whose objects can not be
modelled well by arrays such as lists or trets.

Another issue in constructing state machine specifications is that one usually wishes
to write a specification that is well-defined and consistent So it will be necessary to prove

- 84 -

that these two properties hold. Studying the proofs in Appendix 2. It appears, at first glance,
that the proofs of these two properties are rather complex. Hoffev^whjif the proofs in
Appendix 2 may indeed be somewhat cumbersome, they are basfcally quit? simple and
straight forward. They primarily rely on the definitions In Chapter ,8, The rnjBft "creative"
step in the proofs was the introduction of the lemmas. Even hep, hcnvever, the creativity
involved was minimal. For example, when I started work on showing that the specif kation
of queue was well-defined, I did not begin with the first lemma. It was only wheji I was
forced to show that both front and tec* could be evaluated in my state that I realized that I
had to prove this lemma. So, in carrying out the method outHned in Section 2,24, Itopid
the extra condition I needed to simplify the proof. This experjeoce was repeated when I
attempted to show that V-EvaKS,first_etement) was total.

I feel that in most cases it will be necessary to prove simple lemmas to help in
carrying out proofs of properties of state machine specif katioiu. $ JJa*aejir, it appears «4iat
these lemmas are usually quite easy to discover and that the actual fteps in. the proof wiM
involve one in time consuming, but not difficult, work. ,

However, it appears that proving the eprrefBa^e^a* Jnjj^^
difficult. Here not only is it necessary to show that the hompmpTphUm property holds but
one must also show that the abstraction function is an or^o rna^pjng. ThJ*,)atter task is not
simple. One must first characterize every equivalence c»a»s of the state set ami theji show
that there exists an element of the concrete objects that maps into ||ij^ element.

To prove that some property hold? for an ab^tra|t model specification of a data
abstraction, one must show that the property holds in the dapa abstraction V model. The
difficulty of this proof depends on how well chosen the model is. ThtJ! proving that a

-85-

property holds In a state machine specification can be easier or harder than proving that the
same property holds in an abstract model specification according to the aptness of the latter
specif fciation's model. However proving the correctness of a data abstraction specified by
either technique appears to involve equal difficulty.

7.2 Topics for Further Research

One area for further research is to determine the usefulness of the state machine
specification technique. Specifically, can state machine specifications be used successfully in
the design and development Of large scale software systems? Research that should help
answer this question is currently being done at SRI. They have used state machine type
specifications in the design of a provably secure operating system [Neumann 773 and are
developing a methodology for the development of software that uses state machine type
specif ications. Their preliminary results Ifl this area have been encouraging.

Another research area is the extension of the state machine specification technique's
error handling capabilities. At present, when the applicability condition of an O-functton or
V-f unction evaluates to false, the function returns the special symbol error. Clearly, this
does not give the user any clue as to what has caused the error. More information should be
given. Furthermore, the meaning of returning an error message has not been discussed.

The specifications could be extended to allow one to define more descriptive error
messages. For example, cardinality in the finite set specification of Chapter 5 could return
an error message such as "too many elements" when one attempts to add more than 100
integers to the set. Parnas has noted that more information Is needed to describe how his
specifications handle errors [Parnas 72, 75).

Another e*ten*ion to state machine i|>eettl^t|iil^i^.J^|ll|iii Mi J^^^kMihiir ^^iti
fcbttrictkfffe irjeciffcld. f hroughout this thesis, #e h*ve assOwM mit> tftt am abslt t aUotn
specified by a state machine are ImmutcHt. In ail IrmmnatHe abatracttoo, the ebjeati of the
abstraction ire constants; i:e.; thWr property So not »arj fr»ir qgft, im tWI elpi fcds HHhe
behavior of the states ih a state machine specification. Ah O-fiHittOh 6, *heh gffen a state
S and xcD» ; does hot rtf&tftfy S, but instead* returns ilef state I*. Furthermore, if the
O-f unction o is again |M S t«#,* later in, a coj^p|lii%Ji|^,|^ 4 -B||tt^'#*. Simitar
behavior is aho exhibited % i V-fwiction. Hdwevar in a awtfalto data aliaUoiiHun the
behavior of the objects may change. Ah operathjh of a ra«f»blt data «b«r*ctton when
passed a mutable object may return a dtfferem resuk at ditferent htttanoe* in the
cornputatioh history; Thus, an obvious topic fa farther 1 > HWuHh %Mhilf^^^<4ifml
machine techhKjue to aHow the spetfficit*i»lof^ ibstiaiili** tAtfiHa« -lH- IS

studying how abstract modei specif fcations can be used to aB+clfo oiewbta etati^ i

-87-
Appendix I - Undecidable Properties of State Machines

In this appendix, we shall show that it is impossible to decide algorithmically
whether or not a state machine, specif ed 4n ALMS, is well-defined or consistent. This Is
established by reducing both problems to the Wan* tap* halting problem for Turing
machines. The blank tape halting problem is the problem of determining, given a particular
Turing machine T, whether or not T hates when started on blank tape. This problem Is
undecidable CHennie 771

The definition of a Turing machine used here is given by ((Jennie 77J. A Turing
machine consists of an infinitely long tape coupled to a finite control unit. The tape, which
acts as the machine's memory unit, is ruled off into squares. Each square may be inscribed
with a single symbol from a finite alphabet I, or ft may be blank. The special symbol ii Is
used to represent a blank. The control unit can shift the tape back and forth and is able to
examine one square at any time.

The control unit is capable of assuming any one of a fixed, finite number of states.
We shall only consider deterministic Turing machines. So, at any given time, the state of the
control unit, together with the currently scanned tape symbol, uniquely determines the
behavior of the Turing machine. The Turing machine has two actions: it may either halt
or carry out a move. Each move consists of writing a symbol on the currently scanned tape
square, shifting the tape one square to the left or right, and causing the control unit to enter
a new state. 1 The action of the Turing machine U characterized by the successive moves that

1. The symbol that the Turing machine writes need not differ form the symbol that is
already there and the new state need not differ from the current state.

-88-

occur when, initiatty, the control unit assumes some pndnipmei starting state »nd some
finite number of the tape squares ate Inscribed with symbols and the remainder are left
blank.

A Turing machine It represented by a group of qotnt*ph*oT •0t-f&iimtyfmm

where q. is the current state

Sj is the symbol under the tape head

s^ is the symbol to be primed on the tape

d(< ( right , Mt) tt the direction of the head's nwTemciil

q h is the next state
Each quintuple must have a distinct prefix q,Sj. The Turing machine baits when the control
unit is in a state q and is scanning; a symbol s such that q s is not ; th$ prefix of any
quintuple.

So, assume we are given a Turing machine W with <

and initial state q, .

Now, consider the state machine given in Figure 2t
For the notation &d),

1 if d - rjgM

*d> -

-1 Ifd-jiff

-89-

Ffgure 21. Turlng_machlneJW_1

Turing_machineJWj - stats machine Is tape, state, head_pos, move

state - non-derived V-f unction* > return* character string
Appl. Cond.: true
Initial Value: q.

end state

head_pos - non-derived V-f unction* > return* Integer
Appl. Cond.: true
Initial Value:
end head_pos

tape - non-derived V-f unctlond-.integer) return* character string
Appl. Cond.: true
Initial Value: *
end tape

welljiefinedJV- hidden i V-# unctk*i< ) returns integer
Appl. Cond.: true
Initial Value: undefined
end well_defined_?

move - O-f unction( )

Appl. Cond.: true

Effects:

If state -q, a tape<head_pos> - s, then 'state' - q,,

if state - q. a tape(head_pos) - s, then *head_po$' - head_pos + l<d, )

if state - q, a tape<nead_pos> - s, then *tape'(head_pos) * s,,

if state - q. a tape(head_pos) - Sj then 'state' - q,,

if state - q, A tapetftead_pos> * s. then "head Jpos* - head_pos ♦ Kd, >

if state - q. A tape<head_poj) - s, then .^e^j^feVpojs) - *„

if ~((state - q. a tape(head_pos> - s ( ) v...v (state - q, a tapediead^pos) - s, )>

thentape^headjK^-welLdefined?
end move

end TuringjmachineJWj

-9©-

Turing_machine_»t_l slmufates « by hating a tim t *^ f ^j£^ l £&n.t*!*Q^&*'
computation. ..... . .. ... _. ,..._ ^ .,„,,.... . -, ^

Now, Turlrigjnacfciiie^^ ***«»

on blank tape. Assume %¥ hates when ' started ^ on M»nV{ape. f^
Turing .machine _W J corresponding to the final 4*% te ••% ea«a|liiMlil: InS,

Estate -«», a inj mmrjM '* t) t*\.:W^*'** V m )m * M *o*'~ s, n »
evaluates to tnra. Buti the equation -*^ ^ »

'tapeXbeadoo*) - weH_defi»ed_?
is undefined since the V-functtan wttJUfhudJ tit tJ mUm > '- MtilaM a value. Hance,
Turing_machtne_il J is not we»-def ined. : ^

Going the other ^t/ifopW* Tfr ing ^c l ^ This can

only be caused by ti!l -

'tape'thead_pos> « wetLdef inedj
since the other equations only use total V -functions, T1HW ;

Estate - q, /v taptflfcedipoi) - «, ) Vw**Mf k%i A 1epe*»ead.jw*> . s, »
is satisfied so m must halt. ■„..-*.-.

Now, consider the state machine specification m Figure 38. This ftate machine is
not consistent if and only if W halts when started on blank tape.

■ -i ri-rx'i-' >• ■.«■ v-fw--' Kfc-«t"4;5>*.^ jir? /", t - '■> ■■■■■' ■ ' ■' ?

- FJr«. assume ft ha to oa blank tape. Then^M*?* a *W» $ for which
-((state - a, a tabe(h«d_p«) - $, ) v ... v>stat» - a A tap^l^ead^ws) - s. »
Evaluates to trua. Consider 0-£*aK6jwwv«)(X) - S*. In Sf", sautf* evaluates to trno so the
V -function consistent J is not total. By reversing this ar gum e nt , it is apparent that if
Turing _machineJW_J2 is not consistent, VI hafts on Wank tape.

-91-

Figure 22. Turlng_machlneJW_2

Turing_machineJW_2 - state machine Is tape, state, consistent.?. head_po», move

state - non-derived V-ftmctlon< ) returns character string
Appl, Cond.: true
InHlal Vehie: q {

end state

head_pos - non-derived V-f unctionf ) returns Integer
Appl. Cond.: true
Initial Value:
end head_pos

tape - non-derived V-f uncttontkinteger) returns character string
Appl. Cond.: true
Initial Value: 1i
end tape

consistent.? - non-derived V-f unction* ) returns integer
Appl. Cond.: switch
Initial Value: undefined
end consistent.?

switch - hidden V-function( ) returns Boolean
Appl. Cond.: true
Initial Value: false
end switch

-92-

move - O-f unctkm( )

Appl. Cond.3 trtra

lift***:

If »t«te - ^ a tape<head_p<»> - 1, «*•« 'tfitf - % .

if state - ^ a ttp*<h«d_p«) * ^ «»»«* IwwLpw' * h«d_|K» ♦ *d, )

if state - 4, a i*pe<h«ad_jK») - 1» tlMft 'tap«1lnfed_|*i} - ^

if state ■ ^ a Mipath—d^w^ ^ fc Ml —Slim**/ * WawLj** ♦ Kd, )

If ~Mstate«$ At«p«(h«»d_po^-» j )vj.^(|i «d_poi)-s,))

end nwve >; 5 ...

end Turi«gjm«c#«ifwjij2

"TflP

h i ' |h i i i^ i r u 1 . 1 . i

-93-
Appendix II - Proofs

This appendix contains the proofs of the lemmas litd the theorems in Section 3.3 of
Chapter 3. We shall first show that the specification is well-defined. This wilt be done by
initially proving a lemma that captures the key properties necessary to insure that the
machine is well-defined. Then, with the aid of this lemma, we will directly establish that the
specif ication is well-defined.

First, some notational detaUs must be handled. We shall denote the initial state of
queue by Q,, its state set :bflsl and assume

* c [D storage - Rstarage 1 x < D back * R bac* J x lD f*opt ■* "front 1 -

Lemma For any St SB, back s «UM « integer] and frontgtUX) -» integer] and
back s * d> * front s where d> is the nuH set

Proof by induction:

Basis: By definition,

baekQ^- U*m and front^- {<X,-1>}.

Inductive step: Awume for all

S - NEXT(...NEXT(NI^T<Q r ^ i )^ 4 )^» n , lf a n „ | )caf
where a,€ D^. n*2 and o i dinsert.dilet«} that back s ««X) -<t integer! and
front s «[{*> -» integer] and back s #a> ^ f ront^. We m*»t show for all

S« - NEXT<S,«,x>€*
where x«D w and »< Unsert,detete> that back s .«[U) -» integer] and front^nx) -» integer]
and backg. * 4> * frontg.

-94-

Case 1: backg.

Case la: w « insert

Then S* - NEXT(S , insert , x>.

Since |»(S , true . insert ,x) - true,

S' - TE(S , insert , x , 'storage'(back - » - I , ^back' - back - 1)

- E(E(S , insert , x , 'storage'(back - 1> - i) , Insert , x , "back* - back -. I)

-S,
Since S*( j$, S] is defined and bence
S 2 - E(S , insert , x , 'storage'(back - 1) - i) is defined.
Then S' - E(S 2 , insert , x , "back* - back - 1)

• {storage*; ffX; s»<S 2 , back - 1 , insert , x») , fronts >

- (storage s , {<> , S 2 K back. - l» , fTQ«t s )

- (storage s • {< * • back S, " I)} ■ fro ^S- >
Now back s " ba **S and ■** &7 tne Indlttetrve hypothesis,

it

it is a member of Kx) -» integer] - if).

Thus* baek s *«t(xr -» integer] - 10.

Case lb: w - delete

Since S* - NEXT(S , delete , X) is by assumption defined, there are two

cases relating to i»(S , ~<front« back - 1) , delete , X)

Case lbl: stfS, Mfront - back - 1) , delete . X) - f*lao.

Then S* - $ and by the inductive hypothesis,

back S €t{^} -♦ Integer] - {$}.

Case lb2: i»(S , *Af ront - back - D , delete , X) - frvm.

Then S* - TE(S .delete , X , Yronf • from - 1).

So back s " '*•**$• " hkn ' *J *** *«*»***■** hypothesis,
Is a member of {{*} -♦ integer] - {•>).

Case 2: f ront s »

Case 2a: w - insert

Here, S* - TE(S , insert , x , 'storage^back - 1) - i , 'back' - back - 1).

So, front s * " front s € **** ~* mt *f erJ - W by the inductive hypothesis.

-95-

Case2b: «o -delete

Case 2bl: |t(S , Mf root - back - I) , delete , X) - f •!»•.
Then S* - S and by the Inductive hypothesis,
front s et{X) -» integer] - (♦>.
Case 2b2: it(S , ~(front - back - 1) , delete , X) - truo.
Then S* - TE(S , delete , X , 'f ront' - front - 1)

- E(S .delete , X , 'front'? front - 1)

- (storageg , back s , {(X , »t<S , front - 1 , delete , X»)>

- (storage s , back s , ((X ,S r 3 front - 1»)

- (storage s , back s , {(X , frontg - 1)»

By the inductive hypothesis, fron^cCfX) -♦ integer) - {«» so
froot s .<[(X) -♦ Integer! - (d>). I

We can now prove that the machine is well-defined using the above lemma. Throe
properties must be established: i) the applicability conditions of the O-f unctions Insert and
delete are defined; il) the next state function is defined Tor both insert and delete; and,
finally, Hi) the ordering of the equations hi both Insert's and delete' s effects secttions to
immaterial. Note that iii) is trivially established since dWrtr has only one equation in its
effects section and the two equations in insert's effects section modify different V-f unctions.
Thus, It is only necessary to deal with i) and ii). We now complete the proof.

Case 1: The Applicability Condition

Case la: Insert's Applicability Condition
l»(S , true , insert , x) - S ► true

- truo
Case lb: Delete's Applicability Condition
|t(S , ~(front - back - 1) , delete , PO - S r 5 "(front - back - 1)

. - ^fronts - backs - 1)

-96

By the lemma, both frontg and backg are members of C(X) -- ♦ integer] - (+>
so ~(f rontg - backg - 1) is defined.

Case 2: The Next State Function
Case 2a: NEXT(S , insert , x)
By Case la, it(S , true , insert , x) - true
So,
NEXT(S , insert , x) - TE(S , insert , x , *storage'<back - 1) - i , tack/ - back - 1)

- E(E(S , insert , x , 'storage'(back - 1) - i) , insert , x , tack' - back - 1)
Nbw,
E(S , insert , x , 'storage'(back - 1) - i)

- (Xx.t(x - tt(S,back-l,insert,x» -» t»<S,Unsert,x),storageg<x)],backg,frontg>

- (Xx.[(x - backg - 1) -» x , storagcgfc)) , back s , frontg)
-S*

Note that backg is defined by the lemma so S* is defined.

Now,

E(S* , insert , x , 'back' - back - 1)

- (storageg. , {(X , ta<S" , back - 1 , insert , x)» , frontg)

- (storageg. , {(X , backg. - 1» , frontg)

- (storageg* , U\ , backg - m , frontg)

By the lemma, backg is defined and hence NEXT(S , insert , x) is defined.
Case 2b: N EX T(S , delete , X)

Case 2bl: ii(S , Mfront - back - 1) , delete , X) - fate*

Then NEXT(S , delete , X) - S.

Case2b2: i»(S , ~<front - back - 1) , delete , X) « tr«wi

Then NEXT(S , delete , X) - TE(S , delete , X , 'front* - front - 1)

- E(S , delete , X , 'front' - front - 1)

- (storageg , backg . <"<X . l*<S .front - 1 , delete , X))M

- (storageg , backg , {(X , S f front - 1)1)

- (storageg , backg , ((X , frontg - t)J)

So by the lemma, NEXT(S , delete , X) Is defined. §

-97

We wtH now show that the specification is consistent This involves proving that
the four V-fuhctions are total. For front and back note that

I), back

V-EvaKS , back) - XaI§»<S , true , back , X> -+ back s , error]

- Xaltrtra -♦ back§ , error)

- Xa.back§

2> front

V-EvaKS , front) - XaIn<S . true , front , X) -». front s , error]

- Xaltruo -♦ front s , error]

- Xa.f rontg

By the lemma, both back s and front s are defined.

To see that both V-EvaKS , storage) and V-EvaKS , fimjettmetiO are total, we
must again introduce a lemma and then prove the desired results directly from the lemma.
The lemma describes the domain of storagt.

Lemma

For any Sc», if front s * k * back s , then «orage s <k> is defined.

Basis: Since f ront^ m <{x,-*» and back^ * <{x#», the lemma^lviaHv follows.

Inductive step: Assume for all

S - NEXT(...NEXT(NEXT(Q,, Oj^^ajj)..^.,^.,^*
where a^D^, n*2 and o,c{insert.delete} that if fronts * k * "^^S then storage^*) M
defined. We must show for all

S' - NEXT<S,«,x>cJS

where xeD^and »< {Ju*ert,dflete> that tf fron%. -*fc t »fkg>, «»ft ne wgtft C hUs defined.

Case 1: w ■ Insert ,

Note x«D, nserl .
Case la: frontg* - backg.
Then storage s .(f rontg.) evaluates to x
due to the equations 'stwage'tbeck - » > 4 and Wfc- * btMfe - L
Case lb: frontg. * backg.
Then frontg* > backg.
and front§. - frontg and backg. - backg - 1.
So for frontg. 2 k * backg. ♦ h storageg*(k)
is defined by the inductive hypothesis.
Also, storageg. (backg.) evaluates to x
due to the equations 'storage'fback - 1) - I and ititt* * JMfc - 1.

Case 2: » - delete

Since f rontg. - frontg - 1 and backg. - backg,

for fronts* «Jt z back s . t storage^)

is defined by the inductive hypothesis. J|

To see that V-EvaKS .storage) i$ total, note that

V-EvaKS , storage) - XaifrfS , frartzfeback , storage , aft •♦ storafe s (a) . error]
- Xa.[front s >a>back s -» Moraft^a) . e r ro ri

The : desired ,. result • iromtdtatetr - feHiww f *■* ■ afcr tenwn*, - ; : Y* 1 <-»■■- ' *Ha*
V-EvaKS , first_element) is total, note that for any Sc £

V-EvaKS , f implement)

- Xa.(|t<S,~<f rorit - back - l),f irst.etemenUO -* w(Sjtota^front)Jirst e» l » >t ; ii l A)jr roT3

- Xa.t~< frontg « backg - 1) -» storagegtfrontg) , fp$g|

99-

If ~(front s = back s - 1) is false, then

V-EvaKS , first_e1ement) - Pu. error .
Otherwise,

V-Eval(S , first_element) = *a.storage s (frontg)
Now front s * back S so - b y tne lemma > storage s (front s ) is
defined. Thus, we conclude V-Eval(S , first_element) is total.

100-

Referenees

[Berlins 78] V. Berzins

Abstract Model Specification Jor Data Abstractions

forthcoming Ph. D. Thesis M.I.T. (1978)

IBurstall 69] R. M. Bu«taJJ

"Proving Properties of Programs by Structural Induction"

Computer Journal Vol.12 (1969) pp.41-48

[Curry 50] H. B. Curry

"The Logic of Program Composition"

Applications Scientifique de la Logique Matkematique

Actes du 2 e Colloque International de Logique Matkematique 1992

Paris: Gauthier-Villars (1954) pp.97-102 [Paper written in March, 1950]

IKnuth 76] D. E. Knuth, L. T. Pardo

The Early Development of Programming Languages

Stanford University, STAN-CS-76-562 (August 1978)

tFraleigh 67] J. Fraleigh

A First Course in Abstract Algebra

Addison- Wesley Reading Mass. (1967)

CGoguen 75] J. A. Goguen, J. W. Thatcher, 1. G. Wagnfr, J. *. Wright

"Abstract Data Types as Initial Algebras and the Correctness of Data Representations"

Proc of the Conference on Computer GraphUs, Pattern Recognition and baia Structures

(May 1975) pp.89-93

[Guttag 75] J. V. Guttag

The Specification and Application to Programming of Abstract Date Types

Ph. D. Thesis, University of Toronto CSRG-59 (Wm

CHennie 77] F. Hennie
Introduction to Computability
Addison-Wesley Reading Mass (1977)

[Hoare 72a] C. A. R. Hoare

"Proofs of Correctness of Data Representations"

Acta Informatica Vol.1 No.4 (1972) pp.27l-281

-101-

[Hoare 72b] C. A. R. Hoare
"Notes on Data Structuring"
Structured Programming pp.83-174
A.P.1.C Studies in Data Processing No.8
Academic Press London-New York (1972)

[Kapur 78] D. Kapur

Towards a Theory of Data Abstractions
forthcoming Ph. D. Thesis MIT. (1978)

[Liskov and Zilles 741 B H. Uskojf, 5. Zilles
Programming with Abstract Data types'
Proc, ACM SIGPLAN Conference on Very High Utri Languages
SIGPLAN Notices Vol.9 No.4 (Apr. 1974) PpJmI .TT/T;

t Liskov and Zilles 751 B. H. Liskov, S. Zilles

"Specification Techniques for Data Abstractions"

IEEE Transcations on Software Engineering SE-I VoliiWm pp.7-W

[Liskov and Berzins 771 B. H. Liskov, V. Berlins

"An Apppraisal of Program Specifications"

Computation Structures Group Memo 141-1, M.J.T, (Aprtll977)

[Mime and Strachey 76]

A Theory of Programming Language Semantics

Halsted Press New Yofk (1976)

[Neumann 74J P. G. Neumann

Towards a hi etkodofogyfor Designing Large System and Verifying their Properties

Gesellschaft fur Informatif, Berlin (1974) v^-» *-

L/T^?* * °P ermnt 5 *""»- r ** *!***, Its Afpttcmtims, and Proofs
SRI Fianl Report, Project 4332 (February 1977)

[Parnas 72] D. L. Parnas

"A Technique for the Speculation of Software Modules, w*h Examples"

Comm. ACM Vol.15 No.5 (May 1972) pp.S30-336 ^^

[Parnas 75) D. L. Parnas

"More on Specfkation Techniques for Software Modules"

Research Group on Operating Systems I, T. H. Darmstadt, Fed. Rep. of Germany

-102-

[Pratt 763 V. R. Pratt

"Semantical Considerations on Floyd-Hoare Logic"

17th IEEE Symposium on the Foundations of Computer Jctfitc* (Oct tfft$> pp 4GM21

[Price 73] W. L. Price

Implications of a Virtual Memory Mechanism for Implementing Protection in a Family of

Operating Systems

Ph. D. Thesis, Carnegie-MeMon University (June If7»

[Robinson 75] L. Robinson, K. Levitt, P. Neumann, A. Saxena

"On Attaining Reliable Software for a Secure Opett$i^VJ{em" ■.. .

Proc. International Conf. on Reliable Software WftSi ^^P^H

t Robinson 773 L. Robinson, K. Levitt

"Proofs Techniques for Hierarchically Structured h'dffiijtt"

Comm. ACM Vol.20 No.4 (April W77) pp.271-285

[Roubine 76] O. Roubine, L. Robinson

SPECIAL Reference Manual

Stanford Research Institute, Technical Report CSG-45 (August VeW

[Spitzen 76] J. Spitzen, K. Levitt, L. Robinson
An Example of Hierarchical Design ana* Proof
Stanford Research Institute (January 1976)

[Yonezawa 77] A. Yonezawa

Specification and Verification Techniques for Parallel Programs Jlased on

Message Passing Semantics

Ph. D. Thesis, M.I.T. Laboratory for Computer Science Ts%4 tr 1977)

[Zilles74] S. Zitles

"Algebraic Specfication of Data Types"

Project MAC Progress Report, {\«^t) ppA2-b6M.IT.