Is it possible to use the VDM mathematical syntax with Overture or is it restricted to the ASCII syntax.
Alternatively, when generating LaTeX, can the mathematical syntax be used for the output?
I have barely used LaTeX. I tried taking the output '.tex' and replacing 'forall' with '\forall' in the TeX file, then regenerated the PDF, but that just inserted '\forall' in the PDF. I tired with '$\forall$' with the same result.
By the way, VDM and Overture in combination make for a fantastic environment in which to create specifications.
Alas no, neither Overture nor VDMJ can use the mathematical notation. I believe VDMTools can though (its pretty printing), but it would be quite annoying to switch between the two just for that. It would be relatively easy to add to Overture, but perhaps of limited use? One of the things I've found over the years is that the mathematical notation is quite off-putting to beginners.
The link below summarizes the differences between Overture and VDMTools, and mentions the pretty printer: http://wiki.overturetool.org/index.php/Differences_between_Overture_and_VDMTools
We're very pleased to hear you find Overture useful. If you have any problems or suggestions, do get in touch and we'll try to help - http://overturetool.org/.