操作语义

操 作 语 义 LA 汇编语言 LE 表达式语言 L0 无声明简单语言 L1 ＝ L0 ＋ Read ＋ Write L2 ＝ Ls ＋ VDec ＋ Block L3 ＝ L2 ＋ PDec ＋ Fdec PL 并发语言软件形式化 程序语言语义形式化（形式语义学） 形式语义学 (1)操作语义学 (2)指称语义学 (3)公理语义学 (4)代数语义学 操作语义方法 (1)抽象机方法 (2)归约式方法 (3)解释器方法 操作语义方法特点：形式地描述程序的执行（操作）过程 抽象级方法：针对给定语言构造抽象机 抽象机：(1)机器状态：MS=Comm﹡×SEnv×DEnv   终止状态初始状态(2)状态转换规则：MS→MS■汇编语言语义的形式化描述（操作语义）语言：L: ADDRx R ε(f) = proc(Params,B,εp)Params = vdec(x1, t1):……:vdec(xn, tn)|RETURN:(return :CL△CCL , ε△ρ,σ△β) → (CCL,ε,σ)MS:|BLOCK:(block(VDL,SL): CLL,ε,σ)→(VDL:SL:ENDB:CCL,ε△[],σ△[])|ENDB:(ENDB:CLL,ε△ρ,σ△β) → (CLL, ε,σ)σεCCL交交叉叉序序列列例：设有 A = [ a1, a2] , B = [b1, b2] , 则下列序列称为 A 和 B 的交叉序列：a1, a2 , b1, b2 b1, b2 , a1, a2 a1, b1 , a2, b2 a1, b1 , b2 , a2……………… ………………形式定义：A || B 表示 A 和 B 的交叉序列？集 1） A || [ ] ≡ {A}2) [ ] || B ≡ {B} 3) (a: A’) || B ≡ a ● ( A’ || B) 4) A || ( b: B’)≡ b ● (A || B’)其中 d ● { α1, α2,…，αn} ≡ {d: α1, d:α2,…，d:αn }状态式描述：非确定性 R1： (α , A || [ ] ) →α AR2: ( α , [ ] || B ) →α B R3: ( α , ( a: A’) || B ) → ( α :: a, A’ || B) R4: (α , A || ( b: B’) ) →( α :: b, A || B’) 初始状态： ( [ ] , A || B )例：A ＝ [a1, a2] , B = [ b1, b2] 初始状态： ( [ ] , A || B )( [ ] , A || B)①( [ ] , (a1: [a2] ) || B )( [a1] , a2: [ ] || B)( [a1, a2] , [ ] || B)[a1, a2, b1, b2]②( [ ] , A || b1:b2: [ ] )( [b1] , A || b2: [ ] )( [ b1 , b2] , A || [ ] )[ b1, b2, a1, a2]③( [ ], a1:a2:[ ] || b1:b2:[ ] )( [a1] , a2: [ ] || b1: b2: [ ] )( [a1, b1] , a2: [ ] || b2: [ ] )( [a1, b1, b2] , a2: [ ] || [ ] )[a1, b1, b2, a2] 归约式： ZERO： [ ] || [ ] → nil(两边空) LEFT： a: A || B → a: ( A || B)(左不空)RIGHT: A || b : B → b: ( A || B)(右不空)无通信并行进程的动作序列无通信并行进程的动作序列 （多进程）（多进程）□□ 语法定义：语法定义： P ：：＝Ω | a. P | P || Q □□ 结构等价：结构等价：R3选择不确定R3R2R4R4R1R3R4R4R1P || Ω≡P P || Q ≡ Q || P ( P || Q ) || R ≡ P || (Q || R) □□ 不确性：不确性： 并发性含有不确性，而归约性本身具有不确定，因此，归约式方法适合于描述并 发性。

□□ 执行轨迹：执行轨迹： 每次并发进程的执行对应一个动作序列，称之为进程的一个轨迹我们要描述产 生轨迹的方法 □□ 归约式描述：归约式描述： ZERO： Ω →nil(与 Ω 等价) PARA：a.P || Q → a:( P || Q)(与 Ω 不等价) INFER： P ≡ Q , Q → β P → β[例] P ＝ [ a1, a2 ] , Q = [ b1] , R = [c1, c2, c3]a1. a2. Ω || b1. Ω || c1.c2. Ω→a1:( a2. Ω || b1. Ω || c1.c2. Ω ) →a2: b1: (a2. Ω || Ω || c1.c2. Ω ) →a2: b1: c1: ( a2. Ω || Ω || c2. Ω) →a2: b1: c1: c2: ( a2. Ω || Ω || Ω) →a2: b1: c1: c2: a2: (Ω || Ω || Ω ) →a2: b1: c1: c2: a2: nil通信的并发进程通信的并发进程□□ 语法：语法： P ::= Ω | α . P | P || Q α ::= a | c! n | c?xa ……非通信动作c!n ……把数发到通道 c，并等待c?x……从通道取一个数，并送给 x 其中，c!n 和 c?x 是同步动作，通信后各自并行执行。

□□ 归约式：归约式： ZERO：Ω → nil ACTION： a . P || Q → a: ( P || Q )COMM: c!n. P || c?x.Q → (x , n): ( P || Q) INFER:P ≡ Q, Q → β P → β( 推理规则 )P = a1. a2. c!n . c?x . a3. Ω Q = b1. c?y . b2. c!e . b3. ΩP || Q1 → a1: (a2 . c!n . c?x . a3.Ω || b1. c?y . b2. c!e . b3. Ω ) → a1: a2: ( c!n .c?x , a3.Ω || b1. c?y . b2. c!e . b3. Ω)→ a1: a2: b1: (c!n .c?x , a3.Ω || c?y . b2. c!e . b3. Ω)→ a1: a2: b1: (y,n): ( c?x , a3. Ω || b2. c!e . b3. Ω )→ a1: a2: b1: (y,n): b2: (c?x , a3. Ω || c!e . b3. Ω )→ a1: a2: b1: (y,n): b2: (x,e): ( a3. Ω || b3. Ω )→ a1: a2: b1: (y,n): b2: (x,e): a3: ( Ω || b3. Ω )→ a1: a2: b1: (y,n): b2: (x,e): a3: b3: ( Ω || Ω )→ a1: a2: b1: (y,n): b2: (x,e): a3: b4: nil■并发模型语言 PML（通信）□ 语言定义 Prog::=PP::=Ω |P1 || P2|S﹒P S::=ass(x,E) |if(E,S1,S2) |do(E,S) |send(c,E) |receive(c,y) □并发动作基本单位 (1)E 计算接赋值 (2)E 计算接判断 (3)E 计算接同步 □抽象机结构MS= set of (P)×DEnv例DEnv= Var→Val 用到下面记法： a⊳S = {a}∪S, 并且 aS.□MS 转换规则ASS:, ', '.,MSPMSPxEass if【E】σ= ttaif【E】σ= ffaDO: if【E】σ= ffaif【E】σ= ttaPARA: ',|| ',||', ',  QPQPPP aaCOMM: aINFER: ',,',,,  RPRP aa□ 结构等价定理 (1)结构等价：（≡）P || Ω ≡ P, P || Q ≡ Q || P, (P || Q) || R ≡P || (Q || R) (2)结构等价定理： 设（Pi1,Pi2,…，Pin）是（P1,P2,…，Pn）的任一置换，则Pi1 || Pi2 || … || Pin ≡ P1 || P2 || … || Pin。