《代数语义学》ppt课件

《《代数语义学》ppt课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、代数语义学理论基础函数式描述方法程序设计语言形式语义指称语义学操作语义学公理语义学代数功能执行逻辑关系模型离散数学程序设计语言形式语义编译原理程序设计语言理论基础语义形式化语法形式化软件开发方法程序设计语言形式语义程序设计方法程序设计语言理解抽象能力FormalMethodFormalSpecificationFormalVerification第九章指称语义的原理与应用指称语义学是ChristopherStrachey和DanaScott在1970年提出的。指称语义学的一个显著特征是:程序中的每一

2、个短语(表达式、命令、声明等)都有其意义。它是与语言的语法结构平行的。每个短语的语义函数就是短语的指称意义。其现代名称为指称语义学。16.1指称语义原理从数学的观点，一个程序可以看作是从输入到输出的映射P(I)→O，即输入域(domain)上的值，经过程序P变为输出域(range)的值。φ〖p〗→d(p∈P，d∈D)。语义域D中的数学实体d,或以辅助函数表达的复杂数学实体d'，称为该短语的数学指称物，即短语在语义函数下的指称语义。指称语义描述的是语义函数映射的后果，不反映如何映射的过程，更没有过程的

3、时间性。而程序设计语言的时间性只能反映到值所表达的状态上。●语义函数和辅助函数描述二进制数的语义二进制数Numeral::=0(16.1-a)｜1(16.1-b)｜Numeral0(16.1-c)｜Numeral1(16.1-d)我们给出求值的语义函数:将Numeral集合中的对象映射为自然数:valuation:Numeral→Natural(16.2)按语法的产生式，我们给出以下语义函数:valuation〖0〗=0valuation〖1〗=1valuation〖N0〗=2×valuation〖

4、N〗∥N∈Numeralvaluation〖N1〗=2×valuation〖N〗+1valuation〖1101〗=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)｜Expr*Expr(16.4-

5、d)Num::=Digit｜NumDigit(16.5)Digit::=0｜1｜2｜3｜4｜5｜6｜7｜8｜9(16.6)execute:Com→lntegerevaluate:Expr→lntegersum:Integer×Integer→Integerdifference:Integer×Integer→Integerproduct:Integer×Integer→Integer以下定义每个短语的语义函数:execute〖C〗=execute〖E=〗=evaluate〖E〗其中C∈Com，E∈E

6、xpr。evaluate〖N〗=valuation〖N〗(N∈Num)evaluate〖E1+E2〗=sum(evaluate〖E1〗，evaluate〖E2〗)evaluate〖E1-E2〗=difference(evaluate〖E1〗，evaluate〖E2〗)evaluate〖E1*E2〗=product(evaluate〖E1〗,evaluate〖E2〗)再定义Num的两个表达式:valuation〖D〗=D’(D∈Digit,D’∈Natural)valuation〖ND〗=10×val

7、uation〖N〗+D’execute〖40-3*9=〗=evaluate〖40-3*9〗=product(evaluate〖40-3〗，evaluate〖9〗)=product(difference(evaluate〖40〗，evaluate〖3〗)，evaluate〖9〗)=product(difference(valuation〖40〗，valuation〖3〗)，valuation〖9〗)=product(difference(40，3)，9)=33316.1.2语义域·基本域Charact

8、er/lnteger/Natural/Truth-Value/Unit用户可定义枚举域,以及以基本域构造的复合域。·笛卡儿积域D×D'元素为对偶(x，x')其中x∈D，x'∈D'。D1×D2×…Dn元素为n元组(x1，x2，…，xn)，其中xi∈Di。·不相交的联合域D+D'元素为对偶(leftx，rightx')其中x∈D，x'∈D'。shape=rectangle(Real×Real)+circleReal+point·函数域D→D'例如lnteger→Even。