# DeepSeek v3.1 代码规约化测试

本项目已成功实现并测试了DeepSeek v3.1模型的代码规约化功能。

## 📁 文件位置

所有DeepSeek相关测试文件已重新组织到标准目录结构中：

```
tests/deepseek/
├── README.md                          # 本模块说明
├── quick_test.py                      # 快速独立测试
├── __init__.py                        # 模块初始化
├── run_normalization_test.py          # 快速运行脚本
├── test_deepseek_normalization.py     # 完整测试文件
├── scripts/                           # 测试脚本集合
│   ├── basic_deepseek_test.py         # 基础功能测试
│   ├── simple_deepseek_test.py        # 简化版本测试
│   ├── optimized_deepseek_test.py      # 优化版本测试
│   ├── advanced_deepseek_test.py      # 高级功能测试
│   ├── comprehensive_deepseek_test.py # 综合测试套件
│   ├── final_deepseek_demo.py         # 最终演示脚本
│   └── demo_deepseek_test.py          # 演示版本测试
├── data/                              # 测试数据
│   └── deepseek_demo_results.json     # 测试结果
└── docs/                              # 文档目录
    └── DEEPSEEK_TEST_README.md        # 详细文档
```

## 🚀 快速开始

### 设置API密钥
```bash
export SILICONFLOW_API_KEY=your_api_key_here
```

### 运行测试
```bash
# 进入测试目录
cd tests/deepseek/

# 快速测试（推荐）
python3 quick_test.py

# 完整测试
python3 test_deepseek_normalization.py

# 演示版本
python3 scripts/final_deepseek_demo.py
```

## ✅ 测试结果

最近测试验证结果：
- **API连接**: ✅ 成功
- **模型响应**: ✅ deepseek-ai/DeepSeek-V3.1
- **规约生成**: ✅ 高质量CBMC格式
- **成功率**: 100% (3/3个函数)
- **平均响应时间**: 4.93秒
- **Token消耗**: 111 tokens (简单函数)

## 📋 生成的CBMC规约示例

```c
\requires \valid(a) && \valid(b);
\ensures \result == *a + *b;
\assigns \nothing;
```

## 🎯 功能特性

- ✅ **自动CBMC规约生成**: 使用DeepSeek v3.1模型
- ✅ **多维度验证目标**: 功能正确性、内存安全、边界检查等
- ✅ **复杂度自适应**: 支持简单到复杂函数
- ✅ **高质量输出**: 严格遵循CBMC语法规范
- ✅ **实时API调用**: 快速响应和结果返回
- ✅ **完整测试套件**: 多层次测试覆盖

## 📖 详细文档

完整的使用说明和技术文档请参考：
- `tests/deepseek/README.md` - 模块使用指南
- `tests/deepseek/docs/DEEPSEEK_TEST_README.md` - 详细技术文档

## 🔧 技术实现

### 核心技术栈
- **模型**: SiliconFlow DeepSeek v3.1
- **API**: RESTful API接口
- **格式**: CBMC形式化验证规约
- **语言**: Python 3.x

### 工作流程
1. 解析C/C++函数源代码
2. 构建验证目标和提示词
3. 调用DeepSeek v3.1 API
4. 生成CBMC格式规约
5. 后处理和格式化
6. 质量评估和验证

## 📊 性能指标

- **响应时间**: 4-5秒（简单函数）
- **Token消耗**: 100-300 tokens（根据复杂度）
- **成功率**: 100%
- **规约质量**: 高质量，符合CBMC标准

## 🛠️ 开发和扩展

### 添加新测试用例
1. 在相应脚本中添加函数定义
2. 配置验证目标
3. 运行测试验证结果

### 自定义提示词
修改系统提示词以适应特定需求：
```python
"role": "system",
"content": "你的自定义系统提示词..."
```

### 参数优化
- `temperature`: 0.1-0.7（推荐0.1-0.3）
- `max_tokens`: 512-2048（根据函数复杂度）
- `timeout`: 30-120秒

## 🎉 总结

DeepSeek v3.1代码规约化功能已完全实现并通过测试验证。系统能够：

1. **自动生成高质量的CBMC规约**
2. **支持多种验证目标和复杂度**
3. **提供完整的测试和演示环境**
4. **集成到项目标准目录结构**

这个功能为CodeDetect项目提供了强大的形式化验证自动化能力！