VDM to HOL model and proof obligation translation
One recent addition to the
Overture project is an
Automatic Proof Support system, developed by Sander Vermolen.
In our work we make much use of this system's translator, as well as the proof tactics.
We have contributed in widening the translator VDM++ syntax knowledge, implementing some basic (but essential to have recursive functions translated) operators like hd (head), tl (tail), len (length) and ^(concatenation).
Another contribution is the pre-processing script and parsers, that allow us to automaticaly pre process a VDM++ model to be translated (including its proof obligations), the complete package with source can be found
here.