Topologically sorting VDM-SL definitions for Isabelle/HOL translation
Programming Languages
2023-05-01 v1
Abstract
There is an ecosystem of VDM libraries and extensions that includes a translation and proof environment for VDM in Isabelle. Translation works for a large subset of VDM-SL and further constructs are being added on demand. A key impediment for novice users is that Isabelle/HOL requires all definitions to be declared before they are used, where (mutually) recursive definitions must be defined in tandem. In this paper, we describe a solution to this problem, which will enable wider access to the translator plugin for novice users as well as real models.
Cite
@article{arxiv.2304.15006,
title = {Topologically sorting VDM-SL definitions for Isabelle/HOL translation},
author = {Leo Freitas},
journal= {arXiv preprint arXiv:2304.15006},
year = {2023}
}