VDM+TeXで形式仕様書を作る - 記述編

はじめに

VDMで仕様記述・検証をするツールVDMToolsには、「清書機能」がある。これは、以下の2つのことができる。

1. 記述した仕様の自動整形
2. 仕様実行カバレッジの表示と実行/未実行の色分け

また、この清書機能を使うには、RTFを用いて仕様記述する場合と、TeXを用いて仕様記述する場合の2種類の方法がある。僕のお勧めは後者のTeX を使う方法で、理由は3つある。

1. TeX、VDM共にテキストファイルとして管理でき、バージョン管理ツールと相性が良い
2. TeXを使った方が美しい文書ができる
3. 清書機能が持つ、「自動整形」の機能はTeXでないとできない（RTFでは単に色分けとカバレッジ表が出るだけ）

なので、この記事では、TeXを使う方法を解説する。記事はいくつかに分けようと思っていて、まずはVDM+TeXでどのように記述するかを解説する。

TeX混じりのVDMを書く方法

といっても、そんなに難しいことはない。今回は簡単なテンプレートを用意したので、最低限であればテンプレートを使えば実現できる。もちろんTeXに詳しい方は、テンプレートをベースに色々カスタマイズできるだろう。
ここにVDM+TeXテンプレートがある

準備

VDM+TeXで書き始めるには、1つ準備が必要。それは、VDM用のTeXスタイルファイルをtexmfなり、texmf-localに配置すること。VDM用のスタイルファイルは、数学記号変換版と数学記号非変換版の2種類あって、数学記号非変換版は公式には公開していない。
元々、VDMToolsの清書機能は、清書した時に数学記号に変換することを前提に作られていた。しかし、数学記号が読めない僕としては、数学記号で清書されるのは迷惑だったのだ。そこで、数学記号に変換しないスタイルファイルを新たに作成した。
数学記号非変換版を公開していないのは、現状まだブラッシュアップが必要な部分があるからだ。だからと言って使えないものではなく、僕はこちらのスタイルファイルを常用している。
今回は、このスタイルファイルをこの記事に置いておく。公式にパッケージに入る or 問題が出た場合は、撤去することをご容赦ください。
※VDMTools 9.0.2で公式に導入されたので、そちらをお使いください。
VDM数学記号非変換版（vpp-nms.sty）
VDM数学記号非変換版（vdmsl-2e-nms.sty）

VDM+TeXで書く

TeX混じりのVDM仕様は大きく2つのセクションに分けて記述する。
これらのセクションは、同じファイルに記述することも可能であるが、今回はお勧めであるTeXとVDMを別ファイルとする方法をご紹介する。

TeX文書セクション（A.tex）

これは、通常のTeX文書であり、VDMToolsはここに書かれた記述については一切関知しない。例えばこのセクションにVDMを記述しても、何ら影響を与えない。
【書き方】
※コピペで円マークがおかしくなる可能性があるので、上のテンプレートファイルを使うことをお勧めします

\documentclass[a4paper,10t]{jsarticle}

\usepackage[dvipdfm]{graphicx, color}

\usepackage{color}
\usepackage{array}
\usepackage{longtable}
\usepackage{alltt}
\usepackage{graphics}
\usepackage{vpp-nms}
\usepackage{makeidx}

\usepackage{colortbl}

\usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,colorlinks,plainpages=true]{hyperref}

\definecolor{covered}{rgb}{0,0,0}      %black
\definecolor{not-covered}{rgb}{1,0,0}  %red

\renewcommand{\sf}{\sffamily \color{blue}}

\begin{document}

\input{A.vpp.tex}

\end{document}

VDM仕様セクション（A.vpp）

TeX文書セクションと反対に、ここがVDMToolsが仕様として対象にする部分。構文・型チェックや仕様実行の対象になるのはこちらのセクションだ。
以下のように、\begin{vdm_al}から\end{vdm_al}までが、VDMToolsが認識する仕様部分となる。また、最下部の\begin{rtinfo}〜\end{rtinfo}の部分は、カバレッジを以下の図のように表として出力するための記述であり、クラス名以外は定型的な書き方である。

Uploaded with Skitch!

【書き方】

\begin{vdm_al}
class A
instance variables
    a : nat := 0;

operations
    public setA : nat ==> ()
    setA(aNat) == a := aNat
    pre
        aNat < 10;
end A
\end{vdm_al}

\begin{rtinfo}
    [A]{vdm.tc}[A]
\end{rtinfo}

以上がVDM+TeXで形式仕様書を作るための書き方である。次回は、この記述したVDM仕様とTeXファイルをどのように使うかを解説する予定。