当前位置：首页 > news >正文

软件工程之形式化说明技术深度解析

news 来源：原创 2025/8/13 17:46:23

按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3种。用自然语言描述需求规格说明书，是典型的非形式化方法。用数据流图或实体-联系图建立模型，是典型的半形式化方法。

所谓形式化方法，是描述系统性质的基于数学的技术，也就是说，如果一种有坚实数学基础，那么它就是形式化的。

前文基础：
1.软件工程学概述：软件工程学概述-CSDN博客

2.软件过程深度解析：软件过程深度解析-CSDN博客

3.软件工程之需求分析涉及的图与工具：软件工程之需求分析涉及的图与工具-CSDN博客

一、概述

（一）非形式化方法的缺点

非形式化方法主要依赖自然语言描述系统需求和设计，其核心缺陷在于语义模糊性和逻辑不严谨性。具体表现为：

（1）矛盾性：同一需求可能存在相互冲突的陈述。例如，某系统需求文档中同时要求“用户必须通过短信验证”和“用户可选择跳过验证”，导致设计无法执行。

（2）二义性：同一描述可能被不同人解读为不同含义。例如，“系统应快速响应”中的“快速”缺乏量化标准，不同开发者可能设定不同阈值（如 1 秒、5 秒）。

（3）含糊性：表述笼统，缺乏具体细节。例如，“系统需具备良好的用户体验”未明确具体指标（如界面响应时间、操作步骤数）。

（4）不完整性：遗漏关键需求或约束条件。例如，某金融系统需求未明确“高并发下的交易一致性”，导致上线后出现数据不一致问题。

（5）抽象层次混乱：高层抽象与低层细节混杂。例如，在需求文档中同时描述业务流程和数据库表结构，导致逻辑层次不清。

（二）形式化方法的优点

形式化方法基于数学逻辑和符号系统，通过严格的数学模型描述系统行为，具有以下显著优势：

（1）精确性：使用数学语言消除歧义，确保需求定义唯一。例如，用一阶逻辑公式明确“所有用户必须登录”的语义。

（2）可验证性：通过数学证明或模型检查技术，验证系统是否满足预期性质。例如，使用模型检查工具SPIN验证通信协议的死锁自由性。

（3）早期错误检测：在开发早期发现设计缺陷，降低后期修改成本。例如，NASA在火星探测项目中使用形式化方法提前发现导航软件的逻辑错误。

（4）跨阶段平滑过渡：从需求规格到系统设计的数学模型可直接映射，支持无缝迭代。例如，Z语言的模式（Schema）可同时描述需求和设计，便于逐步细化。

（5）高可靠性保障：适用于安全关键系统（如航空航天、医疗设备）。例如，空客A320的飞行控制系统通过形式化验证，确保了99.999% 的可靠性。

（三）应用形式化方法的准则

（1）选择适当的表示方法：根据系统特性选择合适的形式化技术。例如，实时系统可采用时间自动机（Timed Automata），并发系统可采用Petri网。

（2）形式化但不过分形式化：仅对关键部分形式化，避免过度复杂。例如，对支付系统的交易逻辑进行形式化，而界面设计采用传统方法。

（3）估算成本与资源：需投入专业人力和工具，需提前评估培训和工具采购成本。例如，使用 Coq 进行定理证明需至少 6 个月的培训周期。

（4）结合传统方法：形式化方法与 UML、敏捷开发等结合，发挥互补优势。例如，用 Petri 网建模并发流程，同时用 UML 活动图描述业务逻辑。

（5）建立详尽文档：用自然语言注释形式化模型，提高可读性。例如，在 Z 语言规格说明中添加需求背景和验证结论。

（6）持续测试与验证：形式化验证无法覆盖所有场景，需结合黑盒测试和白盒测试。例如，对区块链智能合约进行形式化验证后，仍需通过压力测试验证性能。

二、有穷状态机

（一）概念

有穷状态机（Finite State Machine, FSM）是一种基于状态转移的形式化模型，由五元组定义：

