关于使用 VeriFast、VerCors、Plural 与 KeY 检查对象用法
计算机科学中的逻辑
2023-02-09 v2 编程语言
摘要
类型状态(typestate)是一种行为类型概念,用于描述有状态对象的协议,以状态机的形式规定每个状态下可用的方法。通常,带有协议的对象要么被强制以线性方式使用,这限制了程序员所能做的操作,要么需要演绎验证来验证这些对象可能被别名化的程序。为了评估面向对象语言的静态验证工具在检查具有协议的共享对象的正确使用方面的优势与局限,我们针对 Java 的四种工具 VeriFast、VerCors、Plural 和 KeY 展开一项调研。我们描述了文件读取器与链表的实现,针对每种工具检查其在对象被共享于集合中时静态保证协议遵从性与协议完成性的能力,并评估程序员为使代码被这些工具接受所付出的努力。
引用
@article{arxiv.2209.05136,
title = {On using VeriFast, VerCors, Plural, and KeY to check object usage},
author = {João Mota and Marco Giunti and António Ravara},
journal= {arXiv preprint arXiv:2209.05136},
year = {2023}
}