Topologically sorting VDM-SL definitions for Isabelle/HOL translation

TL;DR

This paper presents a method for topologically sorting VDM-SL definitions to enable proper translation into Isabelle/HOL, addressing a key usability challenge for novice users and expanding the translation's applicability.

Contribution

It introduces a topological sorting approach for VDM-SL definitions, allowing recursive definitions to be translated correctly into Isabelle/HOL.

Findings

Enables translation of mutually recursive definitions in VDM-SL

Improves accessibility of the translation tool for new users

Facilitates broader adoption of the VDM to Isabelle/HOL ecosystem

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.