|
|
#!/usr/bin/env python3
|
|
|
"""
|
|
|
DeepSeek v3.1代码规约化演示脚本
|
|
|
|
|
|
模拟API调用的演示版本，展示预期的输出格式
|
|
|
"""
|
|
|
|
|
|
import time
|
|
|
import json
|
|
|
|
|
|
|
|
|
def simulate_api_call(function_info, verification_goals):
|
|
|
"""模拟API调用"""
|
|
|
# 模拟网络延迟
|
|
|
time.sleep(1)
|
|
|
|
|
|
# 根据函数生成不同的规约
|
|
|
if function_info['name'] == 'add_numbers':
|
|
|
specification = """\\requires \\valid(a) && \\valid(b);
|
|
|
\\ensures \\result == a + b;
|
|
|
\\assigns \\nothing;"""
|
|
|
raw_content = """根据函数 `add_numbers` 的功能，我生成以下CBMC规约：
|
|
|
|
|
|
```c
|
|
|
\\requires \\valid(a) && \\valid(b);
|
|
|
\\ensures \\result == a + b;
|
|
|
\\assigns \\nothing;
|
|
|
```
|
|
|
|
|
|
这个规约确保：
|
|
|
1. 输入参数a和b是有效的
|
|
|
2. 返回值等于a和b的和
|
|
|
3. 函数不修改任何外部状态"""
|
|
|
tokens_used = 156
|
|
|
elif function_info['name'] == 'safe_divide':
|
|
|
specification = """\\requires \\valid(result) && b != 0;
|
|
|
\\ensures \\result == true ==> *result == a / b;
|
|
|
\\assigns *result;"""
|
|
|
raw_content = """为安全除法函数 `safe_divide` 生成CBMC规约：
|
|
|
|
|
|
```c
|
|
|
\\requires \\valid(result) && b != 0;
|
|
|
\\ensures \\result == true ==> *result == a / b;
|
|
|
\\assigns *result;
|
|
|
```
|
|
|
|
|
|
规约说明：
|
|
|
- 前置条件：result指针有效且除数b不为0
|
|
|
- 后置条件：如果返回true，则result指向的值等于a/b
|
|
|
- 赋值说明：函数只修改*result的值"""
|
|
|
tokens_used = 234
|
|
|
else:
|
|
|
specification = """\\requires true;
|
|
|
\\ensures \\result == \\old(\\result);
|
|
|
\\assigns \\nothing;"""
|
|
|
raw_content = "默认规约"
|
|
|
tokens_used = 89
|
|
|
|
|
|
return {
|
|
|
'specification': specification,
|
|
|
'raw_content': raw_content,
|
|
|
'generation_time': 1.5,
|
|
|
'tokens_used': tokens_used,
|
|
|
'success': True
|
|
|
}
|
|
|
|
|
|
|
|
|
def create_test_functions():
|
|
|
"""创建测试函数"""
|
|
|
return [
|
|
|
{
|
|
|
'name': 'add_numbers',
|
|
|
'return_type': 'int',
|
|
|
'parameters': [
|
|
|
{'name': 'a', 'type': 'int'},
|
|
|
{'name': 'b', 'type': 'int'}
|
|
|
],
|
|
|
'source_code': 'int add_numbers(int a, int b) { return a + b; }',
|
|
|
'verification_goals': ['functional_correctness']
|
|
|
},
|
|
|
{
|
|
|
'name': 'safe_divide',
|
|
|
'return_type': 'bool',
|
|
|
'parameters': [
|
|
|
{'name': 'a', 'type': 'int'},
|
|
|
{'name': 'b', 'type': 'int'},
|
|
|
{'name': 'result', 'type': 'int*'}
|
|
|
],
|
|
|
'source_code': '''bool safe_divide(int a, int b, int *result) {
|
|
|
if (b == 0 || result == NULL) {
|
|
|
return false;
|
|
|
}
|
|
|
*result = a / b;
|
|
|
return true;
|
|
|
}''',
|
|
|
'verification_goals': ['functional_correctness', 'memory_safety', 'error_handling']
|
|
|
}
|
|
|
]
|
|
|
|
|
|
|
|
|
def main():
|
|
|
"""主演示函数"""
|
|
|
print("🚀 DeepSeek v3.1 代码规约化演示")
|
|
|
print("=" * 50)
|
|
|
print("⚠️ 注意: 这是演示版本，模拟API调用输出")
|
|
|
print("=" * 50)
|
|
|
|
|
|
# 模拟API密钥检查
|
|
|
print("🔑 检查API密钥...")
|
|
|
time.sleep(0.5)
|
|
|
print("✅ API密钥已设置 (演示模式)")
|
|
|
|
|
|
# 模拟健康检查
|
|
|
print("\n🔍 检查API状态...")
|
|
|
time.sleep(0.5)
|
|
|
print("✅ API健康 (响应时间: 1.23s)")
|
|
|
|
|
|
# 测试函数
|
|
|
test_functions = create_test_functions()
|
|
|
|
|
|
for i, func in enumerate(test_functions, 1):
|
|
|
print(f"\n{'='*20} 测试 {i} {'='*20}")
|
|
|
print(f"📝 函数: {func['name']}")
|
|
|
print(f"🎯 目标: {', '.join(func['verification_goals'])}")
|
|
|
|
|
|
print("\n⏳ 正在生成规约...")
|
|
|
result = simulate_api_call(func, func['verification_goals'])
|
|
|
|
|
|
if result['success']:
|
|
|
print(f"✅ 生成成功!")
|
|
|
print(f"⏱️ 时间: {result['generation_time']:.2f}s")
|
|
|
print(f"🔤 Token: {result['tokens_used']}")
|
|
|
|
|
|
print(f"\n📋 生成的CBMC规约:")
|
|
|
print("-" * 40)
|
|
|
print(result['specification'])
|
|
|
print("-" * 40)
|
|
|
|
|
|
print(f"\n📄 原始输出:")
|
|
|
print("-" * 40)
|
|
|
print(result['raw_content'])
|
|
|
print("-" * 40)
|
|
|
else:
|
|
|
print(f"❌ 生成失败: {result['error']}")
|
|
|
|
|
|
print(f"\n🎉 演示完成!")
|
|
|
|
|
|
# 使用说明
|
|
|
print(f"\n" + "="*50)
|
|
|
print("📖 实际使用步骤")
|
|
|
print("="*50)
|
|
|
print("1. 获取SiliconFlow API密钥")
|
|
|
print("2. 设置环境变量: export SILICONFLOW_API_KEY=your_key")
|
|
|
print("3. 运行实际测试: python3 basic_deepseek_test.py")
|
|
|
print("4. 查看生成的CBMC规约")
|
|
|
|
|
|
print(f"\n🔗 生成的文件:")
|
|
|
print("- basic_deepseek_test.py (基础测试脚本)")
|
|
|
print("- simple_deepseek_test.py (异步版本)")
|
|
|
print("- test_deepseek_normalization.py (完整版本)")
|
|
|
print("- DEEPSEEK_TEST_README.md (详细文档)")
|
|
|
|
|
|
print(f"\n💡 CBMC规约说明:")
|
|
|
print("- \\requires: 前置条件")
|
|
|
print("- \\ensures: 后置条件")
|
|
|
print("- \\assigns: 赋值说明")
|
|
|
print("- \\valid: 有效性检查")
|
|
|
print("- \\forall: 全称量词")
|
|
|
print("- \\exists: 存在量词")
|
|
|
|
|
|
|
|
|
if __name__ == "__main__":
|
|
|
main() |
