Add LaTeX thesis scaffold and full Chapter 1

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 修复研究的现实需求，明确了本文的问题边界、研究目标与贡献定位，并给出了覆盖“识别--分析--验证”的整体技术路线。后续章节将在统一数据与规则基础上，分别展开静态、动态与形式化三条分析主线，最终形成可复现且可证明的结论体系。

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}

论文目录修改方案（LaTeX）.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 成稿框架。