# Full text of "mit :: lcs :: tr :: MIT-LCS-TR-202"

## See other formats

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.