ITU-T HDBK VOL II CFD-1982 Chill Formal Definition Part IV (Volume II)《冷正式定义 第4部分 第2册》.pdf

1、 STD-ITU-T HDBK VOL II CFD-ENGL 1982 = 4862593 0682768 567 8 INTERNATIONAL TELECOMMUNICATION UNION CCITT THE INTERNATIONAL TELEGRAPH AND TELEPHONE CONSULTATIVE COM M IlTEE CHILL Formal Definition Volume II Part IV Geneva 1982 - STD.ITU-T HDBK VOL II CFD-ENGL 1782 m 4862593 0bZib1 4T5 1311 INTERNATIO

2、NAL TELECOMMUNICATION UNION CCITT TH E INTERNATIONAL TELEGRAPH AND TELEPHONE CONSULTATIVE COM M IlTEE CHILL Formal Definition Volume II Part IV Geneva 1982 ISBN 92-61 -01681 -2 - STD-ITU-T HDBK VOL II CFD-ENGL I1982 W 4862591 Ob82770 117 O I.T.U. STD-ITU-T HDBK VOL II CFD-ENGL L982 48b259L Ob8277L 0

3、53 II Volume II CONTENTS Part IV. 1 Program Transformation Part IV.2 Context Conditions Part IV.3 Dynamic Semantics 26 pages 91 pages 69 pages STDmITU-T HDBK VOL II CFD-ENGL 2982 II 48b2592 b82772 T9T CHILL Formal Definition Part IV. I Program Transformation STDmITU-T HDBK VOL II CFD-ENGL 1982 II 48

4、62571 Ob82773 92b Program Transformation Part IV.l/l CONTENTS 1 . Prg, and Program Transformation 1.1. Syntactic Domains 1.1 . 1. Program Structuring Domains 1.1.2. Data Statements 1.1 .3 . Mode Expressions 1.1.3.1. Non-composite Mode Expressions . 1.1.3.2. Composite Mode Expressions 1.1.4. Actions

5、1.1.4.1. Bracketed Statement . 1.1.4.2. Simple Statements 1.1.5. Expression . 1.1.5.1. Values . 1.1.5.2. Location Expressions . 1.1.6. Identifiers 1.2. Program Transformation 1.2.1 . transf-Prg, . 1.2.3. transf-returnact, . 1.2.5. transf-ohdl, 1.2.6. transf-Stmt, 1.2.7. transf-If, . 1.2.8. transf-Ca

6、se, 1.2.8.1 . transf-Casealtlist, . 1.2.9. transf-Caselabspec, . 1.2.9.1. transf-Caselablist, . 1.2.1 O . transf-Do, 1.2.10.1. transf-iterlist, 1.2.1 1 . transf-Module, 1.2.1 1 . 1. transf-dvprl, . 1.2.1 2 . transf-Datastmtlist, 1.2.13. transf-Dcllist, 1.2.14. transf-Processdef, 1.2.1 5 . transf-Par

7、m, 1.2.16. transf-Region, 1.2.1 7 . transf-Defstmt, . 1.2.17.1. transf-ores, . 1.2.17.2. transf-Procatt, 1.2.17.3. transf-Pbody, . 1.2.18. transf-Grantstmtlist, 1.2.18.1. getgnames 1 -2.19. transf-Seizestmtlist, 1.2.19.1. getsnames 1.2.20. transf-Begend, 1.2.21. transf-Delaycase, . 1.2.22. transf-Re

8、ceivesgnlcase, 1.2.23. transf-Receivebufcase, . 1.2.24. transf-Asgn, 1.2.25. transf-Update, 1.2.26. transf-Multipleassign, . 1.2.27. transf-Call, . 1.2.28. transf-Start, 1.2.29. transf-Delay, 1.2.30. transf-Sendsgnl, . 1.2.31. transf-Sendbuf, . 1.2.33. transf-Value, 1.2.34. transf-Valexpr, 1.2.34.1.

