验证一个现实的可变哈希表
软件工程
2024-01-31 v6 编程语言
摘要
在本工作中，我们使用 Stainless 程序验证器验证了 Scala 标准库中的可变 LongMap——一种在单一数组内采用开放寻址的哈希表。作为参考实现，我们编写了基于元组列表的不可变映射。随后我们证明 LongMap 的操作对应于该关联列表的操作。为表达哈希表数组的扩容，我们在 Stainless 中引入了一种新的引用交换构造。这使我们能够应用装饰器模式而不引入别名。我们的验证工作使我们发现并修复了原始实现中在大型哈希表下显现的一个缺陷。性能分析表明，经验证的版本性能在原始数据结构的 1.5 倍因子以内。
引用
@article{arxiv.2107.08824,
title = {Verifying a Realistic Mutable Hash Table},
author = {Samuel Chassot and Viktor Kunčak},
journal= {arXiv preprint arXiv:2107.08824},
year = {2024}
}