【PL理论】(25) C- 语言:表达式求值的推理规则 | 执行语句的推理规则 | 语句执行的推理规则

news2024/7/6 19:45:41

  • 💭 写在前面:本章我们将继续更新我们的 "C-" 语言,更新表达式求值的推理规则、执行语句的推理规则以及语句执行的推理规则。

目录

0x00 C- 语言更新:表达式求值的推理规则

0x01 C- 语言更新:执行语句的推理规则

0x02 C- 语言更新:语句执行的推理规则

0x01 接下来我们该做什么?


0x00 C- 语言更新:表达式求值的推理规则

表达式求值的推理规则,定义为关系:

\color{} \rho ,M\vdash e\Downarrow v

含义:给定环境 \color{} \rho 和内存 \color{} M,表达式 \color{} e 求值为 \color{} v

请注意变量 \color{} x 的语义如何改变,其余表达式情况的语义被省略。

0x01 C- 语言更新:执行语句的推理规则

执行语句的推理规则,定义为关系:

\color{} \left \langle \rho ,M,s \right \rangle\Rightarrow \left \langle {\rho }',{M}'\right \rangle

变量声明的语义如下,边界条件 \color{} l\notin Dom(M) 意味着必须分配一个新的内存位置。

💭 举个例子:填写赋值语句的语义

执行语句的推理规则,定义为关系:

 \color{} \left \langle \rho ,M,s \right \rangle\Rightarrow \left \langle {\rho }',{M}' \right \rangle

如果一个变量被立即重新声明如下,会发生什么?这是一个 bug 吗?

var x = 1;
var x = 2;
...

0x02 C- 语言更新:语句执行的推理规则

语句执行的推理规则,定义为关系:

\color{} \left \langle \rho ,M,s \right \rangle\Rightarrow \left \langle {\rho }',{M}' \right \rangle

与 C 语言不同,这在我们当前的 C- 语义中是允许的:

它可以正常运行,尽管在内存中创建了一个无法访问的位置。

定义为关系:

 \color{} \left \langle \rho ,M,s \right \rangle\Rightarrow \left \langle {\rho }',{M}' \right \rangle

举个例子:填写 if 语句的 true 分支的语义,完成 C- 语句的其他情况的语义是直截了当的。

特别地,while 语句可以类似地处理:

0x01 预告:接下来我们要讨论的内容

在当前的 C- 语言中,你可能已经注意到内存位置只会生成,而不会被释放。

因此,长时间运行的程序可能会耗尽内存。

在现实世界的语言中,我们还必须考虑指针、结构、动态分配等问题。

在下一章中,我们将讨论 内存管理机制 (memory management),比如 自动垃圾回收器 (garbage collector) 。


📌 [ 笔者 ]   王亦优
📃 [ 更新 ]   2024.6.10
❌ [ 勘误 ]   /* 暂无 */
📜 [ 声明 ]   由于作者水平有限,本文有错误和不准确之处在所难免,
              本人也很想知道这些错误,恳望读者批评指正!

📜 参考资料 

Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. .

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.coloradmin.cn/o/1827281.html

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈,一经查实,立即删除!

相关文章

观察者模式(大话设计模式)C/C++版本

观察者模式 扩展&#xff1a;观察者模式——委托 C 参考&#xff1a;https://www.cnblogs.com/Galesaur-wcy/p/15905936.html #include <iostream> #include <list> #include <memory> #include <string> using namespace std;// Observer类 抽象观…

港科夜闻 | 香港科大与香港科大(广州)合推红鸟跨校园学习计划,共享教学资源,促进港穗学生交流学习...

关注并星标 每周阅读港科夜闻 建立新视野 开启新思维 1、香港科大与香港科大(广州)合推“红鸟跨校园学习计划”&#xff0c;共享教学资源&#xff0c;促进港穗学生交流学习。香港科大与香港科大(广州)6月14日共同宣布推出“红鸟跨校园学习计划”&#xff0c;以进一步加强两校学…

5.拼数 - 蓝桥杯

