スコーレム標準形を用いたZ仕様の代数仕様への変換

摘要

形式仕様言語Zは高い表現力を持っているが，それによって記述された仕様を検証するためには，人間が地道に演繹規則に従って、計算しなければならない．ソフトウェアの規模が増大化し，構造が複雑化すると，もはや人手で処理することは困難である．この問題を解決するために，Zで記述された仕様（以降，Z仕様と呼ぶ）を実行可能な処理系で動作可能な記述に変換し，コンピュータ支援による検証を行なうというアプローチがいくつか提案されている．我々はZ仕様を実行可能な処理系を持つ代数仕様への変換規則と，その規則に基づいて構築した仕様の変換システムを提案してきた．従来のシステムでは，ごく限られた記述しか扱えなかった．本稿では，従来では対応できなかった，限量記号を含む論理式をスコーレム標準形を利用して等式で記述する方法を提案する．変換によって生成された代数仕様は手動による修正が必要であるが，この枠組が体系化されると，Z仕様から代数仕様への変換作業効率の向上が見込まれる．そしてZ仕様の検証がコンピュータ支援により代数仕様によって自動化されることになり，検証作業の効率化も期待できる．