《代数语义学ppt课件》由会员分享，可在线阅读，更多相关《代数语义学ppt课件（39页珍藏版）》请在金锄头文库上搜索。
1、代代数数语语义义学学理论基础理论基础函数式描述方法函数式描述方法程序设计语言程序设计语言形式语义形式语义指称语义学指称语义学操作语义学操作语义学公公理理语语义义学学代数代数功功能能执执行行逻辑逻辑 关系关系模型模型离散数学离散数学程序设计语言程序设计语言形式语义形式语义编编译译原原理理程序设计语言程序设计语言理理论论基基础础语义形式化语义形式化语法形式化语法形式化软件开发方法软件开发方法程序设计语言程序设计语言形式语义形式语义程程序序设设计计方方法法程序设计语言理解程序设计语言理解抽抽象象能能力力Formal MethodFormal SpecificationFormal Verificat
2、ion第第九章九章 指称语义的原理与应用指称语义的原理与应用指称语义学是Christopher Strachey和Dana Scott在1970年提出的。指称语义学的一个显著特征是: 程序中的每一个短语(表达式、命令、声明等)都有其意义。它是与语言的语法结构平行的。每个短语的语义函数就是短语的指称意义。其现代名称为指称语义学。 16.1 16.1 指称语义原理指称语义原理从数学的观点，一个程序可以看作是从输入到输出的映射P(I)O，即输入域(domain)上的值，经过程序P变为输出域(range)的值。pd (pP，dD)。语义域D中的数学实体d, 或以辅助函数表达的复杂数学实体d，称为该短语
3、的数学指称物，即短语在语义函数下的指称语义。指称语义描述的是语义函数映射的后果，不反映如何映射的过程，更没有过程的时间性。而程序设计语言的时间性只能反映到值所表达的状态上。 语义函数和辅助函数语义函数和辅助函数描述二进制数的语义二进制数 Numeral := 0 (16.1-a) 1 (16.1-b) Numeral 0 (16.1-c) Numeral 1 (16.1-d)我们给出求值的语义函数:将Numeral集合中的对象映射为自然数: valuation: NumeralNatural (16.2)按语法的产生式，我们给出以下语义函数: valuation 0= 0 valuation
4、1 = 1 valuation N0 = 2 valuation N NNumeral valuation N1 = 2 valuation N+ 1 valuation1101 = 2 valuatioin 110+ 1 = 2 (2 valuation 11) + 1 = 2 (2 (2 valuation 1+ 1) + 1 = 2 (2 (2 1 + 1) + 1 = 13计算器命令的语义描述 计算器命令的抽象语法： Com := Expr= (16.3) Expr := Num (16.4-a) Expr + Expr (16.4-b) Expr - Exp (16.4-c) Exp
5、r * Expr (16.4-d) Num := DigitNum Digit (16.5)Digit := 0123456789 (16.6) execute : Com lnteger evaluate: Expr lnteger sum : Integer Integer Integer difference : Integer Integer Integer product : Integer Integer Integer 以下定义每个短语的语义函数: execute C = execute E= = evaluate E 其中CCom，EExpr。 evaluate N= valu
6、ation N (NNum) evaluate E1 + E2 = sum (evaluate E1，evaluate E2) evaluate E1 - E2 = difference (evaluate E1，evaluateE2) evaluate E1 * E2 = product (evaluate E1, evaluate E2)再定义Num的两个表达式: valuation D = D (DDigit,DNatural) valuation ND= 10 valuation N+ D execute 40-3*9= =evaluate 40-3*9 =product (evalu
7、ate40-3，evaluate9) =product (difference (evaluate 40，evaluate 3)， evaluate9) =product (difference (valuation40，valuation3)， valuation9) =product (difference (40，3)，9) =33316.1.2 16.1.2 语义域语义域 基本域基本域 Character / lnteger / Natural / Truth-Value / Unit 用户可定义枚举域,以及以基本域构造的复合域。 笛卡儿积域笛卡儿积域 DD 元素为对偶(x，x)其中x
8、D，xD。 D1D2Dn元素为n元组(x1，x2，xn)，其中xiDi。 不相交的联合域不相交的联合域 D+D 元素为对偶(left x，right x)其中xD，xD。 shape=rectangle( RealReal ) + circle Real + point 函数域函数域 DD 例如lntegerEven。 f(v) 偏函数，vV f() 严格的偏函数 f()v 非严格函数 偏函数域上元素间具有偏序关系，偏序关系的性质是: D域若具偏序性质，它必须包含唯一的底元素，记为，且d，d为D中任一元素。通俗解释是d得到的定义比多。是不对应任何值的值。 若 x，y D，xy此二元素具有偏序关
9、系，即y得到的定义比x多。这一般就复合元素而言，即x中包含的比y多。 若x，y，zD，则偏序关系必须是: 1 自反的，即有xx; 2 反对称的，即若xy，yx，必然有x=y; 3 传递的，即若xy，yz，必然有xz。 序列域序列域 序列域D*中的元素是零个或多个选自域D中的元素有限序列，或为nil元素，或为xs的序列 nil 一般写法是“ ” anil 一般写法是“a” Busy nil 一般写法是“Busy”16.1.3 16.1.3 命令式语言的特殊域命令式语言的特殊域 存储域Store = Location ( stored Storable + undefined + unused)
10、(16.15)empty-store : Store (16.16) allocate : Store Store Location (16.17) deallocate : Store Location Store (16.18) update : Store Location StorableStore (16.19) fetch : Store LocationStorable (16.20)empty_store = loc.unused allocate sto = let loc = any_unused_location (sto) in (sto loc undefined，l
11、oc) deallocate (sto，loc) = sto loc unused update (sto，loc，stble) = sto locstored stble fetch (sto，loc) = let stored_value (stored stble) = stble stored_value (undefined) = fail stored_value (unused) = fail in stored-value (sto(loc) 环境域Environ = ldentifier(bound Bindable + unbound) empty-environ : En
12、viron bind : ldentifierBindable Environ overlay : EnvironEnviron Environ find : EnvironldentifierBindableenpty-environ = I. unbound bind (I，bdble) = I. if I=I then bound bdble else unbound overlay (env，env) = I. if env (I)/=unbound then env (I) else env (I) find (env，I) = let bound_value (bound bdbl
13、e) = bdble bound_value (unbound) = in bound_value (env (I) 16.2 16.2 指称语义示例指称语义示例 过程式小语言过程式小语言 IMPIMP抽象语法是: Command := Skip ldentifier := Expression let Declaration in Command Command; Command if Expression then Command else Command while Expression do Command Expression := Numeral false true Ldenti
14、fier Expression + Expression Expression Expression not Expression . Declaration := const ldentifier = Expression var ldentifier : Type_denoter Type_denoter := bool int IMP IMP的语义域、语义函数和辅助函数的语义域、语义函数和辅助函数 Value = truth_value Truth_Value + integer lnteger Storable = Value Bindable = value Value + vari
15、able Location execute: Command (EnvironStoreStore) executeC env sto = sto evaluate: Expression (EnvironStore Value) evaluate E env sto= elaborate: Declaration (EnvironStore Environstore) elaborate D env sto = 辅助函数有如前所述的empty-environ，find，overlay，bind，empty-store，allocate，deallocate，update，fetch。以及su
16、m，less，not等辅助函数。此外，再增加一个取值函数: coerce: StoreBindableValue coerce (sto，find (env，I) = val = fetch (sto，loc) IMP IMP的指称语义的指称语义 execute Skip env sto = sto execute I:= E env sto = let val = evaluate E env sto in let variable loc = find (env，I) in update(sto，loc，val) execute let D in C env sto = let (env，
17、sto) = elaborate D env sto in execute C (overlay (env，env) stoexecute C1; C2 env sto = execute C2 env (execute C1 env sto)execute if E then C1 else C2 env sto = if evaluate E env sto = truth_value true then execute C1 env sto else execute C2 env stoexecute while E do C= let execute_while env sto = i
18、f evaluate E env sto = truth_value true then execute_while env (execute C env sto) else sto in execute_whileelaborate const I = E env sto = let val = evaluate E env sto in (bind (I，value val)，sto)elaborate var I:T env sto = let (sto，loc)= allocate sto in (bind (I，variable loc)，sto)16.3 16.3 程序抽象的语义描
19、述程序抽象的语义描述 函数抽象函数抽象 Function = ArgumentValue Function = ArgumentStoreValue bind_parameter: Formal_Parameter(ArgumentEnviron) give_argument : Actual_Parameter(EnvironArgument) 扩充扩充IMPIMP语法语法 Command := Identifier (Actual_Parametor) Expression := Identifier (Actual_Parmenter) Declaration := func Ident
20、ifier (Formal_Parameter) is Expression proc ldentifier (Formal_paramenter) is Command Formal_Parameter := const Identifier: Type_Denoter Actual_parameter := Expression Argument = Value Bindable = value Value + variable Location + function Function 写写IMPIMP函数的指称语义函数的指称语义 bind-parameter I:T arg = bind
21、 (I，arg) give-argument E env = evaluate E env 函数调用的语义等式如下: evaluate I(AP) env = let function func = find (env，I) in let arg = give_argument AP env in func arg elaborate fun I(FP) is E env = let func arg = let parenv = bind_parameter FP arg in evaluate E (overlay (parenv，env ) in (bind (I，function fu
22、nc) 过程抽象过程抽象 Procedure = ArgumentStoreStore Argument = Value Bindable = value Value + variable Location+functionFunction +procedure Procedure execute I(AP) env sto= let procedure proc = find (env，I) in let arg = give_argument AP env sto in proc arg sto elaborate proc I(FP) is C env sto = let proc ar
23、g sto = let parent = bind-parameter FP arg in execute C (overlay (parenv env) sto in (bind (I，procedure proc)，sto) 参数机制的语义描述 - 常量和变量参数 先细化参数定义语法 Formal-Parameter := const Identifier: Type_denoter var Identifier : Type_denoter Actual-P arameter := Expression var Identifierbind_parameter : Formal_para
24、meter(ArgumentEnviron)give_parameter : Actural_Parameter(EnvironStoreArgument)形参的语义等式是: bind_parameter const I:T (value val) = bind (I，value val) bind_parameter var I:T (variable loc)= bind(I，variable loc)实参的语义等式是: give_argument E env sto = value (evaluate E env sto) give_argument var I env sto = le
25、t variable loc = find (env，I) in variable loc - 复制参数机制 Formal_Parmeter := value Identifier: Type_denoter result Identifier : Type_denoter Actual_Parameter := Expression var Identifier copy_in: Formal_Parameter(ArgumentStoreEnvironStore) copy_in value I:T (value val) sto = let (sto，local) = allocate
26、sto in (bind (I，variable local)，update (sto，local，val) copy-in result I:T (variable loc) sto= let (sto，local)= allocate sto in (bind (I，variable local)，sto) copy_out: Formal_Parameter(Environ ArgumentStoreStore)copy_out value I:T env (vlaue val) sto = sto copy_out result I:T env (variable loc) sto =
27、 let variable local = find (env，I) in update (sto，loc，fetch (sto，local)过程声明的语义等式作以下修改: elaborateproc (FP) is C env sto= let proc arg sto= let (parenv，sto) copy_in FP arg sto in let sto = execute C (overlay (parenv，env ) sto in copy_out FP parenv arg sto in (bind (I，procedure proc)，sto)- 多参数Function
28、= Argument*StoreValue Procedure = Argument* StoreStorebind_parameter : Formal_Parameter_List(Argument* Environ) give_argument:Acrual_Parameter_List(Environ Store Argament*) - 递归抽象递归函数声明的语义等式如下: elaborate fun I (FP) is E env= let func arg = let env=overlay (bind (I，function func)，env) in let parenv =
29、 bind-parameter FP arg in evaluate E (overlay (parenv，env) in bind (I，function func)16.416.4 复合类型复合类型最简单的复合变量的语义描述暂不考虑函数和过程抽象，只增加最简单的复合量对偶(A:T1,B:T2).先扩充抽象语法：Command := V_name := Expression Expression := V_name (Expression,Expression) V-name := Identifier fst V_name 相当于V(1) snd V_name 相当于V(2) Type_d
30、enoter := bool int |(Type_denoter，Type_denoter) 对偶值本身是一个域:Pair_Value = ValueValue 对偶变量的域：Pair_Variable = VariableVariable Value = truth_value Truth_Value + integer Integer + pair_value Pair_ValueStorable = truth_value Truth_Value + integer IntegerVariable = simple_variable Location + pair_variable P
31、air_Variable辅助函数：辅助函数：fetch_variable: StoreVariable Value update_variable: StoreVariableValue Store fetch_variable(sto，simple_variable loc) = fetch(sto，loc) fetch_variable(sto，pair_variable (var1，var2) = pair_value(fetch_variable(sto，var1),fetch-variable (sto，var2) update_variable(sto,simple_variabl
32、e loc，stble ) = update (sto,loc,stble) update_variable (sto,pair_variable (var1,var2), pair_value (val1,val2)= let sto=update_variable (sto，var1,val1) in update_variable (sto,var2,val2) 增加识别(identify)和分配变量存储(allocate_variable)的语义函数：identify: V-name (Environ Value_or_Variable)Value_or_Variable = valu
33、e Value + variable Variable identifyI env = find(env，I) identifyfst V env = let first (value (pair_value (val1，val2) = value val1 first (variable (pair_variable (var1，var2) = variable var1 in first (identify V env)/辅助函数first将对偶值或对偶变量映射为它的第一子域。赋值语句语义等式：execute V:= E env sto = let val = evaluate E env
34、 sto in let variable var = identify V env in update_variable (sto，var，val)evaluate V env sto= coerce (sto，identify V env)coerce: Store Value_or_VariableValue coerce (sto，value val ) = val coerce (sto，variable var) = fetch_variable (sto，var) allocate_variable: Type_denoterAllocatorAllocator = Store S
35、toreVariable 例：为类型指明符bool分配存储的语义是: allocate_variable bool sto= let (sto，loc) = allocate sto in (sto，simple_variable loc)为对偶指明符分配存储的语义是: allocate_variable(T1，T2) sto= let (sto，var1) = allocate_variable T1 sto in let (sto，var2) = allocate_variable T2 sto in (sto，pair_variable (var1，var2)变量声明的语义: elabo
36、ratevar I:T env sto= let (sto，var) = allocate_variable T sto in (bind(I，var)，sto)数组变量的语义描述(参考教材)16.5 16.5 程序失败的语义描述程序失败的语义描述sum: Integer Integer Integer sum (int1，int2) = if abs(int1+int2) =maxint then int1+int2 else sum (，int2)= sum (int1，) = evaluate E1 + E2 env sto = let integer int1 = evaluate E
37、1 env sto in let integer int2 = evaluete E2 env sto in integer (sum (int1，int2)16.6 16.6 指称语义应用指称语义应用 指称语义用于设计语言指称语义用于设计语言 为一个程序设计语言写指称语义的步骤是:分析(所设计的)程序设计语言的规格说明写出抽象语法。定义该语言的指称域，并为这些域定义洽当的辅助函数以模型值上的操作。 建立语义函数。为抽象语法中的每个短语(即短语类)指定一个域(语义函数的 输入域)，定义输入域到其指称域的语义函数。为每一短语类写出语义等式。16.6.2 16.6.2 指称语义用于程序性质研究指称
38、语义用于程序性质研究 上下文约束的静态描述在程序设计语言的文法产生的所有句子之中只有一部分是良定义的。语法往往不能给出明确的表示，要依靠上下文约束。用指称语义的方法描述程序设计语言的上下文约束要建立类型环境的概念。语言中各类型之总称即为Type域。例如，在前述IMP语言中类型域是:Type=truth_type + integer_type + var_type + error_type Type_Environ = Identifier(bound Type + unbound) equivalent: TypeTypeTruth_Value 可测试两种类型是否等价。 constrain:
39、Command(Type_EnvironTruth_Value) 检查命令在类型环境中是否遵从约束，即是否良定义的。 typify: Expression(Type_EnvironValue_Type) 验明表达式的类型，即在类型环境中的具体类型。 declare : Declaration(Type_EnvironTruth_ValueType_Environ) 在类型环境中给出声明是良定义的真值, 以及所产生的类型束定。 type_denoted_by: Type_DenoterValue_Type产生类型指明符的真实类型。类型环境域有以下辅助函数: empty_environ : Typ
40、e_Environ bind : ldentifier Type Type_Environ overlay: Type_EnvironType_EnvironType_Environ find: Type_EnvironIdentifierType 程序推理C; ship C。要证明相等，即指出两端指称一样即可: execute C; skip env sto = execate skip env (execute C env sto) = execute C env sto将域的各等式也转成ML的datatype定义:typetype Location = int;datatypedatat
41、ype Value= truthvalue ofof bool integer ofof int;typetype Stroeable = Value;datatypedatatype Bindable = value ofof Value variable of of Location;再写出具体函数定义:funfun execute (skip) env sto = sto execute (IbceomesE(I，E) env sto = let let valval val = evaluate E env sto in in let let valval variable loc =
42、 find (env，I) in in update (sto，loc，val) end end end end execute (letDinC (D，C) env sto = let let valval (env，sto) = elaborate D env sto in execute C (overlay (env，env) sto end end 16.6.3 16.6.3 语义原型语义原型先将抽象语法改写为ML的datatype 定义: type type Identifier = string andand Num eral = string; datatypedatatype
43、 Command = skip IbecomesE of of Identifier * Expression letDinC ofof Declaraton * Command CsemicolonC ofof Command * Command ifEthenCelseC ofof Expressiion * Command * Command whileEdoC of Expression * Command andand Expression = num of of Numeral flase true ide of of Identifier EplusE ofof Expressi
44、on * Expression and and Declaration= constIisE of of Ldentifier * Expression varIcolonT ofof Ldentifier* Typerdenoter and and Typedenoter= bool int将域的各等式也转成ML的datatype定义:typetype Location = int;datatypedatatype Value= truthvalue ofof bool integer ofof int;typetype Stroeable = Value;datatypedatatype
45、Bindable = value ofof Value variable of of Location;再写出具体函数定义:funfun execute (skip) env sto = stoexecute (IbceomesE(I，E) env sto = let let valval val = evaluate E env sto in in let let valval variable loc = find (env，I) in in update (sto，loc，val) end end end end execute (letDinC (D，C) env sto = let
46、let valval (env，sto) = elaborate D env sto in execute C (overlay (env，env) sto end end execute (CsemicolonC (C1，C2) env sto = execute C2 env (execate C1 env sto) execute (if E then C else C (E，C1，C2) env sto = if if valuate E env sto = truthvalue true thenthen execute C1 env sto elseelse execute C2
47、env sto execute (whileEdoC (E，C)= let funlet fun executewhile env sto = ifif evaluate E env sto = truthvalue true then then executewhile env (execute C env sto ) else else sto in in executewhile end end andand evaluate (num N) env sto = integer (valuation N)evaluate (false) env sto = truthvalue fals
48、eevaluate (true) env sto = truthvalue trueevaluate (ide I) env sto = coerce (sto，find (env，I )evaluate (EplusE( E1，E2 ) env sto = let let valval integer int1 = evaluate E1 env sto in let let valval integer int2 = evaluate E2 env sto in in integer (sum ( int1，int2 ) ) endend end end.and and elaborate
49、 (constIisE ( I，E ) env sto= let let valval val=evaluate E env sto in (bind (I，value val)，sto) end end elaborate (varIcolonT( I，T ) env sto= let let valval (sto，loc)=allocate sto inin ( bind ( I，variable loc )，sto) end end and valuation (N) = integer (stringtoint N)以上按IMP 抽象语法套写语义函数execute, evaluate，elaborate. 还要把辅助函数改写为ML:fun fun coerce ( sto，value val)= val coerce ( sto，vatiable loc ) = fetch ( sto，loc )设置初始条件运行ML程序有了以上定义，即可运行抽象语法树的ML解释器，例如:valval env0=.; /初始环境valval sto0=.; /初始存储valval prog=.; /一条IMP命令的抽象语法树execute prog env0 sto0;
