# CBMC SpecGen Web Interface

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

## 🌟 功能特性

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

## 🚀 快速开始

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

```bash
# 进入Web接口目录
cd web_interface

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

### 方法二：手动启动

```bash
# 进入后端目录
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接口

### 创建验证任务
```bash
POST /api/tasks
Content-Type: application/json

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

### 查询任务状态
```bash
GET /api/tasks/{task_id}
```

### 获取任务结果
```bash
GET /api/tasks/{task_id}/result
```

### 获取系统信息
```bash
GET /api/system/info
```

### 获取示例代码
```bash
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. **端口被占用**
   ```bash
   # 查看占用端口的进程
   lsof -i :8080
   # 终止进程
   kill -9 <PID>
   ```

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

3. **依赖安装失败**
   ```bash
   # 更新pip
   pip install --upgrade pip
   # 使用国内镜像
   pip install -r requirements.txt -i https://pypi.tuna.tsinghua.edu.cn/simple/
   ```

## 📞 技术支持

如遇到问题，请检查：
1. Python版本是否满足要求
2. CBMC是否正确安装
3. 网络连接是否正常
4. 浏览器控制台是否有错误信息

---

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