嘉定网站建设哪里便宜,如何推动一个教学网站的建设,校园生活网页设计图片模板,济南正宗网站建设平台#x1f4ad; 写在前面#xff1a;本章我们将继续探讨形式化语义#xff0c;讲解语义树#xff0c;然后我们将讨论“为什么需要形式化语义”#xff0c;以及讲述一个比较有趣的事实#xff08;大部分编程语言设计者其实并不会形式化语义的定义#xff09;。
目录
0x00… 写在前面本章我们将继续探讨形式化语义讲解语义树然后我们将讨论“为什么需要形式化语义”以及讲述一个比较有趣的事实大部分编程语言设计者其实并不会形式化语义的定义。
目录
0x00 语义树Derivation Tree
0x01 关于实现语言
0x02 为什么需要形式化语义
0x03 事实部分编程语言的设计者并不会形式化语义 0x00 语义树Derivation Tree
对于程序 如果存在 使得 则其语义被定义 (即成功终止) 。
这里符号 表示初始内存是空的。 举个例子用于程序 x1; yx5 的推导树
x 1
y x 50x01 关于实现语言
我们可以实现一个解释器来解释我们迄今设计的语言我们可以尝试使用 F# 来实现解释器。
例如语义域 可以实现为
type Val Int of int | Boolean of bool
例如表达式的评估可以实现为
let rec eval (e: Exp) (m: Mem) : Val ...
归纳定义 (Inductive definition) 可以通过递归实现。
对于某些程序语义未定义例如
y x true // 无法应用任何规则
这类程序可以认为是运行时错误在实现中我们将设计解释器让其抛出异常。 0x02 为什么需要形式化语义
我们上一章到目前为止都在谈论 形式化语义formal semantics
形式化语义是计算机科学和语言学中的一个重要领域。
它旨在使用形式化的数学工具来准确地描述自然语言或计算机程序的含义。
用形式化方法来定义语言的结构和含义以及推导出语言表达式的含义和行为。
主要目标就是消除歧义确保语言或程序的含义在不同环境下的一致性和可预测性。
它通常包括以下几种主要方法
操作语义Operational Semantics语义动态学Dynamic Semantics语义形式学Denotational Semantics公理化语义Axiomatic Semantics
.
❓ 思考为什么需要形式化语义
因为需要形式地证明某些有用的属性比如
证明类型推断算法的正确性。证明编译器优化的正确性证明程序分析算法的正确性。
所有这些都与程序的行为 (语义) 相关因此我们首先必须定义这种语义比如
要证明优化的正确性我们首先需要定义两个程序的语义等价 0x03 事实部分编程语言的设计者并不会形式化语义
UUUUnfortunately非常不幸的是编程语言的爹爹们通常不会 规范的 定义其语义
例如C 和 JavaScript 的语义是用自然语言口头描述的。
JavaScript 的语义特别复杂经常令人难以理解这样产生了许多有趣的研究
因此编程语言研究者首先必须正式定义他们想讨论的语言的语义
例如CompCert 的作者首先定义了 C 语言的语义以便制作一个带有正确性证明的编译器。 [ 笔者 ] 王亦优[ 更新 ] 2023.6.12
❌ [ 勘误 ] /* 暂无 */[ 声明 ] 由于作者水平有限本文有错误和不准确之处在所难免本人也很想知道这些错误恳望读者批评指正 参考资料 Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. .
