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.