文件名称：stablesort:Coq中的稳定排序算法及其稳定性证明
文件大小：20KB
文件格式：ZIP
更新时间：2024-04-14 05:36:29
coq ssreflect mathcomp Coq
Coq中的稳定排序算法 该库提供了一种通用的方法来证明排序算法的稳定性。 使用规范结构（ StableSort.interface ）重载了此库中提供的稳定性引理，并且在该接口中，稳定的排序函数通过表示排序和征服结构的参数公理和二叉树来表征。 通过使用参数转换（Paramcoq）并提供与二叉树构造相对应的引理，可以证明新排序函数的稳定性。 该库还提供了优化的排序算法：一种用于CBN.sort调用评估（ CBN.sort ），另一种用于按值调用评估（ CBV.sort ）。 元 作者： 坂口和彦（首字母） 许可证： 兼容的Coq版本：8.11或更高版本 其他依赖项： 开发版本 1.1.2或更高版本 Coq名称空间： stablesort 相关出版物：无 建造和安装说明 在Coq中安装最新版本的稳定排序算法的最简单方法是通过 ： opam repo add coq-released
【文件预览】：
stablesort-master
----.gitignore(65B)
----CeCILL-B(21KB)
----Makefile(943B)
----_CoqProject(98B)
----.github()
--------workflows()
----meta.yml(2KB)
----README.md(2KB)
----theories()
--------param.v(874B)
--------stablesort.v(29KB)
----coq-stablesort.opam(1KB)