（1）状态集Q：有限个状态的集合（如Q = { q0, q1, q2 }）。

（2）输入字母表Σ：输入符号的集合（如Σ= { a, b }）。

（3）状态转移函数δ：形式如δ: Q×Σ→ Q，定义状态间的转移规则。

（4）初始状态q0：系统的起始状态。

（5）终止状态集F ⊆Q：接受输入的状态集合。

FSM通过状态转移描述系统行为，适用于处理离散事件系统（如协议解析、流程控制）。

（二）例子：自动售货机控制系统

项目背景：某自动售货机支持投币、选择商品、退币等操作，需确保交易流程的正确性。

1.状态定义：

q0：初始状态（等待投币）。

q1：已投币状态（等待选择商品）。

q2：商品发放状态（处理出货）。

q3：退币状态（处理退币）。

2.转移函数：

投币（输入a）：δ(q0, a) = q1。

选择商品（输入b）：δ(q1, b) = q2。

退币（输入c）：δ(q1, c) = q3。

出货完成（输入d）：δ(q2, d) = q0。

退币完成（输入e）：δ(q3, e) = q0。

3.状态转移图：

q0 [投币a] → q1

q1 [选商品b] → q2

q1 [退币c] → q3

q2 [出货d] → q0

q3 [退币e] → q0

4.流程说明：

（1）用户投币后进入q1，系统检查余额。

（2）若余额足够，选择商品进入q2，发放商品后返回q0。

（3）若余额不足或用户选择退币，进入q3，退币后返回q0。

数学模型：状态转移函数可表示为矩阵形式：

其中“-”表示无效转移。比如，不存在“q0 [投币a] → q2 [出货d]，因为需要先选择商品 ”。

三、Petri网

（一）概念

Petri网是一种图形化建模工具，用于描述并发和异步系统，由四元组C = (P, T, I, O)定义：

（1）库所（Place）P：用圆圈表示，代表系统状态或资源（如“可用打印机”）。

（2）变迁（Transition）T：用矩形表示，代表事件或操作（如“打印任务”）。

（3）输入函数I：定义库所到变迁的输入弧。

（4）输出函数O：定义变迁到库所的输出弧。

Petri网通过令牌（Token）在库所间的流动模拟系统动态行为，适用于分析并发、同步和死锁问题。

（二）例子：生产流水线控制系统

项目背景：某工厂流水线包含三个工序：加工（T1）、质检（T2）、包装（T3），需协调各工序的资源分配。

Petri 网模型：

1.库所：

P_1：原材料库存（初始有 3 个令牌）。令牌可以理解为资源的个数。

P_2：加工中（初始 0 个令牌）。

P_3：质检中（初始 0 个令牌）。

P_4：包装中（初始 0 个令牌）。

P_5：成品库（初始 0 个令牌）。

2.变迁：

T_1：加工（消耗 1 个P_1，生成 1 个P_2）。

T_2：质检（消耗 1 个P_2，生成 1 个P_3）。

T_3：包装（消耗 1 个P_3，生成 1 个P_4）。

T_4：完成（消耗 1 个P_4，生成 1 个P_5）。

关联矩阵：

其中“-1”表示消耗令牌，“+1”表示生成令牌。

3.动态行为分析：

初始状态：M_0 = (3, 0, 0, 0, 0)。

触发T_1：M_1 = (2, 1, 0, 0, 0)（加工中 1 个工件）。

触发T_2：M_2 = (2, 0, 1, 0, 0)（质检中 1 个工件）。

触发T_3：M_3 = (2, 0, 0, 1, 0)（包装中 1 个工件）。

触发T_4：M_4 = (2, 0, 0, 0, 1)（成品库 1 个工件）。

可达性分析：通过状态方程（其中X为变迁触发向量），可验证系统能否达到目标状态。例如，目标状态M_target = (0, 0, 0, 0, 3)是否可达：