9、 transf-Oper1 , . 1.2.34.2. transf-Oper2, . 1.2.2. transf-Al, . 1.2.4. transf-Act, 1.2.5.1. transf-Onaltl, 1.2.18.2. transf-oforbid, 1.2.32. transf-Expr, . 1.2.34.3. transf-Oper3, . 3 3 3 3 3 3 4 4 4 5 5 5 6 6 6 7 7 7 7 7 7 8 8 8 9 9 9 9 9 10 10 10 10 11 11 11 11 12 12 12 13 13 13 13 13 14 14 14 14

10、14 15 15 15 15 15 15 16 16 16 16 16 16 16 1.2.34.4. transf.Oper4, 1.2.34.6. transf.Oper6, 1.2.34.5. transf.Oper5, 1.2.34.7. transf.Primitive, . 1.2.35. transf.Locexpr, 1.2.36.2. transf.Altfields, . 1.2.36.4. transf.Fixfields, . 1.2.36.7. defaultpack I .2.36. 8. transf.layout, 1.2.36. transf.Modeexpr

11、, 1.2.36.1. transf.Nestedstruct, . 1.2.36.3. transf.Fixfieldslist, . . 1.2.36.5. transf.Fieldlayoutexpr, . 1.2.36.6. transf.Elemlayoutexpr, . 1.2.36.9. transf.Levelstructme, . 1.2.36.1 O . change.Nlevelfieldslist, INDEX . . . . . . . . . . . . . . . . 17 17 17 17 19 20 22 22 23 23 23 23 23 23 24 24

12、. 25 STD-ITU-T HDBK VOL II CFD-ENGL 1782 4862571 Ob82375 7T9 Syntactic Domains Part iV.l/3 1. Prg, and Program Transformation 1.1. Syntactic Domains 1.1.1. Program Structuring Domains 1 Prg 2 Moduleact 3 Module 4 Region 5 Procdef 6 Processdef 7 Begend 8 Pbody 9 Visibstmt 10 Grantstmt 11 Window 12 Gr

13、antelemlist 13 Forbid 14 Forbidlist 15 Seizestmt 16 Seizeelernlist 17 Parm 18 Parmatt 19 Res 20 Procatt 2 1 Entry 1 .I .2. Data Statements - 1 Datastmt 2 Defstmt - 3 Synmodedef 4 Newmodedef 5 Syndef 6 Signaldef 7 Dclstmt 8 Dcl 9 Locdcl 10 Init 7 1 Reachinit 12 Lifeinit 13 Lociddcl 14 Baseddcl - - 1.

14、1.3. Mode Expressions - 1 Modeexpr Moduleact I Region) + Modid Module Hdn (Datastrnt I Visibstmt I Region) Regid IDatastmt I Visibstmt) HdA Pid ld+ Parm) Res1 Eid Procatt Pbody Hdo Pid lid+ Parmi Begend Hdn Datastmt Actb Datastmt (Act I Entry) Grantstmt I Seizestmt Window PERU Grantelemlist I ALL (I

15、d Forbid) + Forbidlist I ALL Fid + Seizeelemlist I ALL (Id ALL) Modeexpr i Parma ttl Registerid IN I OUT I INOUT 1 LOC Modeexpr LOCI Registerid GENERAL I SIMPLE 1 INLINEI IRECI Lid Act8 Defstmt I Dclstmt Synmodedef 1 Newmodedef I Sync- EMPTY (Id + Modeexpr) + (Id + Modeexpr) + (Id+ Modeexpr Value) +

16、 ld Modeexpr * Pid) + Dcl+ Locdcl I Lociddcl 1 Baseddcl Id + Modeexpr STATIC lnitl Reachinit I Lifeinit Value Hdn Value I. .ocde Id+ Modeexpr Staticlocexpr Hdll Id+ Modeexpr Id Noncornpme I Compme 1 Processdef I 1 .I .3.1. Non-composite Mode Expressions 1 Noncompme 2 Oiscrme 3 lntme 4 Boolme 5 Charm

