ITU-T HDBK VOL I CFD-1982 Chill Formal Definition Part I Part II Part III (Volume I 105 pp)《冷正式定义 第1 2和3部分 第1册 105页》.pdf

1、STD*ITU-T HDBK VOL I CFD-ENGL 1782 m 4862571 0682768 320 b INTERNATIONAL TELECOMMUNICATION UNION CCITT THE INTERNATIONAL TELEGRAPH AND TELEPHONE CON SU LTATIVE COM M IllE E CHILL Formal Definition Volume I Part I Part II Part III Geneva 1982 STD.ITU-T HDBK VOL I CFD-ENGL 1982 E 4862571 Ob2b7 267 m I

2、NTERNATIONAL TELECOMMUNICATION CCITT THE INTERNATIONAL TELEGRAPH AND TELEPHONE CONSULTATIVE COM MIlTEE UNION CHILL Forma I Definit ion Volume I Part I Part II Part III Geneva 1982 STDmITU-T HDBK VOL I CFD-ENGL 1942 = Y862591 0682970 TB9 SB O I.T.U. STD-ITU-T HDBK VOL I CFD-ENGL 1982 E 4862593 068297

3、1i 935 m Volume I CONTENTS Part I: Prelude 10 pages Part II: Meta Notation Summary 18 pages Part 111.1 : Annotations to Context Conditions 35 pages Part 111.2: Annotations to Dynamic Semantics 26 pages STD-ITU-T HDBK VOL I CFD-ENGL L982 4862592 Ob82772 851 9 CHILL Formal Definition Part I Prelude Pa

4、rt 1/1 1 . INTRODUCTION . 3 2 . MOTIVATION AND PURPOSES 4 3 . FORMAL DEFINITION METHOD . 5 3.1. Reasons for choosing Denotational Semantics 5 3.2. Reasons for choosing the Vienna Development Method 5 3.3. On Denotational Semantics . 5 3.3.1. The Notion of Store . 5 3.3.2. The Notion of State . 5 3.3

5、.3. The Notion of Environment 6 3.3.4. Denotations 6 3.3.5. The Homomorphism-Denotational Semantics Rule 6 3.3.6. Basic Parts of a Denotational Semantics Definition . 6 3.3.7. Static and Dynamic Semantics . 6 3.3.8. The Notion of Control Flow 7 3.4. On Abstractly Modelling CHILL Concurrent Execution

6、 . 7 3.4.1. Non-determinism 7 3.4.2. Fairmerging 7 3.4.3. Non-determinism and Fairmerging 8 3.4.4. Short-term Scheduling Simplifications . 8 4 . MODEL OVERVIEW 9 4.1. Program Transformation 9 4.2. Context Conditions 9 4.3. Dynamic Semantics . 10 4.4. Interpreting a CHILL program . 10 4.5. Subject of

7、 Definition 10 STDmITU-T HDBK VOL I CFD-ENGL 1982 W 4862551 Ob82974 624 INTRODUCTION Part 113 1. INTRODUCTION This formal definition of the CHILL programming language supplements the description given in CCITT Recommendation 2.200. The formal definition is separated into two volumes and four parts.

8、Volume I contains parts I, II and III, and volume II contains part IV. The purpose of this prelude, part I, is to explain the reasons for choosing a formalized definition of CHILL, the specific method used herein, and the particular composition of the formal model. Part II represents a very terse re

9、ference manual to the meta-language notation used. It is not meant to be a tutorial on, or a guide to, the proper use of the notation; merely a place in which to look up the meaning of particular, concrete meta-language constructs. l) Part III contains annotations to part IV. The formulae of part IV

10、 may appear very dry. Annotations serve the point of rendering these formulae more readable. Ideally every formula line should be accompanied by a slightly technical, but mostly natural language text, expressing in words what the formulae purport to express. Since such words are already found in 2.2

11、00. the main part of the recommendation, we instead focus on technical details, and otherwise refer to specific paragraphs of 2.200. Part IV contains the formal definition itself. It has one minor and two major parts. First a proper basis of the formal definition is given. Then is given the syntax o

12、f CHILL together with all statically decidable context conditions, also referred to as static semantics. Then is given the dynamic semantics. The former part refers to what is exclusively the job of a CHILL compiler system, whereas the latter part exclusively deals with run-time properties. 1. “The