解得x_1 = x_2 = x_3 = x_4 = 3，因此可达。

四、Z语言

（一）简介

Z 语言是一种基于集合论和一阶谓词逻辑的形式化规格说明语言，通过模式（Schema）描述系统状态和行为。其核心要素包括：

1.类型定义：

使用集合、序列、映射等数学结构。

Person == ℕ  // 定义Person类型为自然数（身份证号）

2.模式：

封装状态变量和约束条件。

LoginSystem == [users: P Person;  // 用户集合loggedIn: Person → ℙ;  // 登录状态映射∀ p: Person • p ∈ loggedIn ⇒ p ∈ users  // 约束：登录用户必须在用户集合中]

3.操作定义：

通过模式描述状态转换。

LoginRequest == ΔLoginSystem  // Δ表示状态可修改∧ [p?: Person;  // 输入参数：用户IDp? ∈ users \ loggedIn;  // 前置条件：用户未登录loggedIn' = loggedIn ∪ { p? }  // 后置条件：登录状态更新]

应用案例： IBM在开发客户信息控制系统（CICS）时使用Z语言，将需求错误率降低了70%，开发成本减少9%。

（二）评价

1.优点：

（1）精确性：数学语义确保规格说明无歧义。例如，用集合论定义用户权限，避免自然语言描述的模糊性。

（2）可扩展性：模式可组合和重用。例如，将“用户登录”模式与“权限管理”模式组合，构建完整的访问控制系统。

（3）形式化验证支持：可通过定理证明工具（如 ProofPower）验证规格说明的一致性。例如，证明“登录操作不会导致重复登录”的性质。

2.缺点：

（1）学习曲线陡峭：需掌握集合论、逻辑推理和复杂符号。例如，理解Z语言的量化表达式需要数学基础。

（2）工具支持有限：主流IDE（如Eclipse）对Z语言的支持较弱，依赖专用工具（如Z/EVES）。

（3）不适用于实时系统：缺乏时间建模能力，难以描述时序约束（如“操作必须在5秒内完成”）。

3.工业应用现状：

Z语言在航空航天、金融等领域有成功案例，但受限于学习成本和工具生态，普及率低于UML等半形式化方法。例如，欧洲航天局在阿丽亚娜火箭项目中使用Z语言，但后续项目逐渐转向更易上手的模型驱动方法。

五、结语

形式化说明技术通过数学模型和逻辑推理提升软件系统的精确性和可靠性，尤其适用于安全关键领域。实际应用中需权衡成本与收益：

（1）有穷状态机适用于离散事件系统（如协议解析），通过状态转移图直观描述行为。

（2）Petri网擅长并发系统建模，通过关联矩阵和可达性分析揭示潜在问题。

（3）Z语言提供严格的数学规格说明，适合复杂系统的需求定义和验证。

未来，随着自动化验证工具（如Coq、SPIN）的发展和低代码技术的融合，形式化方法将逐步从实验室走向工业界，成为保障软件质量的核心技术之一。

软件工程之形式化说明技术深度解析

按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3种。用自然语言描述需求规格说明书，是典型的非形式化方法。用数据流图或实体-联系图建立模型，是典型的半形式化方法。所谓形式化方法，是描述系统性…...

编程日记 2025/8/13 17:46:23

Nacos源码—6.Nacos升级gRPC分析一

大纲 1.Nacos 2.x版本的一些变化 2.客户端升级gRPC发起服务注册 3.服务端进行服务注册时的处理 4.客户端服务发现和服务端处理服务订阅的源码分析 1.Nacos 2.x版本的一些变化变化一：客户端和服务端的交互方式由HTTP升级为gRPC Nacos 1.x服务端会提供一系列的…...

编程日记 2025/8/9 12:48:39

使用 React 实现语音识别并转换功能

在现代 Web 开发中，语音识别技术的应用越来越广泛。它为用户提供了更加便捷、自然的交互方式，例如语音输入、语音指令等。本文将介绍如何使用 React 实现一个简单的语音识别并转换的功能。功能概述我们要实现的功能是一个语音识别测试页面&#xff0…...

编程日记 2025/8/13 17:45:02

2.5 点云数据存储格式——大型点云传输格式

通常，进行大型点云数据传输时，一般采用一种后缀为bin的文...

编程日记 2025/8/9 22:58:35

Windows系统下使用Kafka和Zookeeper，Python运行kafka（一）

下载和安装见Linux系统下使用Kafka和Zookeeper 配置 Zookeeper Zookeeper 是 Kafka 所依赖的分布式协调服务。在 Kafka 解压目录下，有一个 Zookeeper 的配置文件模板config/zookeeper.properties，你可以直接使用默认配置。启动 Zookeeper 打开命令提示符（CMD），进入 K…...

编程日记 2025/8/9 22:58:29

数据结构（三）——栈和队列

一、栈和队列的定义和特点栈：受约束的线性表，只允许栈顶元素入栈和出栈对栈来说，表尾端称为栈顶，表头端称为栈底，不含元素的空表称为空栈先进后出，后进先出队列：受约束的线性表&#xff0…...

编程日记 2025/6/29 2:19:48

零基础入门Hadoop：IntelliJ IDEA远程连接服务器中Hadoop运行WordCount

今天我们来聊一聊大数据，作为一个Hadoop的新手，我也并不敢深入探讨复杂的底层原理。因此，这篇文章的重点更多是从实际操作和入门实践的角度出发，带领大家一起了解大数据应用的基本过程。我们将通过一个经典的案例——WordCounter&…...

编程日记 2025/8/11 2:38:24

在Postman中高效生成测试接口：从API文档到可执行测试的完整指南

引言在API开发与测试流程中，Postman是一款高效的工具，能将API文档快速转化为可执行的测试用例。本文以《DBC协议管理接口文档》为例，详细讲解如何通过Postman实现接口的创建、配置、批量生成及自动化测试，帮助开发者和测试人员提升效率，确保接口质量。一、准备工作：理…...

编程日记 2025/6/29 2:19:09

飞云分仓操盘副图指标操作技术图文分解

如上图，副图指标-飞云分仓操盘指标，指标三条线蓝色“首峰线”，红色“引力1”，青色“引力2”，多头行情时“首峰线”和“引力1”之间显示为红色，“引力1”和“引力2”多头是区间颜色显示为紫色。如上图图标信…...

编程日记 2025/8/11 1:00:34

K8s中的containerPort与port、targetPort、nodePort的关系：

pod中的containerPort与service中的port、targetPort、nodePort的关系： 1、containerPort为pod的配置，对应pod内部服务监听的具体端口，例如nginx服务默认监听80端口，那么nginx的pod的containerPort应该配置为80，例如m…...

编程日记 2025/6/29 2:18:25

jquery+ajax+SpringBoot实现前后端分离技术

一、前端方面： 第1步，在前端HTML页面的头部引入jquery <head><meta http-equiv"Content-Type" content"text/html;charsetUTF-8"><title>XXX</title><link rel"stylesheet" type"text/…...

编程日记 2025/8/10 23:49:41

阀门产业发展方向报告（石油化工阀门应用技术交流大会）

本文大部分内容来自中国通用机械工业协会副会长张宗列在“2024全国石油化工阀门应用技术交流大会”上发表的报告。一、国外阀门产业发展从全球阀门市场分布看，亚洲是最大的工业阀门市场，美洲是全球第二大工业阀门市场，欧洲位列第三。从国…...

编程日记 2025/6/29 3:11:28

华为云Astro后端开发中对象、事件、脚本、服务编排、触发器、工作流等模块的逻辑关系如何？以iotDA数据传输过程举例演示元素工作过程

目录 🏭 类比总览：低代码平台就像一座自动化工厂 🧱 1. 对象（Object） = 工厂里的“原材料仓库” 🧱 2. 结构体（Structure） = 自定义的“装配模具” 🔔 3. 事件（Event） = 触发的“感应器” ✍️ 4. 脚本（Script） = 后台的“逻辑处理代码” ⚙️ 5. 服务编…...

编程日记 2025/8/10 22:47:36

面向小型企业顶点项目的网络安全咨询人机协作框架

1. 简介 1.1. 背景和动机由于小型企业无法访问结构化系统，且缺乏大型组织通常拥有的专用资源，它们经常面临巨大的网络安全挑战 [ [1 ]。为大型企业设计的网络安全框架通常对小型企业来说过于复杂且不切实际，导致它们容易受到复杂的网络威胁 2 ]。这种复杂性可能导致小型…...

编程日记 2025/8/9 14:54:46

RSAC 2025观察：零信任+AI=网络安全新范式

2025年4月28日~5月1日，全球最具影响力的网络安全盛会RSAC 2025在美国旧金山举办，吸引了全球44,000名网络安全从业者参与。大会以“Many Voices. One Community.”为主题，聚焦AI安全、供应链风险、零信任等核心议题。其中，AI Agent…...

编程日记 2025/6/29 3:23:16

ruoyi-flowable-plus 前端框架启动报错修复

版本 1. ruoyi-flowable-plus 前端框架启动报错修复启动时设置环境变量 "scripts": {"dev": "SET NODE_OPTIONS--openssl-legacy-provider && vue-cli-service serve","build:prod": "vue-cli-service build",&qu…...

编程日记 2025/8/10 21:44:32

安全可控·高效响应|北峰智能互通矿业通信系统解决方案

项目概况随着矿业行业工作环境日益复杂，涵盖地下开采、露天挖掘、矿物运输及深加工等多个环节，作业区域呈现广阔且分散的特点，往往存在诸多安全风险。当面临突发事故，由于应急救援体系不完善，救援通信系统相对落后&a…...

编程日记 2025/6/29 2:18:22

ubuntu查看安装的软件包的位置

在 Ubuntu 中，libcli11-dev 是一个头文件库（header-only），因此它不会像动态库（.so 文件）那样有明确的下载路径。但你可以通过以下方法查看它的安装位置： 1. 查看 libcli11-dev 安装的文件使用…...

编程日记 2025/8/10 20:39:45

【金仓数据库征文】金仓数据库 KES 助力企业数据库迁移的实践路径

在企业数字化转型浪潮的强力推动下，数据库迁移已成为企业升级 IT 架构、提升数据管理能力的关键环节。从 MySQL 到金仓数据库 KingbaseES（KES）的迁移方案，为企业提供了一条高效、可靠的数据库升级路径。一、迁移挑战与金仓数据…...

编程日记 2025/6/29 3:44:20

准备nginx安装文件：nginx-1.26.2.tar.gz cd /usr/local wget http://nginx.org/download/nginx-1.26.2.tar.gz tar -zxvf nginx-1.26.2.tar.gz && cd nginx-1.26.2 1.创建安装目录 mkdir nginx 2.解压安装文件nginx-1.26.2.tar.gz tar -zxvf nginx-1.26…...

编程日记 2025/8/13 17:46:22

kotlin @JvmStatic注解的作用和使用场景

1. JvmStatic 的作用 JvmStatic 是 Kotlin 提供的一个注解，用于在 JVM 上将伴生对象（companion object）中的方法或属性暴露为 Java 静态方法或字段。作用对象：只能用在 companion object 中的函数或属性。效果： 在 …...

编程日记 2025/8/13 17:45:01

Blind SSRF with Shellshock exploitation过关

Blind SSRF with Shellshock exploitation 生活就像一杯咖啡，苦与甜都是必需的，关键是要学会享受每一口。先说通关方法： 1.首先在bp的扩展商店安装插件 Collaborator Everywhere 2.进入靶场首页复制url https://0af600d3048daad080e6…...

编程日记 2025/8/10 17:34:50

2025-05-08 Unity 网络基础9——FTP通信

文章目录 1 FTP1.1 工作原理1.2 传输模式 2 搭建 FTP 服务器2.1 启用服务2.2 配置站点2.3 设置防火墙2.4 指定用户登录 3 常用 API3.1 NetworkCredential3.2 FtpWebRequest3.3 FtpWebResponse 4 实战操作4.1 上传文件4.2 下载文件4.3 删除文件4.4 获取文件大小4.5 创建文件夹4.…...

编程日记 2025/8/10 21:33:38

3.2.3 掌握RDD转换算子 - 5. 合并算子 - union()

在本节课中，我们学习了Spark RDD的union()算子，它能够将两个数据类型一致的RDD合并为一个新的RDD，主要用于整合不同数据源。通过案例演示，我们成功将两个简单的数字RDD合并，直观地看到合并结果是按原顺序纵向拼接&…...

编程日记 2025/8/13 17:46:23

数据来源合法性尽职调查：保障权益的关键防线

首席数据官高鹏律师团队在当今数字化时代，数据已成为企业和个人最为宝贵的资产之一。然而，伴随着数据的广泛应用与流通，其来源的合法性问题愈发凸显，犹如隐藏在暗处的礁石，稍不留神就可能让涉事主体陷入法律的漩涡。…...

编程日记 2025/8/11 20:39:38

sui在windows虚拟化子系统Ubuntu和纯windows下的安装和使用

一、sui在windows虚拟化子系统Ubuntu下的安装使用（WindowsWsl2Ubuntu24.04） 前言：解释一下WSL、Ubuntu的关系 WSL（Windows Subsystem for Linux）是微软推出的一项功能，允许用户在 Windows 系统中原生运行…...

编程日记 2025/8/10 15:59:24

springmvc的入门案例

springmvc的概述 SpringMVC的概述是一种基于Java实现的MVC设计模型的请求驱动类型的轻量级WEB框架。Spring MVC属于SpringFrameWork的后续产品，已经融合在Spring Web Flow里面。Spring 框架提供了构建 Web 应用程序的全功能 MVC 模块。使用 Spring 可插入的 MVC 架…...

编程日记 2025/6/29 4:44:08

【MCP】为什么使用Streamable HTTP: 相比SSE的优势与实践指南

在现代Web开发中，实时通信已经成为许多应用的核心需求。从聊天应用到股票市场更新，从游戏服务器到AI模型通信，各种技术应运而生以满足这些需求。最近，Model Context Protocol (MCP) 引入了一种新的传输机制 —— Streamable HTTP&…...

编程日记 2025/8/10 14:13:47

CentOS的防火墙工具(firewalld和iptables)的使用

CentOS的防火墙工具因版本不同而异，以下是具体操作步骤： 一、firewalld（CentOS 7及以上默认工具）‌ ‌1、安装与启动‌： 安装：sudo yum install firewalld 启动服务：sudo systemctl start fir…...

编程日记 2025/8/13 17:13:07

解析小米大模型MiMo：解锁语言模型推理潜力

一、基本介绍 1.1 项目背景在大型语言模型快速发展的背景下，小米AI团队推出MiMo系列模型，突破性地在7B参数规模上实现卓越推理能力。传统观点认为32B以上模型才能胜任复杂推理任务，而MiMo通过创新的训练范式证明：精心设计的预训练和强化学习策略，可使小模型迸发巨大推理…...

编程日记 2025/8/10 12:37:21

web 自动化之 Selenium 元素定位和浏览器操作

文章目录一、元素定位的八大方法1、基于 id/name/class/tag_name 定位2、基于 a 标签元素的链接文本定位3、基于xpath定位4、css定位二、浏览器操作1、信息获取2、浏览器关闭3、浏览器控制一、元素定位的八大方法 web 自动化测试就是通过代码对网页进行测试，在…...

编程日记 2025/8/12 5:35:39

vscode如何使用 GitHub Copilot

1.在vscode中扩展工具栏搜索“copilot”，选择GitHub Copilot安装。 2.使用快捷键CtrlAltI 打开聊天界面，输入问题后回车即可使用。注意： 使用copilot需要使用GitHub账号先登录，如果打不开登录页面，需要修改host文件&a…...

编程日记 2025/8/10 10:48:46

AWS之存储服务

存储术语分类接口/技术类型应用场景特点关系及区别机械硬盘接口 IDE（Integrated Drive Electronics） 早期用于个人电脑，现已逐渐淘汰机械硬盘接口、固态硬盘接口是硬盘与主机或其他设备连接的物理和协议规范； FC - …...

编程日记 2025/7/26 11:31:55

安装 Docker

一、CentOS 系统安装 Docker 1. 卸载旧版本（如有） sudo yum remove docker \docker-client \docker-client-latest \docker-common \docker-latest \docker-latest-logrotate \docker-logrotate \docker-engine 2. 安装依赖工具 sudo yum install -y…...

编程日记 2025/8/9 19:08:11

代理协议解析：如何根据需求选择HTTP、HTTPS或SOCKS5？

在现代网络中，代理服务器是一种常见的工具，用于提高安全性、匿名性和访问速度。常见的代理协议包括HTTP、HTTPS和SOCKS5。本文将详细解析这三种代理协议，并帮助您根据具体需求选择最合适的代理协议。一、HTTP代理 1.1 特点用途广泛&…...

编程日记 2025/8/10 8:35:13

用于构建安全AI代理的开源防护系统

大家读完觉得有帮助记得及时关注！！！ 大型语言模型（LLMs）已经从简单的聊天机器人演变为能够执行复杂任务的自主代理，例如编辑生产代码、编排工作流程以及基于不受信任的输入（如网页和电子邮件&am…...

编程日记 2025/8/9 23:20:20

CTF-DAY10

[SWPUCTF 2021 新生赛]zipbomb 题目描述： 请注意，不要以任何方式尝试完全解压该文件，运存被塞满后果自负。请尝试分析该文件。使用WinRAR解压打开 CTFSHOW刷题 crypto11 密文：a8db1d82db78ed452ba0882fb9554fc 提交 flag{明…...

编程日记 2025/8/9 17:15:04

WHAT - react-query(TanStack Query) vs swr 请求

文章目录 react-query什么是 TanStack Query（原 React Query）核心特性 TanStack Query vs SWR 对比具体特性对比哪个更适合你总结 react-query react-query（现已更名为 TanStack Query）和 SWR 一样，都是专注于远程数…...

编程日记 2025/8/9 16:21:55

WebFlux与HttpStreamable关系解析

1-Streamable 1-WebFlux与HttpStreamable关系解析2-MCP协议Streamable HTTP 2-参考网址 MCP协议Streamable HTTPMCP协议重大升级，Spring AI Alibaba联合Higress发布业界首个Streamable HTTP实现方案 3-WebFlux与HttpStreamable关系解析 WebFlux 和 HttpStreamabl…...

编程日记 2025/8/10 0:53:13

深度学习工程化：基于TensorFlow的模型部署全流程详解

深度学习工程化：基于TensorFlow的模型部署全流程详解引言在深度学习项目中，模型训练只是第一步，将模型成功部署到生产环境才是真正创造价值的关键。本文将全面介绍TensorFlow模型从训练到部署的完整工程化流程，涵盖多种部署场…...

编程日记 2025/7/29 10:10:20

RAG技术在测试用例生成中的应用

测试用例中的 RAG 通常指 Retrieval-Augmented Generation（检索增强生成） 在测试领域的应用，是一种结合检索与生成的技术方法，用于自动化生成或优化测试用例。核心概念 RAG 技术背景： • RAG 最初由 Meta 提出…...

编程日记 2025/8/9 20:16:49

uniapp + vue3 + 京东Nut动作面板组件：实现登录弹框组件（含代码、案例、小程序截图）

uniapp + vue3 + 京东Nut动作面板组件：实现登录弹框组件（含代码、案例、小程序截图）代码示下，不再赘述。动作面板组件：https://nutui-uniapp.netlify.app/components/feedback/actionsheet.html 项目背景业务需求描述： uniapp + vue3 + 京东Nut框架：实现登录弹框组…...

编程日记 2025/8/10 5:19:53

在登录页面上添加验证码

这是一个简单的登录页面，里面必须通过验证码通过之后才能够进入页面创建一个servlet（验证码的） package qcby.util;import java.io.IOException; import javax.servlet.ServletException; import javax.servlet.annotation.WebServlet; im…...

编程日记 2025/6/29 3:30:28

人协同的自动化需求分析

多人协同的自动化需求分析是指通过技术工具和协作流程，让多个参与者（如产品经理、开发人员、测试人员等）在需求分析阶段高效协作，并借助自动化手段提升需求收集、整理、验证和管理的效率与质量。以下是其核心要点： 1. …...

编程日记 2025/8/10 4:20:36

C++使用PoDoFo库处理PDF文件

📚 PoDoFo 简介 PoDoFo 是一个用 C 编写的自由开源库，专用于读取、写入和操作 PDF 文件。它适用于需要程序化处理 PDF 文件的应用程序，比如批量生成、修改、合并、提取元数据、绘图等。 🌟 核心特点特性说明📄 P…...

编程日记 2025/8/2 16:04:50

18.Java 序列化与反序列化

18.Java 序列化与反序列化概述在Java中，序列化是将对象的状态信息转换为可以存储或传输的格式的过程，而反序列化则是将这种格式转换回Java对象的过程。序列化要使一个对象支持序列化，该对象必须实现java.io.Serializable接口。这个接…...

编程日记 2025/8/9 21:16:36

大语言模型主流架构解析：从 Transformer 到 GPT、BERT

📌 友情提示： 本文内容由银河易创AI（https://ai.eaigx.com）创作平台的gpt-4-turbo模型生成，旨在提供技术参考与灵感启发。文中观点或代码示例需结合实际情况验证，建议读者通过官方文档或实践进一步确认其准…...

编程日记 2025/8/10 3:11:34

flow-matching 之学习matcha-tts cosyvoice

文章目录 matcha 实现cosyvoice 实现chunk_fmchunk_maskcache_attn stream token2wav 关于flow-matching 很好的原理性解释文章， 值得仔细读，多读几遍，关于文章Flow Straight and Fast: Learning to Generate and Transfer Data with Rectifi…...

编程日记 2025/8/9 3:44:07

聊聊自动化办公未来趋势

1. 自动化办公未来趋势 1.1 智能化与AI融合加深随着人工智能技术的不断成熟，其在自动化办公中的应用将更加广泛和深入。未来，办公软件将具备更强的智能交互能力，能够理解自然语言指令，自动完成复杂的任务，如文档编辑…...

编程日记 2025/8/9 21:18:00

软件工程之需求分析涉及的图与工具

需求分析与规格说明书是一项十分艰巨复杂的工作。用户与分析员之间需要沟通的内容非常的多，在双方交流信息的过程中很容易出现误解或遗漏，也可能存在二义性。如何才能更加准确的表达双方的意思，且清楚明了，绘制各类图形就显得非常…...

编程日记 2025/8/11 16:44:43

一、概述

（一）非形式化方法的缺点

（二）形式化方法的优点

（三）应用形式化方法的准则

二、有穷状态机

（一）概念

（二）例子：自动售货机控制系统

1.状态定义：

2.转移函数：

3.状态转移图：

4.流程说明：

三、Petri网

（一）概念

（二）例子：生产流水线控制系统

1.库所：

2.变迁：

3.动态行为分析：

四、Z语言

（一）简介

1.类型定义：

2.模式：

3.操作定义：

（二）评价

1.优点：

2.缺点：

3.工业应用现状：

五、结语

相关文章：