17、e 6 Setme 7 Setlist 8 Numsetlist 9 Unnumsetlist 10 Rangeme 11 Range Discrme 1 Pwsme I Refme I Procme 1 Instanceme I Syncme lntme 1 Boolme I Charme I Setme I Rangeme READ IINT 1 Id) READ (BOOL I Id) READ (CHAR I Id) READ (Setlist I Id) Nurnsetlist I Unnumsetlist fld ValexPr)+ (Id I HOLE) + IREADI (Ra

18、nge I Bin I Id) Modeidl Rng Qnaldef 1 STDmITU-T HDBK VOL II CFD-ENGL I 4862593 Ob82776 b35 11111 Part IV.1/4 Prg, and Program Transformation 12 Bin 13 Rng 14 Pwsme 15 Refme 16 Boundrefme 17 Freerefme 18 Rowme 19 Procme 20 Proc 2 I lnstanceme 22 Syncme 23 Eventme 24 Event 25 Bufme 26 Buffer - - Valex

19、pr s-lower: Valexpr s-upper: Vafexpr READ Discrme I Id) Boundrefme I Freerefme 1 Rowme READ (Modeexpr I Id) READ PTR 1 Id) READ (Stringme I Arrayme I Id) READ (Proc I Id) Parm* Res Eid* REC READ ONSTANCE I Id) Eventme 1 Bufme READ (Event 1 Id) Valexprl READ (Buffer I Id) Valexprl Modeexpr 1.1.3.2. C

20、omposite Mode Expressions 1 Compme 2 Stringme 3 Nonparmstring 4 Parmstring 5 Arrayme 6 Nonparmarra y 7 Index 8 Parmarray 9 Structrne 10 Nonlevelstructme 1 1 Nestedstruct 12 Fields 13 Fixfields 14 Aftfields 15 Parmstruct 16 Levelstructme 17 Arrayspec 1 8 Nle velfields 19 Nlevelfixfields 20 Nonstructf

21、ields 2 1 Structfields 22 Nlevelaltfields 23 Elemla youtexpr 24 Posexpr 25 Posopt 26 Pos 27 Fieldla youtexpr 28 Stepexpr 1.1.4. Actions I Act 2 Strnt 3 Hdl Stringme I Arrayme 1 Structme READ (CHAR 1 BIT) Valexpr Modeid Valexpr READ Index + Modeexpr Elemla youtexpr * Discrme 1 Rng Modeid Vafexpr Nonl

22、evelstructme I Levelstructrne READ Fields + Fixfields I Altfiefds Id + Modeexpr Fieldla youtexprl Id* Caselabspecl Fixfields *I + Fixfields *I Modeid Valexpr + Arra yspecl READ Nlevelfields + READ Index + Elemla youtexpr * Nle velfix fields I Nlevelaltfields Nonstructfields I Structfields Id+ Modeex

23、pr Fieldla youtexprl Id+ Arrayspec READ Fieldla youtexprl Nlevelfields + Id (Caselabspecl Nlevelfixfields *) + Nlevelfixfields *I NOPACK I PACK I Stepexpr Valexpr Valexpr Valexpr Valexpr Valexpr Valexpr NOPACK 1 PACK I Posexpr Posexpr Valexpr i Valexprll (Nonparmstring I Parmstring I fd) (Nonparrnar

24、ray 1 Parmarra y I Id) (Nestedstruct I Parmstruct 1 Id) Posopt I Pos : Lid Stmt Hdll = Brackstmt I Simpstrnt : (Eid+ Act*)* Act* 1.1.4.1. Bracketed Statement 1 Brackstrnt 2 If 3 Else 4 Case 5 Casealtlist 6 Caselabspec 7 Caselablist 8 Caselab 9 Do 10 Control 11 Forctr 12 lterlist 13 Stepenum 14 Rngen

