康奈尔CS4110编程语言与逻辑讲义.pdf资源-CSDN文库

需积分: 5 10 浏览量 2024-02-03 12:13:15 上传评论收藏 3.46MB PDF 举报

资源推荐

资源详情

资源评论

CS 4110 – 程序设计语言与逻辑学

讲座 #2: 语义学导论

程序的意义是什么？当我们编写程序时，我们使用字符序列来表示它。但是这些字符串只是具体

的语法，它们并不能告诉我们程序的实际含义。通过执行程序来定义意义是很诱人的——可以使

用解释器或编译器。但是解释器和编译器经常会有错误！我们可以查阅规范手册。但是这些手册

通常只提供语言构造的非正式描述。

定义意义的更好方法是开发一种形式化的、数学的语义学定义。这种方法是明确的、简洁的，

最重要的是，它使得能够对感兴趣的属性进行严格的证明。主要的缺点是语义学本身可能非常复

杂，特别是如果试图模拟现代完整的编程语言的所有特性。

有三种定义语言含义或语义的方式：

 操作语义通过在抽象机器上执行来定义含义。

 指称语义通过数学对象（如函数）来定义含义。

 公理语义通过在执行过程中满足的逻辑公式来定义含义。

这些方法各有优缺点，涉及到数学上的复杂性、在证明中的使用难度以及在解释器或编译器实现

中的使用难度。我们将在本课程的后面讨论这些权衡。

1 算术表达式

为了理解语义的一些关键概念，让我们考虑一个非常简单的整数算术表达式与变量赋值的语言。

这种语言中的程序是一个表达式；执行一个程序意味着将表达式求值为一个整数。为了描述这种

语言的语法结构，我们将使用范围为以下域的变量：

    变量

   整数

  表达式

变量是程序变量的集合（例如， foo， bar， baz， i等）。整数是常量整数的集合（例如， 42， 4

0， 7）。表达式是表达式的域，我们使用BNF（巴科斯-诺尔范式）语法来指定：

 ::= x

 

 

+ 

 

* 

  := 

; 

Mul(Int 2, Add(Var "foo", Int 1))

我们可以使用类层次结构在类似Java的语言中表示相同的结构，尽管会稍微复杂一些：

抽象类 Expr { }

类 Var 扩展 Expr { String name; .. }

类 Int 扩展 Expr { int val; ... }

类 Add 扩展 Expr { Expr exp1, exp2; ... }

类 Mul 扩展 Expr { Expr exp1, exp2; ... }

类 Assgn 扩展 Expr { String var, Expr exp1, exp2; .. }

2 操作语义

我们对表达式的含义有直观的概念。例如， 7 + (4 * 2)的计算结果为 15，

而  := 6 +1 ; 2 * 3 * i的计算结果为 42。在本节中，我们将准确地形式化这种直觉。

操作语义描述程序在抽象机器上的执行方式。小步操作语义描述了这样一种执行方式，即通过

连续的规约来进行——在这里，是对表达式的规约，直到达到表示计算结果的值。抽象机器的状态

通常被称为一个配置。对于我们的语言，一个配置必须包括两个信息：

一个存储（也称为环境或状态），它将整数值映射到变量。在程序执行期间，我们将参考存

储来确定与变量相关联的值，并更新存储以反映对变量的新值的赋值。

要评估的表达式。

我们将存储表示为从变量到整数的部分函数，并将配置表示为表达式和存储的对：

存储 ≜ 变量 ⇀整数

配置 ≜ 存储 表达式

我们将使用尖括号表示配置。例如， ⟨ (foo + 2) * (bar + 2)⟩是一个配置，其中 是一个存储， (fo

o + 2) * (bar + 2)是一个使用两个变量 foo和 bar的表达式。我们语言的小步操作语义是一个关系 

配置配置，描述了一个配置如何过渡到一个新的配置。也就是说，关系 告诉我们如何逐步

评估程序。我们使用中缀符号表示关系 。

也就是说，给定任意两个配置 ⟨

 

⟩和 ⟨

 

⟩，如果 (⟨

 

⟩ ⟨

 

⟩)在关系 中，那么我们写

作 ⟨

 

⟩  ⟨

 

⟩。例如，我们有 ⟨ (4 + 2) * y⟩  ⟨ 6 * y⟩。也就是说，我们可以通过一步评

估配置 ⟨ (4 + 2) * y⟩得到配置 ⟨ 6 * y⟩。

使用这种方法，定义语言的语义归结为定义描述配置之间转换的关系！

这里的一个问题是整数的域是无限的，表达式的域也是无限的。因此，可能的机器配置有无限

多个，可能的单步转换也有无限多个。我们需要一种有限的方式来描述无限集合的可能转换。我

们可以使用推理规则来简洁地描述！。

 = ()

⟨ x ⟩  ⟨ ⟩

