Towards Operation Proof Obligation Generation for VDM

TL;DR

This paper discusses advancements in generating proof obligations for VDM, focusing on explicit operation bodies, to improve model consistency verification.

Contribution

It introduces new methods for proof obligation generation in VDM, especially for explicit operation bodies, enhancing tool support and consistency checks.

Findings

Current capabilities demonstrated and evaluated.

Identified remaining challenges and future work.

Improved support for explicit operation bodies in proof obligations.

Abstract

All formalisms have the ability to ensure that their models are internally consistent. Potential inconsistencies are generally highlighted by assertions called proof obligations, and the generation of these obligations is an important role of the tools that support the method. This capability has been available for VDM tools for many years. However, support for obligation generation for explicit operation bodies has always been limited. This work describes the current state of work to address this, showing the capabilities so far and highlighting the work remaining.