本報告では，Javaによるソフトウェア開発において，クラスライブラリの仕様
を組み入れた代数的仕様を記述するための支援方法を示す．
ソフトウェアの仕様の代数的仕様による記述は，ソフトウェアの形式的意味を
与え，ソフトウェアの仕様の正当性を数学的根拠に基づき検証することができ
るようになる利点がある．そこでソフトウェアの仕様を代数的仕様を用いて記
述しJavaプログラムで実現することによりソフトウェアの開発を行うことが望
ましい．
Javaプログラムの特性として，豊富なクラスライブラリが存在する．クラスラ
イブラリを用いる事により個々のプログラムの理解がしやすくなり，プログラ
ムの再利用がしやすくなる．ソフトウェアの仕様を記述する際にはクラスライ
ブラリを意識して記述する必要がある．そこで，まずクラスの仕様を代数的仕
様で表す方法を述べ，クラスライブラリの仕様を用意する．次にこのライブラ
リの仕様を組み入れたソフトウェアの仕様を記述できるように支援する．