FormalAspectsofComputing(1998)3:1{36 (cid:13)c 1998BCS Specifying and Re(cid:12)ning internal operations in Z (cid:3) John Derrick, Eerke Boiten, Howard Bowman and Maarten Steen ComputingLaboratory,UniversityofKent,Canterbury,CT27NF,UK. (Phone:+441227764000,Email:[email protected].) Keywords: Z; Re(cid:12)nement; Distributed Systems; Internal Operations; Process Algebras; Concurrency. Abstract. An important aspect in the speci(cid:12)cation of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the interface to the environment (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. In this paper we are interested in the use of the formal speci(cid:12)cation notation Z for the description of distributed systems. Various conventions have been employed to model internal operations when specifying such systems in Z. If internal operations are distinguished in the speci(cid:12)cation notation, then re(cid:12)nement needs to deal with internal operations in appropriate ways. Using an example of a telecommunications protocol we show that standard Z re(cid:12)nement is inappropriate for re(cid:12)ning a system when internal operations are speci(cid:12)ed explicitly. We present a generalization of Z re(cid:12)nement, called weak re- (cid:12)nement,whichtreatsinternaloperationsdi(cid:11)erentlyfromobservableoperations when re(cid:12)ning a system. We discuss the role of internal operations in a Z spec- i(cid:12)cation, and in particular whether an equivalent speci(cid:12)cation not containing internal operations can be found. The nature of divergence through livelock is also discussed. Correspondence and o(cid:11)print requests to:John Derrick,Computing Laboratory, University of Kent,Canterbury,CT27NF,UK. (cid:3) Thiswork waspartiallyfunded by BritishTelecomResearch Labs.,and the EPSRCunder grantnumberGR/K13035. 2 JohnDerrick,EerkeBoiten,HowardBowmanandMaartenSteen 1. Introduction The Z speci(cid:12)cation language [Spi89] has gained a certain amount of acceptance inthesoftwarecommunityasanindustrialstrengthformalmethod.Zisastate- based language based upon set theory and (cid:12)rst order logic. The most common style of speci(cid:12)cation in Z is the so called \state plus operations" style, where a collectionofoperationsdescribechangestothe statespace.Thestatespaceand operations are described as schemas, and the schema calculus has proved to be an enduring structuring mechanism for specifying complex systems. A growing literature and a number of industrial case studies have demon- strated the usability of the language, and attention is being turned to new do- mainsofapplicability-onesuchexamplebeingtheuseofZforthespeci(cid:12)cation of concurrent and distributed systems [Cus91, Rud91, MZ94, Lam94, Str95]. However, concurrent and distributed systems place a number of requirements on notations used to specify such systems, and, in particular, one aspect that is importantistheroleoftheinternal(orunobservable)operation.Internalopera- tionsarenotpartoftheinterfacetotheenvironment(i.e.theusercannotinvoke them),however,theyareessentialtoourunderstandingandcorrectmodellingof the system. Such operations (or actions) arise naturally in distributed systems, eitherasaresultofmodellingconcurrencyorthenon-determinismthatisinher- entinamodelofsuchasystem.Forexample,internaloperationscanbeusedto model communication (e.g. as in the language CCS [Mil89]), non-determinism arisesas a by-productof this interpretation.Internal operationsarealsocentral to obtaining abstract speci(cid:12)cation through hiding, a particularly important ex- ample of this is to enable communication to be internalised - a central facet in the design of distributed systems. The majority of formal notations which have been designed with concurrent systems in mind have a notion of internal action, event or operation as part of the language or its semantics. Examples include CCS [Mil89], CSP [Hoa85] andLOTOS[BB88].In particular,internaleventshaveanimportantrolein the theory of process algebras, and a special symbol is reserved for the occurrence of such an internal event (e.g. i in LOTOS or (cid:28) in CCS). In addition to the description, i.e., speci(cid:12)cation, of a system an important bene(cid:12)tthatformalmethodso(cid:11)eristheabilitytodevelopasystem'sspeci(cid:12)cation according to some theory of re(cid:12)nement in that language. Examples include the use of re(cid:12)nement in Z [Spi89, WD96], VDM [Jon89] or bisimulation in a pro- cessalgebra[Mil89]. However,if internaleventsaredistinguishedinaparticular speci(cid:12)cationnotation,thenthetheoryofre(cid:12)nementinthatlanguageshoulddeal with such internal events in an appropriateway.One way is to treat an internal eventnodi(cid:11)erentlyfromobservableevents,thestrongbisimulationrelationina processalgebraisanexampleofanequivalencerelationadoptingsuchaconven- tion.However,itiswellrecognisedthatstrongbisimulationisinappropriateasa re(cid:12)nement relation because it discriminates too many speci(cid:12)cations that might reasonably be seen as equivalent. Therefore internal events in re(cid:12)nement and equivalencerelationstypicallyhaveadi(cid:11)erentrolethantheobservableeventsof the system. Examples of relations in which the observable is di(cid:11)erentiated from the internal are weak bisimulation [Mil89], testing equivalence [Bri88], reduc- tion and extension [BSS86], failures re(cid:12)nement [Hoa85] and Hennessy's testing pre-orders[Hen88]. Central to these relationsis the understanding that internal eventsareunobservable,andthatre(cid:12)nementrelationsmustre(cid:12)netheobservable behaviourofaspeci(cid:12)cationdi(cid:11)erentlyfromtheinternalaspectsofitsbehaviour. SpecifyingandRe(cid:12)ninginternaloperationsinZ 3 NowthatZisbeingusedforthespeci(cid:12)cationofconcurrentordistributedsys- tems,anumberofauthorshaverecognisedtheneedtoexplicitlyspecifyinternal operationsseparatelyfromtheobservableinterface,andanumberofconventions have been adopted for their description. In each case the internal operation is speci(cid:12)ed as normal and either has a distinguished name or informal commen- tarytellingusthat it isnotpartofthe interfacetothe environment(wewill see examplesofbothapproachesbelow).Thisapproachimmediatelyraisestwoques- tions. Firstly, is it possible to dispense with such internal operations by adding theirbehaviourtotheobservableinterfacein somefashion?Secondly,ifinternal operations are to appear explicitly in a Z speci(cid:12)cation, we need to consider the possibilityofre(cid:12)ningthesespeci(cid:12)cations.Howshouldwetreatthere(cid:12)nementof internal operationsin Z? This paper seeksto addressthese issues.In particular, we shall show that the standard Z re(cid:12)nement rules are inappropriate for the re(cid:12)nement of internal operations. We make a proposal called weak re(cid:12)nement which seeks to o(cid:11)er a correct generalisation of re(cid:12)nement when speci(cid:12)cations contain internaloperations.This hasa similarrelationto ordinaryZ re(cid:12)nement as weak bisimulation does to strong bisimulation in a process algebra. In par- ticular, we de(cid:12)ne weakre(cid:12)nement by consideringthe stand point of an external observer of the system, who manipulates operations in the user interface. Such an external observer will require that a retrieve relation is still de(cid:12)ned betweenthestatespacesoftheabstractandconcretespeci(cid:12)cationsandthateach abstract observable operation AOp is recast as a concrete observable operation COp. The weak re(cid:12)nement relation is de(cid:12)ned to ensure that the observable behaviouroftheconcretespeci(cid:12)cationisare(cid:12)nementoftheobservablebehaviour of the abstract speci(cid:12)cation. We will also consider to what extent internal operations are necessary and whether we can dispense with them. For speci(cid:12)cations that do not contain live- lock(i.e.,in(cid:12)nitesequencesofinternalevents)wewillarguethatwecandispense withtheexplicituseofinternaloperationsinthespeci(cid:12)cation.Forspeci(cid:12)cations containingdivergenceintheformoflivelockwhetherwecandispensewith their explicit speci(cid:12)cation will turn out to depend on the interpretationof divergence used. Throughout the paper we assume the state plus operations style of Z speci- (cid:12)cation, and our discussion takes place within that context. The structure of the paper is as follows. In Section 2 we review the use of internal operations in Z speci(cid:12)cations. Section 3 presents an example of a speci(cid:12)cationandre(cid:12)nementinvolvinginternaloperations,theexampleillustrates thatstandardZre(cid:12)nementisinappropriateinthepresenceofinternaloperations. Section 4 formulates the generalization that we call weak re(cid:12)nement, which is motivated by the treatment of internal events in process algebras. Section 5 revisits the protocol example to show that weak re(cid:12)nement has the required propertiesofare(cid:12)nementwhereinternaloperationshavebeenspeci(cid:12)ed.Section 6 considers whether we can dispense with internal operations and the role of divergence in answering that question. Section 7 discusses some properties of weakre(cid:12)nement, relatedworkis then reviewedin Section 8,and we conclude in Section 9. 4 JohnDerrick,EerkeBoiten,HowardBowmanandMaartenSteen 2. Internal Operations In the traditional approach to the speci(cid:12)cation of sequential systems in Z, the operations speci(cid:12)ed represent the interface to the environment. That is, a state changeoccursinthesystemifandonlyiftheenvironmentinvokesoneoftheop- erations. Eachoperation therefore representsa potential observable event of the system under construction, and this is usually an acceptable model. However, when modelling concurrent and distributed systems it is convenient to model internal events. These internal events represent operations over which the en- vironment has no control (hence the name internal), but are still necessary to specify in a full description of the system. Since they are not part of the envi- ronmental or user interface they can be invoked by the system whenever their pre-conditions hold. They can arise either due to the natural non-determinism of a distributed system [Hoa85], or due to communication within the system [Mil89] or due to some aspect of the system being hidden at this level of ab- straction[BB88].Thenecessityforthe speci(cid:12)cationofinternaleventsin process algebras is well recognised [Mil89], and a number of researchers have found it convenient or necessary to specify internal operations in Z when specifying dis- tributed systems [CW92, WJ94, Raf94, Str95, WD96, DBBS96a]. Forexample,Strulo[Str95]considerstheuseofZinnetworkmanagementand describestheneedforbothobservableandinternaloperationsinthisapplication area.A particular example is described of a network manager'sview of a router within a network. There, alarm noti(cid:12)cations are a typical example of internal events which are speci(cid:12)ed as usual but with informal commentary describing which operationsareobservableand whichareinternal. A similar approachand application area is described in [WJ94, Raf94]. CusackandWezeman,in[CW92],adoptanumberofconventionsfortheuse of Z for the speci(cid:12)cation of OSI network management standards. In particular, they makethe distinction between internaland observableoperationsaccording towhetheranoperationhasinput/output:operationswhich use(cid:1)State buthave neitherinputoroutputvariables areinternal(unobservable)actions,correspond- ing to the internal event in LOTOS. All other operations can be thought of as interactions with the environment, or external operations [CW92]. Their work is placed in an object-oriented setting and they consider notions of subtyping based upon conformance instead of re(cid:12)nement. In [DBBS96a] a distinguishing name (i) is used to denote which operations are internal. The motivation there was to provide a direct mapping between events in LOTOS and operations in Z in order to support the use of multiple viewpoints in the Open Distributed Processing reference model [ITU95]. Woodcock and Davies [WD96] also use informal commentary to describe which operations are internal and which are observable. They also comment on whether these internal operations add to the expressive power of the language, saying: It should be clear that we could dispense with such operations, but only by adding the required degree of non-determinism to the remainder of the speci- (cid:12)cation. We will give a constructive proof of this statement in Section 6. Evans in [Eva97] considers the use of Z for the speci(cid:12)cation of parallel sys- tems,andinparticulardiscussesissuesoflivenessandfairnessindynamicspeci- (cid:12)cations.Internaloperationsarespeci(cid:12)edasin[WD96],andhealsoconsidersthe re(cid:12)nement relations needed for Z speci(cid:12)cations of concurrent systems. Similar workhasappearedinotherstate-basedformalisms.Forexample,Butler[But97] considers the speci(cid:12)cation and re(cid:12)nement of internal actions in the B method SpecifyingandRe(cid:12)ninginternaloperationsinZ 5 [Abr96]. There, internal actions are speci(cid:12)ed explicitly in an abstract machine. Additional work in this area also includes the work of Lano, e.g. [Lan97]. Ineachcasetheinternaloperationisspeci(cid:12)edasnormalandeitherhasadis- tinguishednameorinformalcommentarytellingusthatitisnotpartoftheuser interface. We will see examples of both below.Used in this way,Z is clearly suf- (cid:12)cient as anotationfor the speci(cid:12)cation ofinternal operationsorevents,and as canbeseenfromtheexamplesreferencedabove,internaleventsareneededwhen Z is used to specify parts of a distributed system which contain large amounts of state information. Typical of this application area are managed objects or the information viewpoint of the Open Distributed Processing reference model, where the speci(cid:12)cations contain a lot of state but there is also a need to model internal operations such as alarms. This section has reviewed the use of internal operations in Z speci(cid:12)cations, the next section considers an example of their speci(cid:12)cation and re(cid:12)nement. 3. Re(cid:12)nement A Z speci(cid:12)cation describes the state space together with a collection of opera- tions. The Z re(cid:12)nement relation [Spi89, WD96], de(cid:12)ned between two Z speci(cid:12)- cations, allows both the state space and the individual operations to be re(cid:12)ned y in a uniform manner . Operationre(cid:12)nementistheprocessofrecastingeachabstractoperationAOp into a concrete operation COp, such that, informally, the following holds. The pre-condition of COp may be weaker than the pre-condition of AOp, and COp mayhaveastrongerpost-conditionthanAOp.Thatis,COp mustbeapplicable whenever AOp is, and if AOp is applicable, then every state which COp might produce must be one of those which AOp might produce. Data re(cid:12)nement ex- tendsoperationre(cid:12)nementbyallowingthestatespaceoftheconcreteoperations to be di(cid:11)erent from the state space of the abstract operations. Consider an abstract speci(cid:12)cation with state space Astate, operation AOp, andinitialisationAinit,andare(cid:12)nedspeci(cid:12)cationwithstatespaceCstate,oper- ationCOp,andinitialisationCinit.Re(cid:12)nementisde(cid:12)nedintermsofanabstrac- tionschemaorretrieverelation,usuallycalledRet,Retrieve orAbs,whichrelates the abstract and concrete states. It has the same signature as Astate ^Cstate, and its property holds if the concrete state is one of those which represent the abstract state [Spi89]. The retrieve relation does not need to be total nor func- tional. The concrete speci(cid:12)cation is a re(cid:12)nement of the abstract speci(cid:12)cation if the following conditions hold: 0 0 0 Initialisation 8Cstate (cid:15)Cinit `9Astate (cid:15)Ainit ^Ret Applicability 8Astate; Cstate (cid:15)preAOp^Ret `preCOp 0 0 Correctness 8Astate; Cstate; Cstate (cid:15) preAOp ^Ret ^COp ` 9Astate (cid:15) 0 Ret ^AOp An illustration of re(cid:12)nement will be given in the following subsection. Thereisagrowingbodyofexperienceandliteratureconcerningre(cid:12)nementin thetraditionalcontextofsequentialsystemsspeci(cid:12)edinZ,e.g.[WD96].However, y We consider only re(cid:12)nements de(cid:12)ned by forward simulations in this paper. Similarresults couldbeobtained forbackwardssimulationsifneeded. 6 JohnDerrick,EerkeBoiten,HowardBowmanandMaartenSteen thesere(cid:12)nementrulesassumealloperationsareobservable.Howdoesre(cid:12)nement behave if some of the operations are internal or unobservable? Asanillustrationofre(cid:12)nementinvolvinginternaloperationsweconsiderthe speci(cid:12)cation and re(cid:12)nement of a telecoms protocol (the Signalling System No. 7 standard) adapted from [WD96, HMR89]. The (cid:12)rst speci(cid:12)cation de(cid:12)nes the external view of the protocol, subsequently we develop a sectional view which speci(cid:12)es the route that messages take through the protocol. [HMR89] discusses the formalisation of the informal speci(cid:12)cation in more depth, our purpose here is to use the formalisation given in [WD96] as an illustrative example. 3.1. Speci(cid:12)cation 1: the external view LetM bethe setofmessagesthatthe protocolhandles.Thestateofthe system is represented by the state schema Ext, and comprises two sequences which represent messages that have arrived in the protocol (in), and those that have been forwarded (out). Ext in;out :seqM a 9s :seqM (cid:15)in =s out Incomingmessagesareaddedtothe left ofin, and themessagescontainedin in but not in out represent those currently inside the protocol.The state invariant speci(cid:12)es that the protocol must not corrupt or re-order. Initially, no messages have been sent, and this is speci(cid:12)ed by the following initialisation schema: 0 0 ExtInit =b [Ext jin =hi] The speci(cid:12)cation at this level is completed by the description of two op- erations which model the transmission (Transmit) and reception (Receive) of messages into and out of the protocol. In the speci(cid:12)cation of the Receive op- eration, either no message is available (e.g. all messages are en route in the protocol) or the next one is output, at this level of abstraction this choice is z made non-deterministically. The speci(cid:12)cations are straightforward . Transmit (cid:1)Ext m?:M 0 a in =hm?i in 0 out =out Receive (cid:1)Ext 0 in =in 0 0 #out =#out +1_out =out z TheReceive operationcould,ifdesired,actuallyoutputthetransmittedvalue,howeverthis isimmaterialtoourconcernshere. SpecifyingandRe(cid:12)ninginternaloperationsinZ 7 3.2. Speci(cid:12)cation 2: the sectional view The second speci(cid:12)cation describes the sectional view which speci(cid:12)es the route the messages take through the protocol in terms of a number of sections. Each sectionintheprotocolmayreceiveandsendmessages,andthosewhichhavebeen received, but not yet sent on, are in the section. The messagespass through the sections in order. Let N be the number of sections. In the state schema, ins i represents the messages currently inside section i, rec i the messages that have beenreceivedbysectioni, andsent i themessagesthathavebeensentonwards from section i. The state and initialisation schemas are then given by Section SectionInit 0 rec;ins;sent :seq(seqM) Section N =#rec =#ins =#sent 8i :1::N (cid:15) rec =ins aasent rec0 i =ins0 i =sent0 i =hi frontsent =tailrec aa where denotes pairwise concatenation of the two sequences (so for every i a we have rec i =ins i sent i). The predicate frontsent =tailrec ensures that messagesthataresentfromonesectionarethosethathavebeenreceivedbythe next. This speci(cid:12)cation also has operations to transmit and receive messages, and they are speci(cid:12)ed as follows: STransmit (cid:1)Section m?:M 0 a headrec =hm?i (headrec) 0 tailrec =tailrec 0 sent =sent SReceive0 (cid:1)Section 0 rec =rec 0 frontins =frontins 0 lastins =front(lastins) 0 frontsent =frontsent 0 a lastsent =hlast(lastins)i (lastsent) SReceive =b SReceive0_(cid:4)Section Here, the new message received is added to the (cid:12)rst section in the route by the operation STransmit. The operation SReceive will deliver a message from the last section in the route.Intheexternalviewpresentedabove,messagesarrivenon-deterministically because we did not model the interiorof the protocol.In the sectional view this non-determinismisrepresentedbytheprogressofthemessagesthroughthesec- tions.Thereforeinthismoredetaileddesign,weneedtospecifyhowthemessages makeprogressthroughthe sections.We dosobyde(cid:12)ning anoperationDaemon 8 JohnDerrick,EerkeBoiten,HowardBowmanandMaartenSteen which non-deterministically selects a section to make progress. The oldest mes- sage is then transferred to the following section, and nothing else changes. The important part of this operation is given by: Daemon0 (cid:1)Section 9i :1::N (cid:0)1j ins i 6=hi(cid:15) 0 ins i =front(ins i) 0 a ins (i +1)=hlast(ins i)i ins(i +1) 0 8j :1::N jj 6=i ^j 6=i +1(cid:15)ins j =ins j Theinformalcommentaryaccompanyingthespeci(cid:12)cationtellsusthatDaemon is an internal operation, and so can be invoked by the system whenever its pre- condition holds. As noted in [WD96]: This operation is not part of the user in- terface. The usercannotinvoke Daemon, butitisessential toourunderstanding of the system and to its correctness. The sectional view is in some way a re(cid:12)nement of the external view, where the retrieve relation is given by: Retrieve Ext Section headrec =in lastsent =out We note that the retrieve relation used here is a total function, i.e., 8Section (cid:15) 91Ext (cid:15)Retrieve. Under this re(cid:12)nement STransmit and SReceive correspond to Transmit and Receive respectively, and the internal operation Daemon correspondsto the ex- ternal operation (cid:4)Ext, i.e. the identity operation on Ext. The re(cid:12)nement is proved correct by showing that (where we have omitted the appropriate quan- ti(cid:12)cation over the states): 0 SectionInit ^Retrieve )ExtInit preTransmit ^Retrieve )preSTransmit 0 preTransmit ^Retrieve^STransmit^Retrieve )Transmit preReceive^Retrieve )preSReceive 0 preReceive^Retrieve^SReceive^Retrieve )Receive pre(cid:4)Ext ^Retrieve )preDaemon 0 pre(cid:4)Ext ^Retrieve^Daemon^Retrieve )(cid:4)Ext The re(cid:12)nement is discussed in [WD96]. This completes the (cid:12)rst re(cid:12)nement of the external view. Letussummarisethe situationsofar.Wecanspecifyasystemthatcontains non-determinism in some of the operations in its user interface (e.g. Receive), but which does not contain any internal operations. We can then re(cid:12)ne this speci(cid:12)cation to one that contains internal operations that correctly models (in the sense of a re(cid:12)nement existing between the speci(cid:12)cations) the abstract spec- i(cid:12)cation. We have used the standard Z re(cid:12)nement relations, which have been perfectly adequate at this level. SpecifyingandRe(cid:12)ninginternaloperationsinZ 9 3.3. Speci(cid:12)cation 3: re(cid:12)ning internal operations However, let us look at the re(cid:12)nement of the internal operation Daemon again. As it stands Daemon0 represents the functionality that for non-empty sections (ins i 6= hi) we transfer a message along the sections. But in order that the completeoperationDaemon re(cid:12)nes(cid:4)Ext,Daemon0 mustbeextendedtoensure that pre(cid:4)Ext ^Retrieve )preDaemon i.e. that Daemon is alwaysapplicable. This means that the internal operation Daemon can always be invoked by thesystem,andthereforewehaveintroducedlivelockintothespeci(cid:12)cation.This would not be acceptable in an implementation. The alternative to this would be to leave Daemon as Daemon0, i.e., just specify the intended behaviour. However,now it is not a re(cid:12)nement since pre(cid:4)Ext ^Retrieve )preDaemon fails. We will return to this point later. Suppose for the moment that we are given the sectional view speci(cid:12)cation containing an internal operation Daemon =b Daemon0, we can now re(cid:12)ne this further. In particular we can re(cid:12)ne the Daemon operation. This operation is partial (asit does not specify what happens if ins i =hi foreveryi), and using thestandardZre(cid:12)nementruleswecanweakenitspre-condition,andre(cid:12)neitto the following: NDaemon (cid:1)Section 0 (8i :1::N (cid:0)1; 9m :M (cid:15)ins i =hi^ins 1=hmi) _ (9i :1::N (cid:0)1j ins i 6=hi(cid:15) 0 ins i =front(ins i) 0 a ins (i +1)=hlast(ins i)i ins(i +1) 0 8j :1::N jj 6=i ^j 6=i +1(cid:15)ins j =ins j) Thisoperationincludesthesamefunctionalityasbefore,exceptthatinaddition the system can invoke it non-deterministically (since it is an internal opera- tion) initially to insert an arbitrarymessageinto the (cid:12)rst section. Thus initially there are two possible behaviours of the system: as before the user could in- voke Transmit to insert a message into the protocol, or now the system could non-deterministically invoke NDaemon which corrupts the input stream of the 0 protocol before the user has inserted any messages (ins 1=hmi). The speci(cid:12)cation which contains the sectional view operationstogetherwith this new NDaemon in place of Daemon is a re(cid:12)nement of the sectional view. Yet clearly implementations which introduce arbitrary amounts of noise into a stream of protocol messages are unacceptable. But in these situations, using standard Z re(cid:12)nement this has been allowed to happen, what has gone wrong? We have used standard Z re(cid:12)nement here, and at issue is the re(cid:12)nement of internal operations. Internal operations have behaviour which isn't subject to the normal interpretation of operations that are in the user interface, therefore 10 JohnDerrick,EerkeBoiten,HowardBowmanandMaartenSteen it is not surprising that the standard re(cid:12)nement rules bring about unexpected and undesirable consequences. Furthermore, the standard re(cid:12)nement rules allow the possibility of livelock ordivergencetobeaddedwhenwere(cid:12)neaninternaloperation.Forexample,the Daemon internaloperationinthesectionalviewcouldbereplacedbyadivergent version, DDaemon, speci(cid:12)ed by: DDaemon (cid:1)Section 0 ins =ins Thespeci(cid:12)cationcontainingthisoperationasaninternaloperationisare(cid:12)ne- ment of the externalview.However,the systemnowcontainsdivergencein that DDaemon can be invoked non-deterministically an arbitrary number of times, causing a livelock. The introduction of livelock is not due to the introduction of an internal operation Daemon re(cid:12)ning the identity on Ext, (cid:4)Ext. To see this it is su(cid:14)cient to note that a divergent version of NDaemon given by DNDaemon (cid:1)Section 0 (8i :1::N (cid:0)1(cid:15)ins i =hi^ins =ins)_ (9i :1::N (cid:0)1j ins i 6=hi(cid:15) 0 ins i =front(ins i) 0 a ins (i +1)=hlast(ins i)i ins(i +1) 0 8j :1::N jj 6=i ^j 6=i +1(cid:15)ins j =ins j) isare(cid:12)nementofDaemon,andintroducessimilarpotentiallivelockattheinitial system state. Theweakre(cid:12)nementrulespresentedbelowwillcontaintwoconditionswhich are necessaryand su(cid:14)cient to prevent divergence being introduced upon re(cid:12)ne- ment. An alternative approach to these rules which explicitly prevent livelock beingintroducedistoadoptanon-catastrophicinterpretationofdivergence,this approach is discussed in Section 6.1 below. 3.4. The (cid:12)ring condition interpretation The (cid:12)ring condition interpretation is a potential solution to the problems en- counteredwhenre(cid:12)ninginternaloperationsdescribedbyStruloin[Str95].Ithas the merit of simplicity, but, as we shall see, perhaps constrains re(cid:12)nement too far. Strulo calls internal operations active, and operations in the user interface passive. The (cid:12)ring condition interpretation is the idea that the pre-condition of an operation speci(cid:12)es when the operation can happen instead of saying that an operation is unde(cid:12)ned, but possible, outside its pre-condition. That is, the pre-condition represents the guard of an operation. To de(cid:12)ne re(cid:12)nement, Strulo identi(cid:12)es three regionsfor an operation (uncon- strained, empty and interesting). The three regions of an operation represent: