在交互式定理证明工具Coq中，我们实现了一个针对块云存储系统（CBS）的验证工具。它具备分离逻辑的关键特性，尤其能支持对CBS程序进行局部推导。
对应实际CBS的主从式架构，工具将CBS细分为两个存储层级:文件层、块层。通过整合内部层级的状态和操作，工具支持表示和验证对实际CBS中的各项数据操作。
事实上，我们基于分离逻辑，实现了一个关于CBS的证明系统。它涉及到构建建模语言、断言语言、分离逻辑三元组和推理规则等环节。这些环节与工程文件的对应关系如下：
- 建模语言——Language.v
- 断言语言——内部堆谓词（InnerPre.v）+ CBS堆谓词（Himpl.v）
- CBS分离逻辑三元组和推理规则——Rules.v
- 验证实例——Example.v
此外，还有一些支持工具开发的原有库文件
- TLC：Coq标准库
- Fmap.v：有限映射
- Var.v: 变量符号
工具的实现共涉及3325行代码，其中包括51条定义，242条引理。
最后，工具还提供了7个实例的证明，它们分别为：拷贝数据块、移动数据块、清除文件、读取文件内容、向文件尾部添加一个数据块、创建文件、拷贝文件。以此说明了工具对CBS程序的表示和推理能力。
本工具的开发环境为：
- 操作系统：Windows 10
- Coq版本：Coq 8.8.0
- IDE : vscode
注意：解压缩后的文件路径中，不可以有中文！！
- 安装Coq
下载地址：
https://github.com/coq/coq/releases/download/V8.8.0/coq-8.8.0-installer-windows-x86_64.exe
完成安装后，需要配置Coq的环境变量：
- 打开环境变量设置
- 在系统变量的Path一栏中，添加Coq的安装路径
-
安装终端模拟器Cmder（需要安装full版本）
下载地址：https://cmder.net/
cmder解压后即可使用，建议和本工具文件解压到同一个根目录中。
-
以管理员方式打开cmder，粘贴如下指令
-
安装软件管理器Chocolatey：
@powershell -NoProfile -ExecutionPolicy unrestricted -Command "iex ((new-object net.webclient).DownloadString('https://chocolatey.org/install.ps1'))" && SET PATH=%PATH%;%ALLUSERSPROFILE%\chocolatey\bin注:如果出现
... 未能创建SSL/TLS安全通道 ...的问题时,可参考如下网站进行解决. https://blog.csdn.net/qq_43650934/article/details/106637645 -
安装make编译工具：
choco install make
-
最后，直接双击*.v文件，可以用CoqIDE审阅相应的代码。
（如果此时Coq崩溃，说明路径中有中文）
