diff --git a/thesis/chapters/chapter1_intro.tex b/thesis/chapters/chapter1_intro.tex new file mode 100644 index 0000000..3ef21a2 --- /dev/null +++ b/thesis/chapters/chapter1_intro.tex @@ -0,0 +1,68 @@ +\chapter{绪论} + +\section{研究背景与问题定义} + +PostgreSQL 是当前最具代表性的开源关系型数据库管理系统之一,其代码规模大、模块耦合复杂、演化周期长,长期服务于金融、政企与互联网等高可靠场景。随着版本持续迭代,系统在性能、并发能力与功能丰富度不断提升的同时,也不可避免地产生与修复各类缺陷。相比单次 Bug 个案分析,面向长期提交历史的系统性研究更有助于回答两个核心问题:其一,Bug 修复在时间、作者与模块维度上是否存在稳定规律;其二,修复行为在代码结构层与逻辑约束层是否可被统一建模与验证。 + +现有工程实践中,对 Bug 修复质量的判断通常依赖代码审查与回归测试。然而,测试本质上只能证明“存在问题”或“在有限样例下未发现问题”,难以在全输入空间上证明修复逻辑的完备性。特别是“静默逻辑失效(Silent Failure)”这类非崩溃型缺陷,可能在返回码正常的情况下造成行为偏差,传统测试覆盖不足时容易长期潜伏。因此,本研究将静态结构分析、动态执行追踪与形式化验证联合起来,尝试建立一条可复现、可解释、可证明的 Bug 修复分析路径。 + +基于上述背景,本文将研究对象限定为 PostgreSQL 主分支近年提交,围绕“如何识别高置信 Bug 修复提交、如何抽象修复结构模式、如何验证关键修复的正确性”展开。研究问题可形式化为: +\begin{enumerate} + \item Bug 修复提交在时间分布、作者贡献和模块热点上是否具有可量化规律; + \item 修复前后代码在条件判断、控制流和错误处理路径上是否存在可迁移的结构演化模式; + \item 能否将动态分析发现的逻辑漏洞抽象为约束模型,并利用求解器给出“修复前可构造反例、修复后不可构造反例”的严格证据。 +\end{enumerate} + +\section{研究目标与贡献} + +围绕以上问题,本文设定如下研究目标: +\begin{itemize} + \item 构建 PostgreSQL Bug 修复提交的识别与标注流程,形成可复查的数据基础; + \item 通过静态分析提炼修复行为的结构化特征,给出可解释的模式归纳; + \item 通过动态追踪复现关键案例,定位非崩溃型逻辑缺陷并验证修复效果; + \item 通过 Z3 形式化建模,将“测试结论”提升为“逻辑正确性证明”。 +\end{itemize} + +本文的主要贡献体现在以下三个方面: +\begin{enumerate} + \item \textbf{多证据链研究框架}:提出“提交统计--静态结构--动态轨迹--形式化验证”的闭环分析框架,兼顾宏观规律与微观机制; + \item \textbf{结构化修复模式抽象}:归纳出前置条件显式化、错误路径显式化、条件语义增强等可迁移模式,为后续自动审计与自动修复提供结构基础; + \item \textbf{可证明的修复有效性}:在典型配置同步案例上,以 SAT/UNSAT 对照方式证明修复前后逻辑差异,增强结论的严格性与工程可信度。 +\end{enumerate} + +\section{研究方法与技术路线} + +本文采用分层方法设计,技术路线如图~\ref{fig:tech-route} 所示(可在后续章节补充正式图示): +\begin{enumerate} + \item \textbf{提交数据采集与预处理}:围绕目标时间段提取提交元数据与差异信息; + \item \textbf{Bug 修复识别与标注}:结合关键词信号、结构信号与测试信号,对候选提交进行 Y/M/N 分级标注; + \item \textbf{静态结构演化分析}:使用 AST/libcst 对修复前后代码结构进行对比,统计条件节点、分支路径与错误处理变化; + \item \textbf{动态执行轨迹分析}:基于 PySnooper 与测试脚本复现实例,捕获变量演化与异常触发路径; + \item \textbf{形式化建模与验证}:将关键逻辑抽象为状态与约束,利用 Z3 检验是否存在违反规约的反例。 +\end{enumerate} + +\begin{figure}[H] + \centering + % \includegraphics[width=0.85\textwidth]{figures/tech_route.pdf} + \caption{本文技术路线示意图(占位符,后续替换为正式图)} + \label{fig:tech-route} +\end{figure} + +为确保结果可复现,本文在每个阶段都保留了对应产物:识别规则文档、标注流程说明、动态日志、测试结果及求解脚本。通过多源证据互证,尽量减少单一方法的偏差风险。 + +\section{论文结构} + +全文共七章,章节安排如下: +\begin{itemize} + \item \textbf{第一章 绪论}:说明研究背景、问题定义、目标贡献与技术路线; + \item \textbf{第二章 数据集构建与 Bug 修复识别}:介绍数据来源、识别规则、标注流程与统计结果; + \item \textbf{第三章 Bug 修复结构演化分析(静态)}:给出 AST/libcst 视角下的结构变化与模式归纳; + \item \textbf{第四章 动态执行轨迹与案例复现}:展示关键案例的异常定位、修复策略与回归验证; + \item \textbf{第五章 形式化建模与修复正确性验证}:给出 Z3 建模过程与 SAT/UNSAT 结果对照; + \item \textbf{第六章 综合讨论}:分析三类证据的互补关系、工程启示与有效性威胁; + \item \textbf{第七章 结论与未来工作}:总结研究发现并给出后续拓展方向。 +\end{itemize} + +\section{本章小结} + +本章围绕 PostgreSQL Bug 修复研究的现实需求,明确了本文的问题边界、研究目标与贡献定位,并给出了覆盖“识别--分析--验证”的整体技术路线。后续章节将在统一数据与规则基础上,分别展开静态、动态与形式化三条分析主线,最终形成可复现且可证明的结论体系。 diff --git a/thesis/main.tex b/thesis/main.tex new file mode 100644 index 0000000..8ebffc8 --- /dev/null +++ b/thesis/main.tex @@ -0,0 +1,43 @@ +\documentclass[12pt,a4paper]{ctexbook} + +\usepackage[left=2.8cm,right=2.8cm,top=2.5cm,bottom=2.5cm]{geometry} +\usepackage{setspace} +\usepackage{graphicx} +\usepackage{booktabs} +\usepackage{longtable} +\usepackage{array} +\usepackage{amsmath,amssymb} +\usepackage{hyperref} +\usepackage{float} +\usepackage{caption} + +\hypersetup{ + colorlinks=true, + linkcolor=black, + citecolor=black, + urlcolor=blue +} + +\title{PostgreSQL Bug 修复行为分析与形式化验证} +\author{王虹景} +\date{\today} + +\begin{document} + +\maketitle +\frontmatter +\tableofcontents + +\mainmatter +\input{chapters/chapter1_intro} + +% 后续章节按需添加 +% \input{chapters/chapter2_dataset_and_identification} +% \input{chapters/chapter3_static_analysis} +% \input{chapters/chapter4_dynamic_analysis} +% \input{chapters/chapter5_formal_verification} +% \input{chapters/chapter6_discussion} +% \input{chapters/chapter7_conclusion} + +\backmatter +\end{document} diff --git "a/\350\256\272\346\226\207\347\233\256\345\275\225\344\277\256\346\224\271\346\226\271\346\241\210\357\274\210LaTeX\357\274\211.md" "b/\350\256\272\346\226\207\347\233\256\345\275\225\344\277\256\346\224\271\346\226\271\346\241\210\357\274\210LaTeX\357\274\211.md" new file mode 100644 index 0000000..d3619ce --- /dev/null +++ "b/\350\256\272\346\226\207\347\233\256\345\275\225\344\277\256\346\224\271\346\226\271\346\241\210\357\274\210LaTeX\357\274\211.md" @@ -0,0 +1,161 @@ +# 论文目录修改方案(LaTeX 具体执行版) + +## 1. 本次修改目标 + +针对你“仓库已完成整合、论文使用 LaTeX 撰写”的现状,本方案不再停留在目录建议层,而是提供可直接落地的改造路径: + +1. 明确主控文件与章节拆分方式; +2. 给出逐文件修改清单; +3. 统一章节命名、引用与图表编号规范; +4. 确保你可以从现有 `.md/.log/.py` 材料快速迁移到 LaTeX 论文。 + +--- + +## 2. 目录结构修改为“可编译工程” + +建议将论文部分固定为以下结构(已按本仓库落地): + +```text +thesis/ +├── main.tex +└── chapters/ + ├── chapter1_intro.tex + ├── chapter2_dataset_and_identification.tex + ├── chapter3_static_analysis.tex + ├── chapter4_dynamic_analysis.tex + ├── chapter5_formal_verification.tex + ├── chapter6_discussion.tex + └── chapter7_conclusion.tex +``` + +说明:目前已新增 `main.tex` 与 `chapter1_intro.tex`,其余章节按同样模式继续补齐。 + +--- + +## 3. 逐文件具体修改方案 + +### 3.1 `thesis/main.tex`(主控文件) + +需要保留并检查以下点: + +1. 文档类使用 `ctexbook`,保障中文章节与目录正常; +2. 统一加载基础宏包:`geometry`、`graphicx`、`booktabs`、`amsmath`、`hyperref`; +3. 前置部分包含:`\maketitle`、`\tableofcontents`; +4. 正文部分使用 `\input{chapters/chapterX_xxx}` 按章拆分; +5. 先保证第一章可编译,再逐章解除注释。 + +### 3.2 `thesis/chapters/chapter1_intro.tex`(绪论) + +本章建议固定为 5 节: + +- 1.1 研究背景与问题定义 +- 1.2 研究目标与贡献 +- 1.3 研究方法与技术路线 +- 1.4 论文结构 +- 1.5 本章小结 + +写作要求: + +1. 背景中要交代 PostgreSQL 的工程复杂度与 Bug 修复研究价值; +2. 问题定义要明确“测试不足以证明正确性”,引出形式化验证; +3. 技术路线需覆盖统计、静态、动态、形式化四段证据链; +4. 小结要为第二章做承接。 + +### 3.3 第二至七章(待补齐文件) + +按以下模板创建文件并在 `main.tex` 中 `\input`: + +- `chapter2_dataset_and_identification.tex` +- `chapter3_static_analysis.tex` +- `chapter4_dynamic_analysis.tex` +- `chapter5_formal_verification.tex` +- `chapter6_discussion.tex` +- `chapter7_conclusion.tex` + +每章最少包含:`\chapter` + 3 个 `\section` + `\section{本章小结}`。 + +--- + +## 4. 仓库材料到章节的迁移映射(可直接执行) + +### 第二章(数据与识别) + +来源: + +- `bug_fix_identification_rules.md` +- `bug_fix_commit_rules_member2.md` +- `bug_fix_annotation_workflow.md` +- `bug_fix_trend_analysis.md` +- `bug_fix_trend_analysis_conclusion.md` + +迁移方法: + +1. 规则类文档进“2.2 识别规则”; +2. 标注流程进“2.3 标注流程与质量控制”; +3. 时间/作者/模块统计进“2.4 描述性统计”。 + +### 第三章(静态分析) + +来源: + +- `bug_fix.md` +- `bug_fix_structure_feature.md` +- `fix_example.md` + +迁移方法: + +1. 概念与方法写入“3.1 AST/libcst 方法”; +2. 模式总结写入“3.2/3.3 结构演化规律”; +3. 示例代码放附录或代码块环境。 + +### 第四章(动态分析) + +来源: + +- `dynamic_analyze/dynamic_analyze.md` +- `dynamic_analyze/成员四总结报告.md` +- `dynamic_analyze/异常逻辑识别报告.md` +- `dynamic_analyze/逻辑修复与验证报告.md` +- `dynamic_analyze/da_*.log` 与 `test_validation*.log` + +迁移方法: + +1. 异常发现、定位证据、修复回归按“问题-证据-修复-验证”组织; +2. 日志只保留关键片段,完整日志放附录。 + +### 第五章(形式化验证) + +来源: + +- `z3-solver/verify_config_logic.py` +- `z3-solver/verify_fix.py` +- `z3-solver/PostgreSQL 配置同步逻辑的形式化验证报告 (Z3-Solver).md` + +迁移方法: + +1. 抽象变量与规约写“5.1”; +2. SAT 反例写“5.2”; +3. UNSAT 证明写“5.3”; +4. 强调“从测试到证明”的方法价值写“5.4”。 + +--- + +## 5. LaTeX 规范(避免返工) + +1. 图表统一:图 `Figure`、表 `Table`,均用 `\label`+`\ref`; +2. 公式仅在需要时使用 `equation` 环境,避免行内堆叠; +3. 代码片段建议使用 `verbatim` 或后续引入 `listings`; +4. 英文术语首次出现中英文并列:如“静默逻辑失效(Silent Failure)”; +5. 每章末尾必须有“本章小结”,保证论证连贯。 + +--- + +## 6. 一次性执行清单(按顺序) + +1. 先编译 `thesis/main.tex`,确认第一章通过; +2. 逐章创建 chapter2--chapter7 文件并填最小骨架; +3. 按“第 4 节映射表”迁移已有材料; +4. 补图表编号、交叉引用与参考文献; +5. 最后统一摘要、结论、附录格式与术语。 + +执行完这 5 步后,你的论文将从“资料集合”升级为“可编译、可提交、可答辩”的 LaTeX 成稿框架。