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

はじめに

前回書いた、TeX混じりでVDMを書く方法。今回は、それの続編で、形式仕様書として仕上げる部分。できることは以下の通り。

• Makefile+VDM記述+TeXファイルを使って、形式仕様書PDFを作る
• VDMToolsを用いた静的チェック＋動的チェックをし、カバレッジ情報も含めて出力する
• これらをコマンド一発で実施する

と言っても、特別なことをするわけではない。各種ファイルを用意した上でmakeを走らせ 、その中でコマンドライン版VDMToolsを使ったり、TeXのコンパイルをしているだけ。

前準備

• TeXがコンパイルできる環境を作っておく
• Macなら→mas-lab.blog：Snow Leopardの開発系インストールログ
• Windowsなら→Texのインストール法
• makeが使える環境を作っておく
• Macは標準で付いているはず
• WindowsはCygwinでインストールがお勧め
• VDMToolsをインストールしておく

Makefile

以下のMakefileを参考に、一部を変更すれば基本的にはmakeができて、PDFができるはず。

###########################
# Auto VDM -> TeX report
###########################

## Definitions
#################

# TeX commands
PLATEX = platex
MENDEX = mendex
DVIPDFM = dvipdfmx
EBB = ebb

# VDMTools command line
# これは、各自の環境でパスを変えた方が良い
VPPDE = vppde

# Output document name
# メインのTeXファイル
OUTDOC = VDMTeXTemplate
# VPP files
# vppファイル達
VPPFILES = spec.vpp specT.vpp VPPUnit.vpp io.vpp
# Test script name
# これは、インタープリタで動かすコマンドを書いたファイル
# 例えば、「new testapp().Execute()」だけを書いたファイル
TESTSCRIPT = test.script
# Image directory
# TeXの説明で画像を使う場合はこのサブディレクトリへ
IMGDIR = image

## Make
#################

# make target
all: $(OUTDOC)

$(OUTDOC): makebb vdmtex
	$(PLATEX) $(OUTDOC)
	$(MENDEX) -f -g $(OUTDOC)
	$(PLATEX) $(OUTDOC)
	$(PLATEX) $(OUTDOC)
	$(DVIPDFM) $(OUTDOC)

# run VDMTools
vdmtex:
	# Read & Syntax check
	$(VPPDE) -p -R vdm.tc $(VPPFILES)
	# Type check
	$(VPPDE) -t $(VPPFILES)
	# Run Interpreter with TESTSCRIPT
	$(VPPDE) -i -D -I -P -Q -R vdm.tc $(TESTSCRIPT) $(VPPFILES)
	# Pretty print
	$(VPPDE)  -l -r -n $(VPPFILES)

# To use the PNG file on TeX, *.bb is needed. 
makebb:
	cd $(IMGDIR); $(EBB) *.png

# Clean files. But Output document is not deleted.
clean:
	rm -rf *.aux *.log *.bbl *.blg *.dvi *.toc *.ilg *.ind
	rm -rf *.out *.vpp.tex *.idx vdm.tc
	rm -rf image/*.bb

# Clean output document
realclean: clean
	rm -rf $(OUTDOC).pdf

このMakefileを使って、「% make all」すると、以下のようなPDFができる。

Uploaded with Skitch!