基础知识要求&#xff1a; Java&#xff1a;for循环、if判断、Scanner类、数组、字符串 Python&#xff1a; for循环、if判断、列表、字符串、input() 题目&#xff1a; 思路解析&#xff1a; 读取输入&#xff1a; 首先读取要排序的字符串数量。然后读取相应数量的字符串&am…

【Redis】String的常用命令及图解String使用场景

本文将详细介绍 Redis String 类型的常见命令及其使用场景&#xff0c;包括缓存、计数器、共享会话、手机验证码、分布式锁等场景&#xff0c;并且配图和伪代码进一步方便理解和使用。 命令执行效果时间复杂度set key value [key value…]设置key的值是valueO(k),k是键个数get…

使用消息队列(MQ)实现MySQL持久化存储与MySQL server has gone away问题解决

在现代应用程序开发中&#xff0c;消息队列&#xff08;MQ&#xff09;扮演着重要的角色。它们可以帮助我们解决异步通信和解耦系统组件之间的依赖关系。而其中一个常见的需求是将消息队列中的数据持久化到数据库中&#xff0c;以确保数据的安全性和可靠性。在本文中&#xff0…

gbase8s数据库阻塞检查点和非阻塞检查点的执行机制

1. 检查点的描述 为了便于数据库系统的复原和逻辑恢复&#xff0c;数据库服务器生成的一致性标志点&#xff0c;称为检查点&#xff0c;其是建立在数据库系统的已知和一致状态时日志中的某个时间点检查点的目的在于定期将逻辑日志中的重新启动点向前移动 如果存在检查点&#…

【Quartus 13.0】NIOS II 部署UART 和 PWM

打算在 EP1C3T144I7 芯片上部署 nios ii 做 uart & pwm控制 这个芯片或许不够做 QT 部署 这个芯片好老啊&#xff0c;但是做控制足够了&#xff0c;我只是想装13写 leader给的接口代码是用VHDL写的&#xff0c;我不会 当然verilog我也不太会 就这样&#xff0c;随便写吧 co…

[大模型]XVERSE-7B-chat Transformers 推理

XVERSE-7B-Chat为XVERSE-7B模型对齐后的版本。 XVERSE-7B 是由深圳元象科技自主研发的支持多语言的大语言模型&#xff08;Large Language Model&#xff09;&#xff0c;参数规模为 70 亿&#xff0c;主要特点如下&#xff1a; 模型结构&#xff1a;XVERSE-7B 使用主流 Deco…

【ARMv8/ARMv9 硬件加速系列 3.2 -- SVE 读写内存指令 st1b | st1w | st1w | st1d 使用介绍】

文章目录 SVE Load 和 Store 指令使用介绍LD1 加载指令ST1 存储指令PFR 预取指令参考示例LD1 加载示例ST1 存储示例 代码实例 SVE Load 和 Store 指令使用介绍 ARMv9架构中的SVE&#xff08;Scalable Vector Extension&#xff09;指令集为向量计算提供了强大支持&#xff0c;…

fs.1.10 ON rockeylinux8 dockerfile模式

概述 freeswitch是一款简单好用的VOIP开源软交换平台。 rockeylinux8 docker上编译安装fs.1.10的流程记录&#xff0c;本文使用dockerfile模式。 环境 docker engine&#xff1a;Version 24.0.6 rockylinux docker&#xff1a;8 freeswitch&#xff1a;v1.10.7 dockerfi…

CleanMyMacX4.15.4如何优化苹果电脑系统缓存,告别MacBook卡顿,提升mac电脑性能

你是否曾为苹果电脑存储空间不够而烦恼&#xff1f;是否曾因系统运行缓慢而苦恼&#xff1f;别担心&#xff0c;今天我要给大家种草一个神器——CleanMyMac&#xff01;这款软件可以帮助你轻松解决苹果电脑的种种问题&#xff0c;让你的电脑焕然一新&#xff01; 让我来给大家介…

显著提高iOS应用中Web页面的加载速度 - 提前下载页面的关键资源(如JavaScript、CSS和图像)