13、Vienna Development Method: The Meta-Language“ (Eds. D. jerner used in holding signals sent but not yet received; etc. In this definition all such state components are imperatively modelled by appropriately declared, global meta-variables. In denotational semantics one associates with each language c

14、onstruct its denotation. For actions these are functions from STD-ITU-T HDBK VOL I CFD-ENGL 3982 4862593 0682777 333 Part 1/6 PRELUDE states to states. For expressions they can (simplifying) be considered functions from states to values. 3.3.3. The Notion of Environment The store component of the st

15、ate forms a semantic Domain which serves to capture the notion of variables and their values. To capture the notion of scope-determined name-binding another semantic domain construct, the environment, is introduced. It records the denotation of names of a CHILL program. 3.3.4. Denotations The denota

16、tion of a variable identifier ( is a location, where a store is a map from locations to values. The denotation of a subroutine-like procedure identifier is a function from argument value lists to functions from states to states. Hence, when such a procedure is called, its denotation is applied to an

17、 argument list and a state, resulting in a new state. If the procedure returns a value then its denotation is normally taken to be that of a function from argument value lists to functions from states to states and values. Thus, when such a procedure is called, its denotation is applied to an argume

18、nt list and a state and yields a new state and a resulting value. 3.3.5. The Homomorphism-Denotational Semantics Rule For a semantics definition to be denotational the definition of the semantics of a composite (syntactic) construct must be a function, Fct, of the semantics of each individual, const

19、ituent construct. Let fcl,c2, ., c,J represent a composite CHILL construct, with c, for all i, represents simple or composite CHILL constructs. Let Sem designate the semantics (finding) function, then the denotational semantics rule can be phrased: Semlc, , c2,. . ., c,l = Fct fSem(c,l, Semlc,), . .

20、 . , Semlc Jl Sem and Fct are usually defined in terms of various kinds of semantic Domain objects, like stores and environments. 3.3.6. Basic Parts of a Denotational Semantics Definition Establishing a denotational semantics definition of CHILL therefore amounts to the stepwise establishment of a n

21、umber of definitions: (1 1 (2) (3) First we define the Domains of syntactic CHILL constructs. Then we define the Domains of semantic objects: stores, environments, etc Finally we define the Elaboration functions which to every syntactic construct ascribes its meaning: Ffs ynllsem-list) = Body type:

22、SYN -+ (SEM, SEM, . SEM, I-, SEMI here SYN, SEW. and SEM denote the Domains, - the logical types - of the syntactic input object, the semantic input objects and the resulting object. The latter is, in Denotational Semantics, always taken to be a semantic object. The above is a simplified exposition.

23、 It is now expanded upon. 3.3.7. Static and Dynamic Semantics The BNF grammar specifies certain strings to be valid program texts. There are, however, rules, called static semantics rules, or (static) context conditions, that these syntactically valid program texts should satisfy. To determine wheth

24、er an occurrence, in a CHILL program, of a language construct is valid, (a summarization of) the context in which it occurs is required. In connection with Static Semantics we term this summarization a Dictionary. (in the context of Dynamic Semantics it is called an Environment.) Now functions, whos

25、e names usually have the prefix: is-wf- (for is-well-formed), can be defined which apply to syntactic constructs and dictionaries and yield a truth value designating whether or not the construct is well-formed, .e. satisfies the context conditions, in the surroundings summarized by the dictionary. I

26、n summary: functions checking program text properties purely on the basis of the program text alone are called Static Semantics Functions or Context Condition Functions. Functions ascribing meaning to program texts, .e. such functions which can be understood (and read) as interpreting, or more collo

27、quially “executing“, program texts, are called Dynamic Semantics Functions or Elaboration Functions. STDmITU-T HDBK VOL I CFD-ENGL 1982 48b259L Ob82978 27T FORMAL DEFINITION METHOD Part 1/7 Semantics functions are really defining what the whole thing is about. Such functions usually require, as brou

28、ght up in the introduction to this chapter, environments and stores as “semantic“ arguments. The “content“ of environment codomains and of stores is only knowable at execution-, .e. run-time. The Static Semantics functions are all expected to be realized by a compiler, whereas the Dynamic Semantics

29、functions correspond to the target machine code generated by such a compiler. 3.3.8. The Notion of Control Flow To capture the notion of control flow (statement sequencing or evaluation order), whether normal, as when obeying a source semicolon “;“), or abnormal, as when expressing the semantics of

30、GOTOs, EXITS, RETURNS and exceptions, we make use of corresponding, but far simpler notions in the semantics-defining meta-language. Normal control flow, in an applicative definition, is handled by function application, and in an imperative definition by its equivalent: the meta-semicolon “;“ . Abno

31、rmal control flow is handled by the meta-notion of exit. Thus we do not use the more powerful continuation technique. We do not do so for three reasons. It is judged more difficult to comprehend than the exit mechanism; it is far too powerful even for a language the size and complexity of CHILL; and

32、 it requires an applicative definition style where we believe that an imperative definition style is more suitable for the intended audience of the definition. 3.4. On Abstractly Modelling CHILL Concurrent Execution To cope with the notion of processes (in the source language CHILL) we introduce, in

33、to the meta-language, a notion of meta-processes. To each actually started, and not yet stopped CHILL process, whether actually running or temporarily delayed, there corresponds exactly one meta-process, denoted by the process processor. CHILL processes may share storage, for instance by global decl

34、arations and by parameter passing. As a consequence we have decided to collect storage of all processes (whether actually shared or not), in a separate, single meta-process denoted by the storage-handler processor. Two or more separately active CHILL processes may independently request the mutually

35、exclusive execution of a critical procedure of a region. As a consequence we have decided to establish a single, separate meta-process which arbitrates between CHILL processes all wishing to execute critical procedures of shared regions. This, the monitor, short-term schedules CHILL processes waitin

36、g for critical procedure execution. For similar reasons separate meta-processes have been established for each of the three remaining process primitives: Events, Buffers and Signals. All of the Region-, Event-, Buffer- and Signal handler meta-processes together with a few, well-isolated aspects of t

37、he CHILL- and Storage Handler meta-processes, can be said to define all of concurrent CHILL. The notion of a meta-process is far simpler, of course, than the notion of a CHILL process. Meta-processes share no resources, thus they do not share meta-variables. Meta-processes need to communicate. The m

38、eans of communication is that of output/input messages in the style of the “CSP: Communicating Sequential Processes“ -language well-described in the literature. 3.4.1. Non-determinism Existing, published formal mathematical (but not denotationall models of our meta-process notion, and of CSP, attemp

39、ts to capture the notion of non-determinism. This notion is briefly characterized by the following: (1) If two or more processes “simultaneously“ wish to access a shared resource, then the abstract model implies a non-deterministic selection (or: scheduling). That is an arbitrary one of the processe

40、s is picked first, etc If, as in e.g. the receive case action of CHILL, two or more alternatives are potential candidates for execution, .e. if they otherwise satisfy candidate requirements, then one of them is arbitrarily chosen - again a non-deterministic choice. (2) 3.4.2. Fairmerging Fairmerging

41、 is the following: guarantee finite, “ pseudo-equal or balanced“ progress, in any time interval, of any CHILL process which is desiring to progress. But the “state-of-the-art“ of defining fairmerging mathematically, let alone denotationally, had, at the time that the major parts of this supplement w

42、ere readied, not progressed to the point where a definition could be constructed which specifies the degree of fairmerging that any realization should satisfy. STD-ITU-T HDBK VOL I CFD-ENGL 1982 W 4862591 0682979 10b Part 1/8 PRELUDE 3.4.3. Non-determinism and Fairmerging As a result the model, part

43、ly implicitly: through the semantics of the meta-process constructs, partly through explicit definitions, captures all desired aspects of non-determinism. The same model prescribes no fairmerging requirements. These have now been informally and incompletely specified by the last sentence of previous

44、 paragraph. 3.4.4. Short-term Scheduling Simplifications Two or more CHILL processes wishing to access ”overlapping”, as well as ” non-overlapping” storage are, however, according to the abstract model, subject to a form of (very) short term scheduling. One is processed before the other, where in fa

45、ct, a realization should be allowed to potentially service such requests simultaneously. Similar remarks can be made about the specification of access to the other resources: critical procedures of distinct regions, independent event- and buffer locations, and actual handling of signals. The problem

46、 of specifying the highest degree of simultaneous scheduling of processes requesting access to independent resources is, in general, practically unsolvable. One could easily device means of specifying increased simultaneity, but this leads, in all the cases considered, to vastly more detailed, and h

47、ence more opaque, specifications. This was deemed too high a price to pay; and it was consequently not attempted. STD*ITU-T HDBK VOL I CFD-ENGL 1982 4862591 Ob82980 328 = MODEL OVERVIEW Part 1/9 4. MODEL OVERVIEW The formulae fall in three parts, each based on its own abstract syntax. 4.1. Program T

48、ransformation The abstract syntax (AS,) of this first part is derived directly (rule by rule) from the Backus-Naur (context sensitive) concrete syntax of Recommandation 2.200. It includes derived syntax (as defined in 2.2001, when this may be abstractly modelled (e.g. multiple array indexing and lev

49、el number notation for structure modes is found in AS, whereas e.g. the optional keyword CALL for procedure calls and the use of = instead of : = is not). The purpose of this part is to provide a mutual starting point - namely the concrete syntax of CHILL - for the informal and the formal definitions. The formulae of this part transform a program satisfying AS, into a program satisfying the abstract syntax of the context conditions (AS, ). This transformation changes derived syntax into strict syntax, and involves furthermore the enforcement of (very) few static con