Towards Operation Proof Obligation Generation for VDM
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913899298684928 |
|---|---|
| author | Battle, Nick Larsen, Peter Gorm |
| author_facet | Battle, Nick Larsen, Peter Gorm |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_12858 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards Operation Proof Obligation Generation for VDM Battle, Nick Larsen, Peter Gorm Software Engineering 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. |
| title | Towards Operation Proof Obligation Generation for VDM |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2506.12858 |