VAR

⟨ 

⟩  ⟨

′

 

′

⟩

⟨ 

+ 

⟩  ⟨

′

 

′

⟩

LADD

⟨ 

⟩  ⟨

′

 

′

⟩

⟨  + 

⟩  ⟨

′

  + 

′

⟩

RADD

 =  + 

⟨  + ⟩  ⟨ ⟩

ADD

⟨ 

⟩  ⟨

′

 

′

⟩

⟨ 

* 

⟩  ⟨

′

 

′

* 

⟩

LMUL

⟨ 

⟩  ⟨

′

 

′

⟩

⟨  * 

⟩  ⟨

′

  * 

′

⟩

RMUL

 =   

⟨  * ⟩  ⟨ ⟩

MUL

⟨ 

⟩  ⟨

′

 

′

⟩

⟨ x := 

; 

⟩  ⟨

′

 x := 

′

; 

⟩

ASSGN 1



′

= [  ]

⟨ x :=  ; 

⟩  ⟨

′

 

⟩

ASSGN

推理规则的含义是，如果上方的事实成立，则下方的事实也成立。上方的事实称为前提；下方

的事实称为结论。

没有前提的规则称为公理；有前提的规则称为归纳规则。我们使用符号 [  ]表示将变量 x映

射到整数 ，并将其他变量映射到 映射的值。更明确地说，如果 是函数 [  ]，则有

() =

{

 如果  = 

否则

3 使用语义

现在让我们看看如何使用这些规则。假设我们想要评估表达式 (foo + 2) * (bar + 1)使用一个存储器 其中

(foo) = 4和 (bar) = 3。也就是说，我们想要找到转换的配置 ⟨ (foo + 2) * (bar + 1)⟩。为此，

我们寻找一个具有这种配置形式的规则在结论中。通过检查规则，我们发现唯一与我们的配置形

式匹配的规则是LMUL，其中 

= foo + 2和 

= bar + 1但 

′

尚未知道。我们可以实例化LMUL，

用适当的表达式替换元变量 

和 

。

⟨ foo + 2⟩  ⟨

′

  ⟩

⟨ (foo + 2) * (bar + 1)⟩  ⟨ 

′

* (bar + 1)⟩

LMUL

现在我们需要证明前提实际上成立，并找出 

′

是什么。我们寻找一个规则

其结论与 ⟨ foo + 2⟩  ⟨

′

  ⟩相匹配。我们发现LA DD是唯一匹配的规则：

⟨ foo⟩  ⟨ 

′′

⟩

⟨ foo + 2⟩  ⟨ 

′′

+ 2⟩

LADD

我们对 ⟨ foo⟩  ⟨ 

′′

⟩和 ﬁnd 进行了相同的推理，发现唯一适用的规则是公理

VAR:

(foo) = 4

⟨ foo⟩  ⟨ 4⟩

VAR

剩余110页未读，继续阅读

评论收藏

内容反馈

绝不原创的飞龙

粉丝: 1w+
资源: 1091

康奈尔 CS4110 编程语言与逻辑讲义.pdf

最新资源

康奈尔 CS4110 编程语言与逻辑讲义.pdf

康奈尔 CS1130 面向编程过渡讲义.pdf

康奈尔 CS4820 算法分析导论讲义.pdf

康奈尔 CS3220 科学计算导论.pdf

2021最新手账系列-康奈尔绿.pdf

康奈尔 CS6840 算法博弈论讲义

康奈尔大学金融数学专业解析.pdf

康奈尔 CS6820 算法分析讲义

康奈尔大学开发机器人建模系统.pdf

2021最新手账系列-康奈尔内页2.pdf

2021最新手账系列-康奈尔笔记本.pdf

2021最新手账系列-康奈尔笔记.pdf

2021最新手账系列-横线康奈尔笔记本（超链接） .pdf

康奈尔笔记____模板.pdf

2021最新手账系列-少女心康奈尔.pdf

2021最新手账系列-康奈尔内页3.pdf

2021最新手账系列-康奈尔笔记标准模板(可打印).pdf

2021最新手账系列-学霸直男主题康奈尔笔记本.pdf

康奈尔大学笔记法模板.pdf

b5 康奈尔.pdf b5版的文档模板

相关实用应用程序（Windows可用）

免费可用的ChatGPT网页版.zip

ChatGPT使用总结：150个ChatGPT提示词模板（完整版）

chromedriver-win64.zip

李飞飞自传 我看见的世界 The World I see

全国计算机二级WPSoffice精选350道选择题题库（含答案）.pdf

哈尔滨工业大学-ChatGPT调研报告-2023.3.6-94页.pdf

4个亲测好用的ChatGPT4渠道

农村公交与异构无人机协同配送优化

学术海报模板+论文科研+研究生

最新资源

李飞飞自传我看见的世界 The World I see