研究詳細

RESEARCH

Research and Industry-Academia Collaboration

研究?産学連携

仕様の異なるXML文書間の変換言語～変換の「正しさ」の理論による保証～

概要

〇XML文書変換の正しさの検証
インターネットの世界では、ある仕様に従うXML文書から別の仕様に従うXML文書への変換が頻繁に行われます。そのような変換を記述する言語としてXSLTが有名です。しかし、XSLTで記述された変換プログラムは、仕様に関係なく変換を行うので、仕様を満たさないXML文書を生成してしまう場合があります。また、仕様は満たしていても望ましくない文書を生成したり、変換そのものが停止しないこともあります。
変換プログラムがこのようなことを起こさない、つまりプログラムが行う変換が「正しい」ことを、変換を行う前に検証できるようなXML文書変換言語を設計しています。

〇理論に基づいた言語設計
変換プログラムの正しさを保証するためには、変換の振る舞いを解析するための理論が必要になります。
ここでは、「型理論」と「項書き換え系」と呼ばれる理論をベースとして、その理論を構築し、それに基づいて言語を設計しています。また、理論に基づいて言語を設計することで、変換の正しさを保証しつつ、従来の変換言語では記述しづらいような強力な変換方法を提案することができるようになります。