25、urn I5 Pwsenum - - - - - If I Case I Do I Module I Begend I Delaycase I Receivecase Valexpr Act* Else I lfl Act ValexPr+ Discrrne +I Casealtlist Act *I (Caselabspec Act *) + Caselablist I ELSE 1 IRR)+ Caselab + Valexpr I Rng 1 Modeid Controll Act* Forctr 1 Whcrr 1 Withpart llterlist 1 EVER) Whctrl (

26、Stepenurn 1 Rngenum 1 Pwsenum I Locenum)+ Id c-start: Valexpr s-step: Valexprl DOWNI s-end: Vafexpr Id DOWN Discrrne fd iDOWNI Valexpr Syntactic Domains Part IV.1/5 16 Locenum 1 7 Whctr 18 Withpart 19 Delaycase 20 Delayalt 2 1 Receivecase - 22 Receivesgnlcase : 23 Sgnlreceivealt 24 Receivebufcase 25

27、 Bufreceivealt 1 .I .4.2. Simple Statements - 1 Simps tm t 2 Assign 3 Singleassign 4 Asgn 5 Update 6 Updop 7 Multipleassign 8 Call 9 Birproccall IO Exit 11 Return 12 Result 13 Goto 14 Assert 15 Start 16 Delay 17 Continue 18 Send 19 Sendsgni 20 Sendbuf 2 1 Cause - - - - 1 .I .5. Expression - 1 Expr 1

28、 .I .5.1. Values 1 Value 2 Valexpr 3 Oper1 4 Oper2 5 Op3 6 Relop 7 Pwsinclop 8 Oper3 9 Op4 10 Armaddop Il Pwsdifop 12 Oper4 13 Armultop 14 Oper5 15 Mop 16 Oper6 17 Primitive 18 Deloc 19 Valuename 20 Literal - 2 1 lntlit 22 Boollit 23 Setlit 24 Proclit 25 Chrstrlit 26 Bitstrlit id DOWN Locexpr Valexp

29、r (Locexpr 1 Valexpr) + ILocexpd s-priority: Valexprl Dela yalt + Locexpr+ Act* Receivesgnlcase I Receivebufcase Locexprl Sgnlreceivealt + Act *I Sgnlid Id* Act* Locexpr Bufreceivealt+ Act Locexpr id Act* Assign I Call I Birproccall I Exit I Return I Result I Goto I Assert I EMPTY 1 Start I STOP I D

30、elay I Continue I Send I Cause Singleassign I Multipleassign Asgn I Update Locexpr Value Locexpr Updop Value Pwsdifop I Armaddop 1 Armmultop I OR I XOR 1 AND Locexpr + Value (Pid I Valexpr) Bircall Lid Result Value Staticlocexpr Lid Valexpr Startexpr Locexprl Locexpr s-priority: Valexprl Locexpr Sen

