使用 Kind 2 进行契约的可实现性检查
计算机科学中的逻辑
2022-05-19 v1
摘要
我们展示了开源模型检测器 Kind 2 的一项新特性，该特性检查组件契约是否可现实化（realizable）；即，是否可能构造一个组件，使得对于契约假设所允许的任何输入，组件都能产生某个满足契约保证的输出值。当契约被证明不可现实化时，它提供一个死锁计算以及一组冲突的保证。这一新特性可用于检测组件规范中的缺陷，并确保 Kind 2 组合证明论证的正确性。
引用
@article{arxiv.2205.09082,
title = {Realizability Checking of Contracts with Kind 2},
author = {Daniel Larraz and Cesare Tinelli},
journal= {arXiv preprint arXiv:2205.09082},
year = {2022}
}