We describe recent work on a lightweight verification tool for VDM specifications, called QuickCheck. The objective of the tool is to quickly categorise proof obligations: identifying those that fail with counterexamples, those that are probably provable and those that require deeper analysis. The paper discusses the design of the tool and its use of pluggable strategies for adding extra checking. We present the results of the tool being used to check a large set of VDM specifications, and suggest future directions.
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。