cbmc/specgen/web_interface/README.md

CBMC SpecGen Web Interface

一个现代化的Web界面，用于展示CBMC SpecGen的智能代码验证功能。

🌟 功能特性

• 现代化Web界面: 基于Tailwind CSS的响应式设计
• 实时任务状态: 实时显示代码验证进度
• 代码高亮: 使用Prism.js实现语法高亮
• 任务历史: 查看所有验证任务的历史记录
• API接口: RESTful API支持程序化访问
• 演示模式: 内置演示功能，无需API密钥

🚀 快速开始

方法一：使用启动脚本（推荐）

# 进入Web接口目录
cd web_interface

# 运行启动脚本
./start_web_interface.sh

方法二：手动启动

# 进入后端目录
cd web_interface/backend

# 创建虚拟环境
python3 -m venv venv
source venv/bin/activate

# 安装依赖
pip install -r requirements.txt

# 启动服务器
python app.py

🌐 访问界面

启动后，在浏览器中访问：

• 本地访问: http://localhost:8080
• 网络访问: http://[你的IP地址]:8080

📋 系统要求

• Python 3.8+
• CBMC (用于实际验证)
• 现代Web浏览器

🎯 使用方法

1. 打开浏览器，访问Web界面
2. 加载示例代码或输入自定义C代码
3. **点击"开始验证"**按钮
4. 查看实时进度和验证结果
5. 分析生成的断言代码和CBMC验证输出

🔧 API接口

创建验证任务

POST /api/tasks
Content-Type: application/json

{
    "input_code": "#include <stdio.h>\nint main() { return 0; }",
    "options": {}
}

查询任务状态

GET /api/tasks/{task_id}

获取任务结果

GET /api/tasks/{task_id}/result

获取系统信息

GET /api/system/info

获取示例代码

GET /api/demo/sample

📁 项目结构

web_interface/
├── backend/
│   ├── app.py              # Flask后端应用
│   ├── demo_code.py        # 演示代码生成器
│   ├── requirements.txt    # Python依赖
│   └── venv/              # 虚拟环境
├── frontend/              # 前端资源（如需要）
├── index.html             # 主页面
├── start_web_interface.sh # 启动脚本
└── README.md             # 使用说明

🎨 界面功能

主要区域

1. 系统信息面板: 显示CBMC版本和任务统计
2. 代码输入区: 支持C代码输入和示例加载
3. 任务状态区: 实时显示验证进度
4. 结果展示区:
   • 生成的验证代码（语法高亮）
   • CBMC验证结果
   • 统计摘要
5. 任务历史: 所有验证任务的记录

交互功能

• 加载示例: 一键加载演示代码
• 清空输入: 清除代码编辑器内容
• 复制代码: 复制生成的验证代码
• 查看结果: 点击历史记录查看详细结果

🔍 演示模式

当前版本运行在演示模式下，特点：

• ✅ 无需DeepSeek API密钥
• ✅ 快速生成演示验证代码
• ✅ 模拟CBMC验证结果
• ✅ 完整的用户界面体验

⚠️ 注意事项

1. 演示模式: 当前版本为演示版本，生成的断言为示例性质
2. 网络访问: 如需网络访问，确保防火墙允许8080端口
3. 浏览器兼容: 推荐使用Chrome、Firefox、Safari等现代浏览器
4. 生产部署: 当前为开发环境，生产环境需要使用WSGI服务器

🐛 故障排除

常见问题

1. 端口被占用

   # 查看占用端口的进程
   lsof -i :8080
   # 终止进程
   kill -9 <PID>
   

2. 虚拟环境问题

   # 删除并重新创建虚拟环境
   rm -rf venv
   python3 -m venv venv
   source venv/bin/activate
   pip install -r requirements.txt
   

3. 依赖安装失败

   # 更新pip
   pip install --upgrade pip
   # 使用国内镜像
   pip install -r requirements.txt -i https://pypi.tuna.tsinghua.edu.cn/simple/
   

📞 技术支持

如遇到问题，请检查：

1. Python版本是否满足要求
2. CBMC是否正确安装
3. 网络连接是否正常
4. 浏览器控制台是否有错误信息

---

🎉 享受智能代码验证体验！