关于 VDM 操作证明义务生成的探索之路
软件工程
2025-06-19 v1
摘要
所有形式化方法都具备确保其模型内部一致性的能力。潜在的不一致性通常由称为证明义务的断言来指示，而生成这些义务的能力是支持该方法工具的重要作用。这一能力在 VDM 工具中已有多年时间。然而，对于显式操作主体的义务生成支持始终有限。本工作描述了为此工作进行的当前进展，展示了迄今为止的能力，并突出了仍需完成的工作。
引用
@article{arxiv.2506.12858,
title = {Towards Operation Proof Obligation Generation for VDM},
author = {Nick Battle and Peter Gorm Larsen},
journal= {arXiv preprint arXiv:2506.12858},
year = {2025}
}
备注
Presented at the 23rd Overture workshop, June 2025 (arXiv:cs/2506.08680)