手动下载并缓存资源是一种有效的方式&#xff0c;可以确保在需要时资源已经在本地存储&#xff0c;这样可以显著提高加载速度。 缓存整个 web 页面的所有资源文件 具体实现步骤 下载和缓存资源&#xff1a;包括 HTML 文件、CSS、JavaScript 和图像。在应用启动时预加载资源。…

CSS从入门到精通——动画:CSS3动画执行次数和逆向播放

目录 任务描述 相关知识 动画执行次数 动画反向播放 编程要求 任务描述 本关任务&#xff1a;用 CSS3 实现loading效果。效果图如下&#xff1a; 相关知识 为了完成本关任务&#xff0c;你需要掌握&#xff1a;1.动画执行次数&#xff0c;2.动画反向播放。 需要实现的效…

CSS从入门到精通——动画:CSS3动画延迟和完成后状态的保持

目录 任务描述 相关知识 动画状态 动画完成时的状态 动画延迟 编程要求 任务描述 本关任务&#xff1a;用 CSS3 实现小车等待红绿灯的效果。效果图如下&#xff1a; 相关知识 为了完成本关任务&#xff0c;你需要掌握&#xff1a;1.动画状态&#xff0c;2.动画完成时的状…

mac下Xcode在iphone真机上测试运行iOS软件

最近一个需求需要在iPhone真机上测试一个视频直播的项目。 需要解决如何将项目 app 安装到真机上 在进行真机调试。 安装Xcode 直接在App Store上搜索Xcode安装即可。 关键是要安装Simulator。项目需要安装iOS17.5但是由于安装包太大&#xff0c;并且网络不稳定的原因。在Xco…

关于yolov5训练的那些事儿

1.YOLOv5 的模型系列包括从最小到最大的多种模型&#xff1a;YOLOv5n&#xff08;Nano&#xff09;&#xff0c;YOLOv5s&#xff08;Small&#xff09;&#xff0c;YOLOv5m&#xff08;Medium&#xff09;&#xff0c;YOLOv5l&#xff08;Large&#xff09;&#xff0c;以及 YO…

【Linux硬盘读取】Windows下读取Linux系统的文件解决方案:Linux Reader4.5 By DiskInternals

前言 相信做机器视觉相关的很多人都会安装 Windows 和 Linux 双系统。在 Linux 下&#xff0c;我们可以很方便的访问Windows的磁盘&#xff0c;反过来却不行。但是这又是必须的。通过亲身体验&#xff0c;向大家推荐这么一个工具&#xff0c;可以让 Windows 方便的访问 Ext 2/3…

Linux 文件的权限信息解读 chmod修改权限 数字序号表示权限

ls -l #列出当前文件 显示详细信息 drwxr-xr-x. 2 dpc test 6 Jun 15 07:45 test.txt共分为三部分 drwxr-xr-x.&#xff1a;表示文件和文件夹的权限信息dpc &#xff1a;文件&#xff0c;文件夹所属的用户test &#xff1a; 文件和文件夹所属的用户组 drwxr-xr-x 解读 d表示为…

实用软件下载:BetterZip 5最新安装包及详细安装教程

BetterZip是一款功能强大的Mac解/压缩软件&#xff0c;可以满足用户对文件压缩、解压、加密和保护等方面的需求。以下是关于BetterZip软件的主要功能、特点和使用方法的详细介绍&#xff0c;以及对其用户友好度、稳定性和安全性的评价。 安 装 包 获 取 地 址: BetterZip 5-安…

【尚庭公寓SpringBoot + Vue 项目实战】公寓管理(十一)

【尚庭公寓SpringBoot Vue 项目实战】公寓管理&#xff08;十一&#xff09; 文章目录 【尚庭公寓SpringBoot Vue 项目实战】公寓管理&#xff08;十一&#xff09;1、业务介绍2、逻辑模型介绍3、接口开发3.1、保存或更新公寓信息3.2、根据条件分页查询详细信息3.3、根据ID获…