31、dsgnl I Sendbuf Sgniid Value s-receiver: I Valexprl s-priorit y: Valexprl Locexpr Value s-priority: Valexpr Eid (Value I Staticlocexpr) Value I Locexpr Valexpr I UNDEF Valexpr (OR I XORII Oper 1 Oper 1 ANO Oper2 (Oper2 Op31 Oper3 Relop I IN I Pwsinclop Eil 1 NE I GT I GE I LT I LE LE I GE 1 LT I GT

32、Oper3 Op41 Oper4 Arrnaddop I CONC I Pwsdifop ADD I SUB SUB Oper4 Arrnrnultopl Oper5 MU1 I DIV I MOD I REM Mop Oper6 MINUS I NOT I Valexpr Primitive I Valexpr Deloc I Valuename I Literal I Tuple 1 Valstringelern I Valsubstring 1 I I Valsubarray I Valarrayslice I Valstructfield I Bircall 1 Startexpr I

33、 Receiveexpr I THIS Valstringslice I Valarra yele, Ref I Valconv I Valproccall Locexpr Id lntlit I Boollit I Setlit I NULL BOOL Sid Pid QUOT * BOOL NO Proclit I Chrstrlit I Bitstrlit STD-ITU-T HDBK VOL II CFD-ENGL 19B2 6 YB62591 0682778 408 M Part IV.116 Prg, and Program Transformation 27 Tuple 28 W

34、eaktuple 29 Pwstuple 30 Arra ytuple 3 7 Unlabarra ytuple 32 Labarra ytuple 33 Structtuple 34 Unlabstructtuple 35 Labstructtuple 36 Valstringelem 3 7 Valsubstring 38 Slice 40 Valstringslice 4 1 Valarra yelem 42 Valsubarra y 43 Valarra yslice 44 Valstructfield 45 Ref 46 Valconv 4 7 Valproccall 48 Birc

35、all 39 up 49 Num 50 Pred 51 Succ 52 Abs 53 Addr 54 Card 55 Max 56 Min 57 Size 58 Upper 59 Getstack 60 Getref 6 1 Getarra ysliceref 62 Getstringsliceref 63 Ge tparms tructre f 64 Startexpr 65 Receiveexpr - ,. - - - 1 .I .5.2. Location Expressions 1 Locexpr 2 Staticlocexpr 3 Accessname 4 Derefboundref

36、 5 Dereffreeref 6 Locstringelem 7 Locsubstring 8 Locarra yelem 9 Locsubarra y 10 Locstructfield 1 1 Locproccall 12 Locconv 13 D ynlocexpr 14 Locstringslice 7 5 Locarra yslice 16 Derefrow 1.1.6. identifiers ,. ,. - Modeid Weaktuple Pwstuple 1 Arra ytuple I Structtuple (Valexpr 1 Rng/* Unlabarra ytupl

37、e I Labarra ytuple Value + (ICaseIablist 1 ELSE I IRR) Unlabstructtuple 1 Labstructtuple Value + (Fid + Value/ + Valexpr Valexpr Valexpr Slice s-lower: Valexpr s-upper: Valexpr Valexpr Rng Valexpr Valexpr + Valexpr Slice Valexpr Rng Valexpr Fid Locexpr Modeid Valexpr Call Num 1 Pred 1 Succ 1 Abs 1 A

38、ddr 1 Card 1 Max 1 Min I Size I Upper I Getstack Valexpr Valexpr Valexpr Valexpr Locexpr Valexpr Valexpr Valexpr Modeid 1 Staticlocexpr Valexpr Getref 1 Getarra ysliceref 1 Getstringsliceref I Getparmstructref Modeid Modeid Valexpr Modeid Valexpr Modeid Valexpr + Pid (Staticlocexpr 1 Value/ * Locexp

39、r Value/+ Rng I UP Staticlocexpr 1 D ynlocexpr Accessname I Derefboundref 1 Dereffreeref 1 Locstringelem 1 Locsubstring Locarrayelern I Locsubarra y 1 Locstructfield I Locproccall I Locconv Id Valexpr Modeid Valexpr Modeid Locexpr Valexpr Locexpr Slice Locexpr Valexpr + Locexpr Slice Locexpr Fid Cal

40、l Modeid Staticlocexpr Locstringslice I Locarra yslice I Derefrow Locexpr Rng Locexpr Rng Valexpr Modid, Regid, Pid, Modeid, Sid, Fid, Lid, Eid, Sgnlid, Registerid = Id Id C TOKEN 1.2. Program Transformation STDSITU-T HDBK VOL II CFD-ENGL 1982 m 4862591 Ob82777 344 SS Program Transformation Part IV.

41、 117 1.2.1. transf-Prg, trans f-Prg, prg,) = ccases prgoirl : (mk-Moduleacb (olid,mod,ohdl,l -+ flet lid = if olid = nil then getid0 else olid, mod, = transf-Module, (mod,) , ohdl, = transf-ohdl,(ohdI,l in mk-Moduleact, Ilid,mod, ,ohdl,ll , T + flet mk-Def, /id,region,) = transf-Region,(prg,rll in m

42、k-Regiondef, (id,region,l) I 1 I i I len prg, type: Prg, -+ Prg, 1.2.2. transf-Al, transf-Ah (ah) = conc I 1 I i I len al, type: Act; -+ Act; 1.2.3. transf-returnact, trans f-returnacb (m k-A ct, (olid, m k-Return, (oresultd, ohdld) = /oresuit, # nil T + I type: Ac$ -t Act; + , 1 .2.4. transf -Act,

43、trans f-Act, (mk-Acto (olid,stmt, ohdldl = flet olid, = if olido = nil A is-Module,(stmtd then getid0 else alid, stmt, = transf-Stmt,(stmt,) , ohdl, = transf-ohdl,(ohdl,) in mk-Act, lolid, ,stmt,ohdl,)l type: Act, + Act, 1.2.5. transf-ohdl, transf-ohdl,(ohd/ol = cases ohdh : Imk-Hdh (onalth, aal,) o

44、al, = if -+ flet onaltm, = transf-Onalt/,/onaltlo) , oah = nil then nil else transf-Al,oal,l in mk-Hdl, (onaltrn,oal,)l , T -* nil ) type: IHdhI -+ iHd1, 1 1.2.5.1. transf-Onaltl, trans f- Onalth (onaltl,) = if onalth = then i 1 else flet (eidl,al,) = hd onaltl, in STD-ITU-T HDBK VOL II CFD-ENGL I19

45、82 LiBb259L Ob82780 Ob6 9 Part IV.1/8 Prg, and Program Transformation let onaltrn, = transf-Onaltl, ftl onaltl,) in if len eidl = card elems eidl A elems eidl fl dom onaltm, = then onaltrn, U eid -+ transf-Al,(ale,) else exit type: Iterlist, + (Id ,+ Iter,) 1.2.1 1. transf-Module, trans f-Module, (m

46、k-Module, (dvprl, al,) = flet (visib, ,ddl,) = transf-dvprI,(dvprl,) , al, = transf-Al,(al,) in mk-Module, (visib, ddl, al,) type: Module, + Module, 1.2.1 1.1. transf-dvprl, trans f-dvprl, (dvprl,) = flet dsl, = , grstmtl, = , sstmtl, = in grant, = trans f- Grantstmtlist, (grstm tloi , seize, = tran

47、s f-Seizestmtlist, (sstmtl,) in let ddl, = trans f- Da tas tm tlis to (dsi,) , (mk- Visib, (grant, ,seize , I, ddl, i) type: (Datastmt, 1 Visibstmt, I Region,) * + (Visib, Datadef,) 1.2.1 2. transf-Datastrntlist, trans f-Datastmtlist, (dsl,) = conc , m k- Region, (, , ) T + , -+ transf-Defstmt,/ds/,

48、/I/) I 1 I i I len dsl, type: (Datastmh 1 Region,) -+ Datadef, 1.2.13. transf-Dcllist, trans f-Dcllist, fdcll,) = conc + mk-Lifeinit, (transf- Value,(val,ll , if then else exit I, mk-Lociddcd id 1.2.17.1. transf-ores, trans f-ores, ores,l = cases ores, : frnk-Res,/me,oloc, ) -+ mk-Resultspec, (trans

49、f-Modeexpr,(me,),olocI , T -+ nil ) type: Res, + Resu/tspec, I 1.2.17.2. transf-Procatto transf-Procatb (mk-Procatt, (gen, orecl) = cases gen,: (GENERAL + mk-General, (orec) , SIMPLE -+ mk-Simple, lored , INLINE -+ if orec = nil then INLINE else exit, T -* getdefaultprocatt 1) type: Procatt, + Procatt, 1.2.17.3. transf-Pbody, transf-Pbody,(mk-Pbody,lds,aeldI = (let (,ddl,) = transf-dvprI,(