(57)【要約】【課題】  本発明は、搭載システム（７）に向けられたソース・コードから変換済みコードへの変換器の検証方法に関する。【解決手段】  この方法は少なくとも、これら二つのコード（１）、（３）の作用を因数に分解する唯一のバーチャル・マシンの決定のステップと、前記ソース・コード（１）および変換済みコード（３）の各々について前記ソース・コード（１）および変換済みコード（３）内に常駐する差異を表現する前記複数の補助関数を決定するステップと、補助関数の間の対応の適切さを検証することからなるステップを含んでいて、コードの変換器の検証（２）は、この最後のステップから得られる。特にＩＣカード（７）に利用される。【選択図】図３
2012027936.tif 000002
【特許請求の範囲】
【請求項１】
所定ソース・コードから搭載システム向けの所定変換済みコードにする変換器の検証方法であって、前記ソース・コードと前記変換済みコードはバーチャル・マシンに結合され、
前記ソース・コード（１）と前記変換済みコード（３）のそれぞれについて、これら２つのコード（１，３）の作用を因数分解する唯一のバーチャル・マシンを構成する共通の第１部分集合（１３）を決定するステップと、
前記唯一のバーチャル・マシンにより使用される複数の所定補助関数（１０i−３０i）で構成され、前記補助関数（１０i−３０i）が前記ソース・コード（１）および前記変換済みコード（３）内の常駐差異を表現する第２部分集合（１０，３０）を、前記ソース・コード（１）と前記変換済みコード（３）のそれぞれについて、決定するステップと、
前記ソース・コード（１）に結合された前記第２部分集合（１０）に属する各ペアの第１補助関数（１０i）と、前記変換済みコード（３）に結合された前記第２部分集合（３０）に属する各ペアの第２補助関数（３０i）を、前記補助関数のペアごとに結合するステップと、
前記全てのペアの前記補助関数（１０i−３０i）の間で決定される対応の特性を検証（６）するステップと、
前記コンバータ（２）によるソース・コード（１）から変換済みコード（３）への前記変換は前記決定される対応の特性を満足することを検証するステップを、少なくとも含んでいることを特徴とする前記検証方法。
【請求項２】
前記対応の特性が論理的関係であって、前記各ペアの前記補助関数（１０i−３０i）がそれらの実行のときに前記関係論理によって結ばれた結果を生成するようになっており、またこの関係が、前記ソース・コードと前記変換済みコードの各々の前記観察可能な実体について同一関係であるという点において、補助関数の全てのペアについて、前記変換のときに前記ソース・コード（１）の相関関係が変換済み関数（３）のなかに保存されるようになっていて、コード変換器（２）の前記検証が実現されることを特徴とする請求項１記載の方法。
【請求項３】
コード変換器（２）がソース・コード（１）から変換済みコード（３）を生成し、この変換済みコード（３）は、ＩＣカード（７）の記憶手段（７１）の中に登録されるように定められている請求項１または請求項２による検証方法のアプリケーション。
【請求項４】
前記変換済みコードは特定情報言語のバーチャル・マシン内に書かれたプログラムであって、前記ＩＣカード（７）がこの変換済みコード（３）で書かれた複数のアプリケーション・ソフトウェア（ＡlないしＡn）を登録したＩＣカードであることを特徴とする、請求項３記載のアプリケーション。
【請求項５】
前記ソース・コード（１）が「ＪＡＶＡ」（登録商標）言語のバーチャル・マシン内に書かれたプログラムであり、前記変換済みコード（３）が「ＪＡＶＡ  ＣＡＲＤ」（登録商標）言語のバーチャル・マシン内にかかれたプログラムであることを特徴とする請求項３または請求項４記載のアプリケーション。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、搭載されたシステムのコードの変換器を検証する方法に関する。
【０００２】
本発明はまた、ＩＣカード向けのコードを生成するための変換器へそうした方法を適用することにも関する。
【０００３】
本発明の範囲内で、「搭載（された）システム」という用語は最も一般的な意味で考慮されるべきである。それは特にＩＣカードへ向けられたシステムに関し、ＩＣカードは本発明の好ましい実施例を構成するが、しかし情報データ処理の適当な手段を有する携帯用または移動用の装置へ向けられた全てのシステムに同様に関係し、それらを以下に「処理のリソース」と呼ぶことにする。
【背景技術】
【０００４】
データ処理のリソースを備えたモデム搭載システムは、ますます複雑でますます多数の機能を遂行できるようになっている。しかしながら、技術市場への投資とますます効率的な構成部品にもかかわらず、搭載システムの顕著な特性は、通常の情報システム（マイクロ・コンピュータ、ワーク・ステーションなど）に関して、それらがリソースの材料に課する制約（特に記憶容量とマイクロプロセッサの能力）に関係する。これらの制約を満足するために、搭載システム上で実行するためのコードを変換することが必要である。この変換の目的は、リソースにおいて一層効率的で一層経済的なコードを生成することである。
【０００５】
思想を固定して、コードの非限定的な例とするために、「ＪＡＶＡ（登録商標）」（ＳＵＮ  ＭＩＣＲＯＳＹＳＴＥＭＳ社の登録商標）言語のバーチャル・マシン内に書かれたプログラムに従って考察するが、これは多数の環境内で実行できる有利さを提示する。この言語のアプリケーションの領域は特にインターネット回路網の重要な展開によって、実際に増殖した。「ａｐｐｌｅｔｓ」と呼ばれる小さな記憶容量の論理的利用の多くが、この言語で書かれていて、「ＷＥＢ」タイプのナビゲータによって実行できる。
【０００６】
同様に本発明の好ましい利用の一つとして、ＩＣカードの固有の情報リソースによってこのタイプのコードを実行することがある。上述のように、重要な技術進歩にもかかわらず、ＩＣカードのメモリ容量は、それが装備するマイクロプロセッサの能力と同様に、比較的に限定されている。同様に重要なのは、ＩＣカード内にコードが常駐することであって、なぜならＩＣカードとホスト端末機の間の伝送は、それがどんなものであっても、実行速度が遅いからである。実際の規格は、直列タイプの伝送しか用意していない。従って、この用途のために最適化する全ての場合において「軽量化」できるコードで処理する必要が感じられる。これをするために、「ＪＡＶＡ」から派生した言語で、「ＪＡＶＡ」の制限の形で現れるもの、すなわち「ＪＡＶＡ  ＣＡＲＤ」（同様にＳＵＮ  ＭＩＣＲＯＳＹＳＴＥＭＳ社の登録商標）を使用することが提案された。
【０００７】
搭載システムは一般に事実の信頼性と同時にセキュリティについて最も高度な保証を要求する環境で使用されるという事実から、複雑な補足的機構が生じる。ＩＣカードの新バージョンの例として、調和的に協働すべき複数の論理アプリケーションを、機密情報を明らかにせずにＩＣカード上に設立することを希望できるものを挙げることができよう。実際アプリオリに、これらの複数のアプリケーションは、異なったユーザに関するものであり得る。前記の協働にもかかわらず、厳格な仕切りを保って、所与のユーザに関する情報が機密のままであり、資格のないユーザがそれらを知る（読取り）こと、および／または操作する（書込みおよび連関した作業：消去、修正）ことが少しでも可能でないようにする。「機密性」の面のほかに、他の要求が考慮に入れられ、特にいわゆる「完全性」：データの消失、不一致の修正などの要求を考慮に入れられる。
【０００８】
「初期コード」の意味で「ソース」コードを考慮するならば、たとえば前記「ＪＡＶＡ」言語の「バイト・コード」のように初期コードは必要な全ての保証を提供し前記の諸要求を満足するが、この「バイト・コード」は「ＪＡＶＡ」言語のバーチャル・マシン内に書かれるプログラムである。長期間にわたり実際多数のテストが実行を可能にしてきた。
【０００９】
前記「変換済み」コードは、コード変換器を使って「ソース・コード」から得られ、コード変換器は一般に搭載システムの外部にあるが、しかし同様にその内部にも常駐し得る。したがってソース・コードと変換済みコードの間では等価であることを示すことが必要である。
【００１０】
このことはコードに実施された変換が（外部の観点において）どの点でもその作用を変えないということと、セキュリティの欠陥が導入されないことを保証されることにより実施される。言いかえれば（変換前の）初期コードは論理の観点から（変換後の）結果のコードと等価な物でなければならない。
【００１１】
変換はコードと操作されるデータの表現に上にグローバルな効果を有するので、この特性を一般的に保証することはとくに困難である。実際のやり方では、この作業により課される複雑性のために、経済的な条件および／または実際的な技法において実施することができない。他方において、こうした必要は非常に最近まで現れなかったことを理解すべきであり、とくにマルチ・アプリケーションおよび／またはマルチ・ユーザのＩＣカードの前記の技術開発に結びついて現れたものであることを理解すべきである。
【発明の概要】
【発明が解決しようとする課題】
【００１２】
本発明はこの必要に対して、極端に長くかつ高価な手順を必要とすることなく応答することを目指す。
【課題を解決するための手段】
【００１３】
本発明による方法は、コードの変換の訂正を組織的でモジュール的な仕方で検証することを可能にする。
【００１４】
この発明の範囲内で、それ自体よく知られた二つのフォルマリスムが本質的な仕方で使用される。それは操作的意味論と論理関係論である。これらのフォルマリスムの一層詳細な記述については、第１にＨ．Ｒ．Ｎｉｅｌｓｏｎ、およびＦ．Ｎｉｅｌｓｏｎ著「意味論とその応用：正式な紹介」Ｗｉｌｅｙ、１９９２年および第２にＭｉｔｃｈｅｌｌ著、「プログラミング言語の基礎」ＭＩＴプレス、１９９６年に出ているのが有益である。
【００１５】
本発明の本質的特徴によれば、コード変換器の検証方法は、「補助関数」と呼ばれる諸関数によりパラメータ表現された共通の一つのバーチャル・マシーンを使って二つのコードの意味を明示することからなる。二つのコードの相違は、前記補助関数で表現され再グループ化される。各補助関数は二つのバージョンを有し、それはソース・コード内のバージョンと変換済みコード内のバージョンである。最初のモジュールは二つのコードについて共通であるから同一であり、それらが等価ならば検証は行なわれない。二つのコードの等価を示すには前記補助関数が二つずつ等価であることが示されれば充分である。これら二つの部分集合は、ソース・コードと変換済みコードの二つの全体において考えて表現した二つの集合よりもはるかに複雑さを少なくすることができる。本発明によれば検証処理に固有の困難さは非常に減少されることになり、相関的な方法により検証のプロセスが経済的で技術的に実現可能なものになる。
【００１６】
本発明のひとつの目的は、所定ソース・コードから搭載システム向けの所定変換済みコードにする変換器の検証方法であって、前記ソース・コードと前記変換済みコードはバーチャル・マシンに結合され、
前記ソース・コードと前記変換済みコードのそれぞれについて、これら２つのコードの作用を因数分解する唯一のバーチャル・マシンを構成する共通の第１部分集合を決定するステップと、
複数の所定補助関数で構成され、前記補助関数が前記ソース・コードおよび前記変換済みコード内の常駐差異を表現する第２部分集合を、前記ソース・コードと前記変換済みコードのそれぞれについて、決定するステップと、
前記ソース・コードに結合された前記第２部分集合に属する各ペアの第１補助関数と、前記変換済みコードに結合された前記第２部分集合に属する各ペアの第２補助関数を、前記補助関数のペアごとに結合するステップと、
前記全てのペアの前記補助関数の間で決定される対応の特性を検証するステップと、前記コンバータによるソース・コードから変換済みコードへの前記変換は前記決定される対応の特性を満足することを検証するステップを、少なくとも含んでいることを特徴とする前記検証方法である。
【００１７】
本発明の更なる目的は、ＩＣカード内に登録されるためのコードの生成のための変換器のこのような方法の利用である。
【００１８】
添付図面を参照しながら本発明を詳細に説明する。
【図面の簡単な説明】
【００１９】
【図１】ソース・コードから最終変換済みコードへの変換のプロセスを図式的に示す。
【図２Ａ】本発明による方法の本質的な特性の一つを図式的に示す。
【図２Ｂ】本発明による方法の本質的な特性の一つを図式的に示す。
【図３】ＩＣカード上の本発明による方法の適用を図式的に示す。
【発明を実施するための形態】
【００２０】
本発明によるコードの変換器の検証方法をこれから一層詳細な仕方で説明する。
【００２１】
図１は、最初または起源のコードという意味で、「ソース・コード」と呼ばれるコード１から、コード２の変換器を使って「変換済みコード」と呼ばれる最終コード３へ変換する処理を図式的に示す。この変換器はおそらく情報手段または一つの特定ソフトウェアである。従来の方法で変換済みコードは（実線の中の）搭載システム４の中に常駐するように定められている。変換器２も同様に（点線内の）参照番号４’の搭載システム内に常駐またはダウンロードされ得る。
【００２２】
搭載システム４−４’内にローディングまたは記録の後に、変換済みコードは唯一の参照番号５で表現された必要なだけの一つまたはいくつかのタスクの実行を可能にする。搭載システム４が普通の自動的な情報資源（図示なし）を有するものと仮定する。
【００２３】
アプリオリにコードの変換は全部で一回だけで所与の変換器により、またはまれな機会すなわちたとえばオリジナルコード、またはソース・コード１のバージョンの更新において実行される。
【００２４】
したがって変換済みコード３がソース・コード１に等価であることの正式な証明を確立できることが必要である。もし変換器２が正しい仕方で機能すればこのプロセスが検証を可能にする。
【００２５】
しかしながらすでに想起したように、全体としてソース・コードと変換済みコードにより形成された二つの集合を考えるならば、このような決定が一般的に実際的なやり方では理論的に不可能であることが証明される。
【００２６】
本発明による方法の本質的な特徴は結局、二つのコードの各々について二つの集合、すなわち第１部分集合と第２部分集合を見出すことで構成されることになる。本発明の方法の重要な特徴によれば、第１部分集合はソース・コードと変換済みコードの二つのコードに共通のバーチャル・マシンを形成する。この事実により、第１部分集合の等価なことを検証することは不必要である。
【００２７】
補助関数で構成される第２部分集合は、反対に一つのコードと他のコードを区別する。ソース・コードと変換済みコードが等価であること決定は、このとき第２部分集合の補助関数のペアが全て等価であることの決定になる。こうして補助関数に常駐する複雑性を大きく減少し得る。結局等価であることの正確な決定が可能になる。
【００２８】
図２Ａと図２Ｂは本発明による方法を非常に図式的に示す。
【００２９】
図２Ａが一層詳細に示すように、ソース・コード１および変換済みコード３の第１部分集合が一つの共通のバーチャル・マシン１３を形成する。第２部分集合１０と同３０はそれぞれ一連の前記補助関数により構成され、それらが等価であることは認証されるようになる。これらの補助関数１０と同３０は共通のバーチャル・マシン１３をパラメータ表現する。
【００３０】
ソース・コード１と変換済みコード２の二つのコードの等価であることは、二つずつ取った補助関数１０と同３０の等価であることを検証することになるが、これは図２Ｂに関して後に示す。
【００３１】
これから処理のステップを一層詳細な仕方で説明する。
【００３２】
ソース・コードと変換済みコードが、それぞれ前記第１バーチャル・マシンおよび第２バーチャル・マシンに結合される。
【００３３】
第１ステップはソース・コードと変換済みコードの内容を因数分解できる唯一のバーチャル・マシン（すなわち操作的意味論）の定義で構成される。二つのコードの間の差異は、そのとき、二つのコードの中で異なって解釈されるかまたは作動される補助関数を通して現れる。
【００３４】
バーチャル・マシンは、下記の規則の集合により表現できる。
【数１】
2012027936.tif 000003
【００３５】
諸前提（ｐｒｅｍｉｓｓｅｓ）は、ある規則の適用条件、すなわちブール代数式でも、状態変化を表現するために使用される変数への数の代入でもある。状態の情報を引き出したり条件を表現したりするために、諸前提が補助関数の助けを求める。諸前提が検証されて命令「Ｉｎｓｔｒｕｃｔｉｏｎ１」が見出されたときに、マシンの状態がどのように展開するかを、各規則が指示する。コードの命令の各タイプについて、この形式の規則を１つまたはいくつか定義される。
【００３６】
第２のステップは、２つのコードの中に使用されるデータのタイプまたは構造の定義からなる。基本的なタイプを例えば次のように定義できる。
【数２】
2012027936.tif 000004
そしていくつかのタイプは例えば次のように構成される。
【数３】
2012027936.tif 000005
【００３７】
第３のステップは、θで参照され、諸バーチャル・マシンに使用されている諸タイプの解釈からなる。各タイプθについてソース・コードについての解釈
【数４】
2012027936.tif 000006
と、変換済みコードについての解釈
【数５】
2012027936.tif 000007
と、２つの解釈
【数６】
2012027936.tif 000008
の間の関係
【数７】
2012027936.tif 000009
について１つの解釈が定義される。これらの関係は論理的関係と呼ばれて、諸タイプの構造を満足する。単純なタイプについては、それらは明示的に定義され、構造化されたタイプについては、それらは構造の構成要素から推論される。
【００３８】
例えば、下記の諸ペアについて、
【数８】
2012027936.tif 000010
これらの関係で、θ１とθ２はタイプであり、またａ、ｂ、ａ’、ｂ’はタイプの要素である。
【００３９】
同様に諸関数について、
【数９】
2012027936.tif 000011
【００４０】
論理的諸関係が観察可能な諸タイプについて「同定される」関係であるはずであり、すなわち、２つのコードが同じ結果になることが望ましい。印刷可能なタイプおよび／または情報ディスプレイに表示可能なタイプが習慣的に問題になっている。問題になるのは基本的なタイプであろうが、しかし例えばスタックすなわち所与のプログラムの諸変数を表現する構造化されたタイプも問題であろう。
【００４１】
第４のステップはバーチャル・マシン内で使用される補助関数の解釈からなる。各補助関数ｆについて、
【数１０】
2012027936.tif 000012
と記されるソース・コードについての解釈と、
【数１１】
2012027936.tif 000013
と記される変換済みコードについての解釈が与えられる。
【００４２】
等価の決定は、補助関数の定義が論理的関係を満足することを示すことからなる。一層正確には、各補助関数ｆ：θ→θ’について、下記のように示される。
【数１２】
2012027936.tif 000014
【００４３】
２つのバーチャル・マシンは下記の関係にあることになる。
【数１３】
2012027936.tif 000015
【００４４】
観察可能な諸タイプについて関係が同定されるように、ソース・コードと変換済みコードが対話的に同定される。
【００４５】
最後のステップは、論理的関係を満足する変換器Γ（図１：２）が存在することを示すことから構成される。それは、Γ：Ｓ→Ｔがその論証のタイプに連合した論理的関係を、ソース・コードＳ（図１：１）と変換済みコードＴ（図１：３）によって満足することを検証することで為される。それを行なうには、下記の関係に従うことが必要である。
【数１４】
2012027936.tif 000016
【００４６】
論理的関係が制約の集合を明示することが今や示された、従って、変換器２を図面によって、洗練と抽出の技法を適用して、適当な証明の助けを求めながら、正しく読み取ることができる。
【００４７】
したがって本発明による方法は、検証のプロセスの大きな機械化を可能にするので重要な利点を提供し、特にこの検証が複雑さの一層少ない部分集合上で行われるので、それを良好に実行することができる。
【００４８】
ソース・コード１の変換は一層簡単な変換の連続のように書かれ得るが、この方法は各変換を独立に示すために応用され得る。結局それはモジュール化の大きな利点を提供する。
【００４９】
図２Ｂに示すように物理的装置または論理的装置である装置６の助けを借りて、補助機能１０と同３０の部分集合上だけで、検証を実行できる。ｎ個の補助関数が存在して、それぞれ１０a、１０b...、１０i...、１０n-1、１０nおよび２０a、２０b...、２０i...、２０n-1、２０nと参照されるものと仮定する。装置６が物理的装置であれば、検証回路６０a、６０b...、６０i...、６０n-1、6０n（コンバータの記号により図２Ｂに任意に表現される）と同様に、たとえば関数１０iおよび３０iのペアのための検証回路６０iのように検証のための補助関数のペアを含む。この装置６の出力または諸出力を一つの参照記号６１で示すが、ソース・コード１および変換済みコード３に対応する補助関数の全ての可能なペアの中の論理的関係が満足されることを指示する。この一連の操作は、二つのコードの等価の正式な証明を、そのグローバル性においてもたらすのに充分である。
【００５０】
注意すべきは、本発明による方法はアポステリオリすなわち既存の変換器を検証するために同様に、アプリオリに新しい変換器の開発の援助として使用できる。特にこれは後者の場合に、正しく機能するための、言いかえればこの変換器によってソース・コードから生成される変換済みコードが前記の等価の要求を満足するための、その特性を決定することができる。
【００５１】
これからＩＣカードの範囲内で説明する。図３は、ＩＣカード７のアーキテクチャを図式的に示す。この図には本発明による方法を良く理解するために必要な要素のみを示している。
【００５２】
ＩＣカード７は特に、外部世界との通信を可能にする入出力装置７０、固定またはプログラム可能の（「ＲＯＭ」、「ＰＲＯＭ」、「ＥＰＲＯＭ」、または「ＥＥＰＲＯＭ」タイプの）１次メモリ装置７１、およびランダム・アクセス・メモリ装置７２を含んでいる。ＩＣカード７はまたバスを介してＩＣカード７の他の構成要素と対話するマイクロプロセッサまたはマイクロコントローラ７３を含んでいる。
【００５３】
このようなＩＣカード７の論理的アーキテクチャはＩＳＯ規格７８１６−３に従って、プロトコル層によって翻訳されて入出力装置７０に結合された最下層につながり、さらにＩＣカード内に登録された論理アプリケーションに結合した最上層につながっている。これらの規格は伝送が直列モードで実行されることを予想している。
【００５４】
ソース・コード１は変換器によってコード２へ変換されると、ＩＣカード７へ伝送されてそこへ登録されるが、一般に入出力装置７０を介して固定または「半固定の」メモリ装置７１内に登録される。ＩＣカード７により取扱われる単数または複数の論理アプリケーションはＩＣカード７内、すなわちメモリ装置７１内に常駐として登録されるか、またはランダム・アクセス・メモリ７２内に一時的な仕方で登録され得る。後者の場合はアプリケーションは入出力装置７０を介して通信回線によってロードされる。説明している例ではＩＣカード７がマルチ・アプリケーション・タイプであって、そのうえマルチ・ユーザのタイプであると仮定している。したがってＩＣカード７はｍ個の論理アプリケーションを取扱い、Ａ1ないしＡmは変換された言語３で記述される。
【００５５】
ＩＣカードのために現在使用されている言語の一つは「Ｊａｖａ  Ｃａｒｄ」と呼ばれてきた。それはＩＣカードのプログラム作成の専用の言語であって、言語「Ｊａｖａ（登録商標）」の制約によって構成される。
【００５６】
同様にＩＣカード７はコードの諸部分にローディングを現場で変換するように働く補助コンバータをストックすることができる。
【００５７】
本発明による方法の諸ステップを一般的な範囲において以下に説明するが、この好ましいアプリケーションの範囲以内で特に詳しく例示する。
【００５８】
知られているように言語「Ｊａｖａ  Ｃａｒｄ」の設立は、ファイル「ＣＡＰ」内の「ｄｅ  Ｃｌａｓｓｅｓ」と呼ばれるファイルを変換するコンバータによってコンバータを呼び出す。クラスの一つのファイルは、コンパイルの単位でありまたプログラム「Ｊａｖａ」のオブジェクトコードの表現である。ファイルＣＡＰは同一の「ｐａｃｋａｇｅ  Ｊａｖａ  Ｃａｒｄ」の全てのクラスを再グループして、唯一の「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」しか含まない。「ｐａｃｋａｇｅ  Ｊａｖａ  Ｃａｒｄ」はクラスを再グループして、名称の種類を創設するための「Ｊａｖａ」構成である。「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」の役割はテーブルであって、「Ｊａｖａ」のためのクラスの各ファイルに結合されたテーブルであり、また「Ｊａｖａ  Ｃａｒｄ」のために各ファイル「ＣＡＰ」に結合されたテーブルである。このテーブルは定数（文字、実体などのストリング）を再グループする。それは「Ｊａｖａ」と「Ｊａｖａ  Ｃａｒｄ」のバーチャル・マシン内で使用される。変換はトリビアルでなくグローバルである。すなわちそれは「トークン」と呼ばれる実体、すなわち全部で７または８ビットの数字により、全ての「パッケージ、クラス、フィールド、方法の」名称を取りかえる。これらの「トークン」はテーブルにアクセスするための索引の役をする。そのうえ変換はファイル「ＣＡＰ」内の同一のパッケージのクラスの全てのファイルを、（「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」の併合と方法のテーブルの再組織化によって）再グループする。
【００５９】
言語「Ｊａｖａ  Ｃａｒｄ」は特に銀行用ＩＣカード上で使用されるのを目的としている。したがって、言語「Ｊａｖａ」のバーチャル・マシン内に書かれたプログラム（すなわち「バイト・コード」）から言語「Ｊａｖａ  Ｃａｒｄ」のバーチャル・マシン内に書かれたプログラムへの変換の修正を検証すること、すなわちこれら二つのプログラムの等価の証明をもたらすことが非常に重要である。
【００６０】
この正式な証明は、本発明による方法の諸ステップを実行することによりもたらされる。
【００６１】
第１のステップは操作的意味論の定義からなる。
【００６２】
「バイト・コード」の各命令に一つまたは複数の意味論的規則が結合される。「バイト・コード」はポータブルなアセンブラ・コードである。それは、バーチャル・マシン「Ｊａｖａ」または「Ｊａｖａ  Ｃａｒｄ」のためのオブジェクト・コードである。たとえばこのコードの命令の一つに結合された意味論的規則である命令「ｇｅｔｆｉｅｌｄ」は下記のように記述される。
【数１５】
2012027936.tif 000017
【００６３】
例において状態は、最初にカレントな命令（ｇｅｔｆｉｅｌｄ  ｉ；ｂｃ）と共に実行されるコード、オペランドのスタック（ｒ：：ｏｐｓ）、ローカル変数（ｌ）、カレントのクラスの参照（ｃ）およびスタック（ｈ）から構成される。ｇｅｔｆｉｅｌｄ  ｉの実行時に実行される操作を規則が規定する。
−  補助関数「ｃｏｎｓｔａｎｔ＿ｐｏｏｌ」はインデックスｉを使用するが、これは該当する「ｃｏｎｓｔａｎｔ＿ｐｏｏｌ」内のフィールド（ソース・コードまたは変換済みコードがそれによって動かされる署名または「トークン」）の参照ｆ＿ｒｅｆを得るためである。
−  参照τはオブジェクトを示し、それはスタック（ｓｔａｃｋ）の頂上で読まれて読み出されるべき領域のオブジェクトである。この参照により、ヒープ（ｈｅａｐ）（ｈ（ｒ））の中にｃ＿ｒｅｆ（それによってソース・コードまたは変換済みコードが動かされる資格ある名称またはトークンのペア）の動的クラスおよびオブジェクト（ｉｖ）のフィールドのリストを発見することができる。
−  あらかじめ計算された参照とフィールドのリストを使用することによりフィールドが、（ｖ：＝ｉｖ（ｆ＿ｒｅｆ））と読まれる。
−  命令ｇｅｔｆｉｅｌｄはフィールドの値によってオブジェクトの参照を置換えて状態を変更して、コード（ｂｃ）の続きにより実行が継続される。
【００６４】
第２のステップはタイプの定義により構成される。
【００６５】
「Ｊａｖａ  Ｃａｒｄ」言語の場合は貯蔵場所の統一を表現するためにタイプＷｏｒｄを定義する。
【数１６】
2012027936.tif 000018
【００６６】
構築されるタイプの例としてｃｏｎｓｔａｎｔ  ｐｏｏｌのタイプは下記の通りである。
【数１７】
2012027936.tif 000019
これと共に
【数１８】
2012027936.tif 000020
【００６７】
例において「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」はインデックス（ＣＰ＿ｉｎｄｅｘは基本的と考えられる）を取り、また入力（ここでは一つのクラス、一つの方法、または一つのフィールドへの参照）を返す関数と見られる。
【００６８】
「ｂｙｔｅ  ｃｏｄｅ」のタイプは、下記の通りである。
【数１９】
2012027936.tif 000021
【００６９】
「ｂｙｔｅ  ｃｏｄｅ」は命令のシーケンスである。タイプＩｎｓｔｒｕｃｔｉｏｎは、「Ｊａｖａ  Ｃａｒｄ」の「ｂｙｔｅ  ｃｏｄｅ」内に使用される全ての命令を列挙する。
【００７０】
第３ステップは諸タイプの解釈からなる。
【００７１】
「Ｊａｖａ  Ｃａｒｄ」の場合において、ソース・コードについての解釈は、（名称を使用する）クラスのファイルの形式のもとに
【数２０】
2012027936.tif 000022
と記され、（「ｔｏｋｅｎｓ」を使用する）ファイルＣＡＰの形式のもとに変換されたコードについての解釈は
【数２１】
2012027936.tif 000023
と記される。
【００７２】
例としてタイプ
【数２２】
2012027936.tif 000024
は、下記の通りソース・コードについて検証される。
【数２３】
2012027936.tif 000025
【００７３】
名称の基礎へのモデルにおいて、「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」はクラスの名称（参照される「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」を指示するため）および一つのｉｎｄｅｘの名称からなる。
【００７４】
タイプ
【数２４】
2012027936.tif 000026
は、下記の通り変換済みコードについて検証される。
【数２５】
2012027936.tif 000027
【００７５】
「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」のインデックスは「ｐａｃｋａｇｅ」の「ｔｏｋｅｎ」（説明する例においては、「ｐａｃｋａｇｅ」またはファイルＣＡＰごとに唯一の「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」が存在する）および一つのインデックスにより構成される。
【００７６】
関係Ｒcp＿ｉｎｄｅｘは、下記の式（１６）のような全単射として定義される。
【数２６】
2012027936.tif 000028
【００７７】
名称の基礎へのモデル内で参照される「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」を含むクラスの「ｐａｃｋａｇｅ」の名称は、「ｔｏｋｅｎｓ」をベースとするモデル内で参照される「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」を含む「ｐａｃｋａｇｅ」の「ｔｏｋｅｎ」と関係があるはずである。ｉｎｄｅｘ  ｉおよびｉ’上の唯一の制約は、Ｒcp_indexが全単射であるべきことだけである。（したがって「ｃｏｎｓｔａｎｔ  ｐｏｏｌｓ」の入力は再グループされ、再配列され得る）。
【００７８】
第４ステップは補助関数の解釈で構成される。
【００７９】
たとえば名称の基礎へのモデルについての補助関数「ｃｏｎｓｔａｎｔ＿ｐｏｏｌ」のバージョンは、下記の通りである。
【数２７】
2012027936.tif 000029
これと共に
【数２８】
2012027936.tif 000030
【００８０】
関数ｐａｃｋ＿ｎａｍｅはクラスの名称を取って「ｐａｃｋａｇｅ」の名称を介し、また関数ｅｎｖ＿ｎａｍｅはパッケージの名称とクラスの名称を取って、指定されたクラスのファイルを表現する構造を、クラスの階層の中に発見する。ｃｏｎｓｔａｎｔ  ｐｏｏｌはクラスのファイルから抽出される。
【００８１】
「ｔｏｋｅｎｓ」をベースとするモデルについて、補助関数のバージョンは
【数２９】
2012027936.tif 000031
は、下記の通りである。
【数３０】
2012027936.tif 000032
これと共に
【数３１】
2012027936.tif 000033
【００８２】
「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」は関数ｅｎｖ＿ｔｏｋとパッケージのｔｏｋｅｎを使って環境（すなわちファイルＣＡＰ）内に発見される。
【００８３】
第５のステップは、補助関数が論理的関係を尊重することの証明からなる。
【００８４】
もし「ｃｏｎｓｔａｎｔ  ｐｏｏｌ」へのアクセスの関数の例が新しく参照されるならば下記の通り決定することが必要である。
【数３２】
2012027936.tif 000034
【００８５】
【数３３】
2012027936.tif 000035
は関係Ｒcp_indexと関係Ｒcp_infoの関数で完全に定義される。この定義を使用して下記のように検証するのに充分であることが示される。
【数３４】
2012027936.tif 000036
これにともに
【数３５】
2012027936.tif 000037
【００８６】
証明はＲcp_infoおよび下の式（２４）から想起される特性に基く。
【数３６】
2012027936.tif 000038
【００８７】
この方法の最後の第６ステップは、このコンバータによるコードとデータの変換が、決定された論理的関係を尊重するように変換器を決定することからなる。たとえば「ｐａｃｋａｇｅｓ」への参照は、モデルによって名称であったり「ｔｏｋｅｎｅｓ」であったりする。Ｒpackage_refに結合した論理的関係は「ｐａｃｋａｇｅ」の名称と「ｐａｃｋａｇｅ」の「ｔｏｋｅｎｓ」の間の全単射のように定義される。「ｔｏｋｅｎｓ」内のパッケージの名称の変換を実現するコンバータの関数が実際に全単射であることを検証するだけで充分である。
【００８８】
以上のことを読めば本発明が定めた目的を本発明が充分に達成することを容易に認められる。
【００８９】
しかしながらとくに図２と図３に関して明示的に説明した実施例だけに本発明を限定すべきではない。
【００９０】
最後に、ＩＣカードまたは類似のタイプのアプリケーションのためにとくに関係がある言語「Ｊａｖａ  Ｃａｒｄ」のバーチャル・マシンのプログラムにおける言語「Ｊａｖａ」のバーチャル・マシンのプログラムの変換の場合についての詳細の仕方でこの方法を説明してきたが、本発明はいかなる場合もこの特別なアプリケーションに限定されない。
【００９１】
含まれる装置が比較的に限定された情報資源しか処理しない場合のたびに、本発明を応用することができ、特にＲＡＭまたはＲＯＭのメモリ容量および／または使用されるプロセッサの計算能力が比較的限定される場合には本発明を利用することができる。例としては電子的な書物、たとえばインターネット・サイトの出所のデータを送信し貯蔵するためのいわゆる「ｅ−ｂｏｏｋ」、たとえばいわゆる「ｏｒｇａｎｉｓｅｒ」タイプのポケット電卓、インターネット・ネットワークに接続できるある種の移動電話などを例としてあげることができる。これら全ての場合において総合情報資源をより良く使用するためには最適な言語で処理する必要がある。
【図１】
2012027936.tif 000039
【図２Ａ】
2012027936.tif 000040
【図２Ｂ】
2012027936.tif 000041
【図３】
2012027936.tif 000042
【手続補正書】
【提出日】平成23年9月26日(2011.9.26)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
ソース・コードから搭載システム向けの変換済みコードにする変換器の検証方法であって、前記ソース・コードと前記変換済みコードはバーチャル・マシンに関連付けられ、
前記ソース・コードと前記変換済みコードのそれぞれについて、２つのコードに共通し及びバーチャル・マシンを構成する第１部分集合を決定するステップと、
前記ソース・コードと前記変換済みコードのそれぞれについて、前記単一のバーチャル・マシンにより使用される複数の補助関数で構成され、前記ソース・コードおよび前記変換済みコードの間の残存する差異を表わす、第２部分集合を決定するステップと、
前記補助関数をペアに関連付けるステップであって、各ペアの第１補助関数は前記ソース・コードに関連する前記第２部分集合に属し、各ペアの第２補助関数は前記変換済みコードに関連する前記第２部分集合に属する、ステップと、
前記全てのペアの前記補助関数の間で所定の対応の特性を検証するステップであって、前記対応の特性が論理的関係であり、前記各ペアの前記補助関数が、実行されたときに、前記関係論理によって結ばれた結果を生成する、前記ステップと、
ソース・コードから変換済みコードへの前記変換が前記所定の対応の特性を満足することを検証するステップを、少なくとも含んでいることを特徴とする前記検証方法。
【請求項２】
この関係が、補助関数の全てのペアについて、前記ソース・コードと前記変換済みコードの各々の観察可能な実体について恒等関係であり、その結果、前記変換のときに、前記ソース・コードの機能が前記変換済みコードのなかに維持され、コード変換器の前記検証が実行されることを特徴とする請求項１記載の方法。
【請求項３】
コード変換器が前記ソース・コードから変換済みコードを生成し、この変換済みコードは、ＩＣカードの記憶手段の中に格納されるように定められている請求項１または請求項２による検証方法のアプリケーション。
【請求項４】
前記変換済みコードは所定のコンピュータ言語のバーチャル・マシンで書かれたプログラムであって、前記ＩＣカードがこの変換済みコードで書かれた複数のアプリケーション・ソフトウェアを格納したＩＣカードであることを特徴とする、請求項３記載のアプリケーション。
【請求項５】
前記ソース・コードが「ＪＡＶＡ」（登録商標）バーチャル・マシンで書かれたプログラムであり、前記変換済みコードが「ＪＡＶＡ  ＣＡＲＤ」（登録商標）バーチャル・マシンで書かれたプログラムであることを特徴とする請求項３または請求項４記載のアプリケーション。