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

  • 💭 写在前面:本章我们将继续更新我们的 "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.xdnf.cn/news/1452860.html

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

相关文章

13.docker registry(私有仓库)

docker registry(私有仓库) 1.从公有仓库中下载镜像比较慢 ,比如docker run执行一个命令假设本地不存在的镜像,则会去共有仓库进行下载。 2.如果要是2台机器之间进行拷贝,则拷贝的是完整的镜像更消耗空间。 3.如果1个…

springboot优雅shutdown时如何保障异步线程的安全

我前面写了一篇springboot优雅shutdown的文章,看起来一切很美好。 https://blog.csdn.net/chenshm/article/details/139640775 那是因为没有进行多线程测试。如果一个请求中包括阻塞线程(主线程)和非阻塞线程(异步线程&#xff09…

JVM 垃圾回收分配及算法

一、判断对象是否可以回收 垃圾收集器在做垃圾回收的时候,首先需要判定的就是哪些内存是需要被回收 的,哪些对象是「存活」的,是不可以被回收的;哪些对象已经「死掉」了,需 要被回收。 一般有两种方法来判断&#xff…

[Cloud Networking] SPDY 协议

文章目录 1. 背景2. SPDY 之前3. SPDY 项目目标4. SPDY 功能特点4.1 SPDY基本功能4.2 SPDY高级功能 1. 背景 TCP是通用的、可靠的传输协议,提供保证交付、重复抑制、按顺序交付、流量控制、拥塞避免和其他传输特性。 HTTP是提供基本请求/响应语义的应用层协议。 不…

第一篇:容器化的未来:从Docker的革命到云原生架构

容器化的未来:从Docker的革命到云原生架构 1. 引言 在当今快速演进的技术领域,容器化技术已经成为云计算和微服务架构的重要组成部分。该技术以其高效的资源利用率、快速的部署能力和卓越的隔离性能,彻底改变了软件开发和部署的方式。容器化…

RPG游戏完整指南

环境:unity2021urp 本教程教大家如何使用Unity创建一个RPG游戏,玩家可以在城镇场景中进行导航并寻找战斗,并在战斗中遇到不同类型的敌人。玩家可以向敌人施加不同的动作,如:常规攻击和撤离。这会是一个十分有趣的体验。…

c++20 规范, vs2019 , 头文件 <mutex> ,注释以及几个探讨

(1 探讨一) mutex 这个名称的来源是 mutual exclusion :互相排斥。 mutex 与 recursive_mutex 的数据成员的定义如下: 测试如下: 运行以下: 以及: (2 探讨二) recursive_…

cmake构建Qt项目

cmake构建Qt项目 项目结构 一、添加头文件 # 添加头文件目录,还需要在add_executable中添加头文件!!! include_directories(${CMAKE_CURRENT_SOURCE_DIR}/include) add_executable(landlardsinclude/test.h)二、添加源文件 aux…

【内存管理之堆内存】

1.栈上的基元 2.栈上的聚合对象 3.手动分配和释放 4.分配堆内存 5.数组内存分配和释放 6.数组内存分配 7.不要使用野指针 8.黑暗时代

SpringBoot 第一天

什么是Spring Boot 学习过spring,并且做过项目的估计都经历过,xml文件的繁杂配置,让人眼花缭乱,且极易出错,因此 Spring 一度被称为“配置地狱” 为了简化 Spring 应用的搭建和开发过程,Pivotal 团队在 S…

跻身中国市场前三,联想服务器的“智变”与“质变”

IDC发布的《2024年第一季度中国x86服务器市场报告》显示,联想服务销售额同比增长200.2%,在前十厂商中同比增速第一,并跻身中国市场前三,迈入算力基础设施“第一阵营”。 十年砺剑联想梦,三甲登榜领风骚。探究联想服务器…

datax图形化界面datax-web安装及使用

环境准备:需要先安装git和maven git安装可参考git的安装-CSDN博客 maven只需解压安装包,配置环境变量即可使用 1 源代码下载 直接从Git上面获得datax-web源代码 git clone https://gitee.com/WeiYe-Jing/datax-web.git 2 打包项目 进入项目源码根…

springboot原理篇-bean管理

springboot原理篇-bean管理(二) 我们今天主要学习IOC容器中Bean的其他使用细节,主要学习以下三方面: 如何从IOC容器中手动的获取到bean对象bean的作用域配置管理第三方的bean对象 一、获取Bean 了解即可,默认情况下…

河南资信评价资质申报日期一览

河南资信评价资质申报日期一览如下: 一、申报批次与截止日期 第一批次 开始时间:根据历年经验,第一批次的申报通常在上半年进行,但具体开始时间需以河南省工程咨询协会发布的官方公告为准。截止时间:第一批次的截止日…

(源码)供应商电子招投标管理系统实现方案和功能说明

采购在线招投标供应商管理系统是一个集成了多个关键功能的综合性系统,旨在优化采购流程、提高效率和确保透明度。以下是关于您提到的五个核心功能的详细解释: 供应商管理 此功能允许企业记录和管理供应商的基本信息,如公司名称、联系方式、主…

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

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

java第二十四课 —— super 关键字 | 方法重写

super 关键字 基本介绍 super 代表父类的引用,用于访问父类的属性、方法、构造器。 基本语法 访问父类的属性,但不能访问父类的 private 属性。 super.属性名; 访问父类的方法,不能访问父类的 private 方法。 super.方法名(参数列表); 访…

ord版本升级(0.15升级到0.18.5)

1、升级rust ~# rustup update stable ~# rustc --versionrustc 1.79.0 (129f3b996 2024-06-10)2、拉取0.18.5代码 ~# wget https://github.com/ordinals/ord/archive/refs/tags/0.18.5.tar.gz ~# tar -xf 0.18.5.tar.gz ~# cd ord-0.18.5 ~# cargo build --release3、启动se…

开源高效API管理工具:RAP

RAP:简化API开发,提升团队协作效率- 精选真开源,释放新价值。 概览 RAP(RESTful API Project)是一个开源的API管理工具,由阿里巴巴团队开发并维护。它旨在帮助前后端开发人员通过一个统一的平台来设计、开…

Nginx - 反向代理、负载均衡、动静分离(案例实战分析)

目录 Nginx 开始 概述 安装(非 Docker) 配置环境变量 常用命令 配置文件概述 location 路径匹配方式 配置反向代理 实现效果 准备工作 具体配置 效果演示 配置负载均衡 实现效果 准备工作 具体配置 实现效果 其他负载均衡策略 配置动…