Overture で VDM 数学構文を使用することは可能ですか、それとも ASCII 構文に制限されていますか?
または、LaTeX を生成するときに、出力に数学構文を使用できますか?
LaTeXはほとんど使ったことがありません。出力「.tex」を取得し、TeXファイルで「forall」を「\ forall」に置き換えてからPDFを再生成しようとしましたが、PDFに「\ forall」が挿入されただけです。同じ結果で '$\forall$' に疲れました。
ところで、VDMとOvertureを組み合わせることで、仕様を作成するための素晴らしい環境が整います。