"所定ソースコードから搭載システム向けの所定変換済みコードにする変換器の検証方法であって、前記ソースコードと前記変換済みコードはバーチャルマシンに結合され、前記ソースコード1と前記変換済みコード3のそれぞれについて、これら2つのコード1,3の作用を因数分解する唯一のバーチャルマシンを構成する共通の第1部分集合13を決定するステップと、前記唯一のバーチャルマシンにより使用される複数の所定補助関数10i-30iで構成され、前記補助関数10i-30iが前記ソースコード1および前記変換済みコード3内の常駐差異を表現する第2部分集合10,30を、前記ソースコード1と前記変換済みコード3のそれぞれについて、決定するステップと、前記ソースコード1に結合された前記第2部分集合10に属する各ペアの第1補助関数10iと、前記変換済みコード3に結合された前記第2部分集合30に属する各ペアの第2補助関数30iを、前記補助関数のペアごとに結合するステップと、前記全てのペアの前記補助関数10i-30iの間で決定される対応の特性を検証6するステップと、前記コンバータ2によるソースコード1から変換済みコード3への前記変換は前記決定される対応の特性を満足することを検証するステップを、少なくとも含んでいることを特徴とする前記検証方法。前記対応の特性が論理的関係であって、前記各ペアの前記補助関数10i-30iがそれらの実行のときに前記関係論理によって結ばれた結果を生成するようになっており、またこの関係が、前記ソースコードと前記変換済みコードの各々の前記観察可能な実体について同一関係であるという点において、補助関数の全てのペアについて、前記変換のときに前記ソースコード1の相関関係が変換済み関数3のなかに保存されるようになっていて、コード変換器2の前記検証が実現されることを特徴とする請求項1記載の方法。コード変換器2がソースコード1から変換済みコード3を生成し、この変換済みコード3は、ICカード7の記憶手段71の中に登録されるように定められている請求項1または請求項2による検証方法のアプリケーション。前記変換済みコードは特定情報言語のバーチャルマシン内に書かれたプログラムであって、前記ICカード7がこの変換済みコード3で書かれた複数のアプリケーションソフトウェアAlないしAnを登録したICカードであることを特徴とする、請求項3記載のアプリケーション。前記ソースコード1がJAVA登録商標言語のバーチャルマシン内に書かれたプログラムであり、前記変換済みコード3がJAVACARD登録商標言語のバーチャルマシン内にかかれたプログラムであることを特徴とする請求項3または請求項4記載のアプリケーション。本発明はこの必要に対して、極端に長くかつ高価な手順を必要とすることなく応答することを目指す。本発明による方法は、コードの変換の訂正を組織的でモジュール的な仕方で検証することを可能にする。この発明の範囲内で、それ自体よく知られた二つのフォルマリスムが本質的な仕方で使用される。それは操作的意味論と論理関係論である。これらのフォルマリスムの一層詳細な記述については、第1にH.R.Nielson、およびF.Nielson著意味論とその応用:正式な紹介Wiley、1992年および第2にMitchell著、プログラミング言語の基礎MITプレス、1996年に出ているのが有益である。本発明の本質的特徴によれば、コード変換器の検証方法は、補助関数と呼ばれる諸関数によりパラメータ表現された共通の一つのバーチャルマシーンを使って二つのコードの意味を明示することからなる。二つのコードの相違は、前記補助関数で表現され再グループ化される。各補助関数は二つのバージョンを有し、それはソースコード内のバージョンと変換済みコード内のバージョンである。最初のモジュールは二つのコードについて共通であるから同一であり、それらが等価ならば検証は行なわれない。二つのコードの等価を示すには前記補助関数が二つずつ等価であることが示されれば充分である。これら二つの部分集合は、ソースコードと変換済みコードの二つの全体において考えて表現した二つの集合よりもはるかに複雑さを少なくすることができる。本発明によれば検証処理に固有の困難さは非常に減少されることになり、相関的な方法により検証のプロセスが経済的で技術的に実現可能なものになる。本発明のひとつの目的は、所定ソースコードから搭載システム向けの所定変換済みコードにする変換器の検証方法であって、前記ソースコードと前記変換済みコードはバーチャルマシンに結合され、前記ソースコードと前記変換済みコードのそれぞれについて、これら2つのコードの作用を因数分解する唯一のバーチャルマシンを構成する共通の第1部分集合を決定するステップと、複数の所定補助関数で構成され、前記補助関数が前記ソースコードおよび前記変換済みコード内の常駐差異を表現する第2部分集合を、前記ソースコードと前記変換済みコードのそれぞれについて、決定するステップと、前記ソースコードに結合された前記第2部分集合に属する各ペアの第1補助関数と、前記変換済みコードに結合された前記第2部分集合に属する各ペアの第2補助関数を、前記補助関数のペアごとに結合するステップと、前記全てのペアの前記補助関数の間で決定される対応の特性を検証するステップと、前記コンバータによるソースコードから変換済みコードへの前記変換は前記決定される対応の特性を満足することを検証するステップを、少なくとも含んでいることを特徴とする前記検証方法である。本発明の更なる目的は、ICカード内に登録されるためのコードの生成のための変換器のこのような方法の利用である。添付図面を参照しながら本発明を詳細に説明する。本発明によるコードの変換器の検証方法をこれから一層詳細な仕方で説明する。図1は、最初または起源のコードという意味で、ソースコードと呼ばれるコード1から、コード2の変換器を使って変換済みコードと呼ばれる最終コード3へ変換する処理を図式的に示す。この変換器はおそらく情報手段または一つの特定ソフトウェアである。従来の方法で変換済みコードは実線の中の搭載システム4の中に常駐するように定められている。変換器2も同様に点線内の参照番号4’の搭載システム内に常駐またはダウンロードされ得る。搭載システム4-4’内にローディングまたは記録の後に、変換済みコードは唯一の参照番号5で表現された必要なだけの一つまたはいくつかのタスクの実行を可能にする。搭載システム4が普通の自動的な情報資源図示なしを有するものと仮定する。アプリオリにコードの変換は全部で一回だけで所与の変換器により、またはまれな機会すなわちたとえばオリジナルコード、またはソースコード1のバージョンの更新において実行される。したがって変換済みコード3がソースコード1に等価であることの正式な証明を確立できることが必要である。もし変換器2が正しい仕方で機能すればこのプロセスが検証を可能にする。しかしながらすでに想起したように、全体としてソースコードと変換済みコードにより形成された二つの集合を考えるならば、このような決定が一般的に実際的なやり方では理論的に不可能であることが証明される。本発明による方法の本質的な特徴は結局、二つのコードの各々について二つの集合、すなわち第1部分集合と第2部分集合を見出すことで構成されることになる。本発明の方法の重要な特徴によれば、第1部分集合はソースコードと変換済みコードの二つのコードに共通のバーチャルマシンを形成する。この事実により、第1部分集合の等価なことを検証することは不必要である。補助関数で構成される第2部分集合は、反対に一つのコードと他のコードを区別する。ソースコードと変換済みコードが等価であること決定は、このとき第2部分集合の補助関数のペアが全て等価であることの決定になる。こうして補助関数に常駐する複雑性を大きく減少し得る。結局等価であることの正確な決定が可能になる。図2Aと図2Bは本発明による方法を非常に図式的に示す。図2Aが一層詳細に示すように、ソースコード1および変換済みコード3の第1部分集合が一つの共通のバーチャルマシン13を形成する。第2部分集合10と同30はそれぞれ一連の前記補助関数により構成され、それらが等価であることは認証されるようになる。これらの補助関数10と同30は共通のバーチャルマシン13をパラメータ表現する。ソースコード1と変換済みコード2の二つのコードの等価であることは、二つずつ取った補助関数10と同30の等価であることを検証することになるが、これは図2Bに関して後に示す。これから処理のステップを一層詳細な仕方で説明する。ソースコードと変換済みコードが、それぞれ前記第1バーチャルマシンおよび第2バーチャルマシンに結合される。第1ステップはソースコードと変換済みコードの内容を因数分解できる唯一のバーチャルマシンすなわち操作的意味論の定義で構成される。二つのコードの間の差異は、そのとき、二つのコードの中で異なって解釈されるかまたは作動される補助関数を通して現れる。バーチャルマシンは、下記の規則の集合により表現できる。諸前提premissesは、ある規則の適用条件、すなわちブール代数式でも、状態変化を表現するために使用される変数への数の代入でもある。状態の情報を引き出したり条件を表現したりするために、諸前提が補助関数の助けを求める。諸前提が検証されて命令Instruction1が見出されたときに、マシンの状態がどのように展開するかを、各規則が指示する。コードの命令の各タイプについて、この形式の規則を1つまたはいくつか定義される。第2のステップは、2つのコードの中に使用されるデータのタイプまたは構造の定義からなる。基本的なタイプを例えば次のように定義できる。そしていくつかのタイプは例えば次のように構成される。第3のステップは、θで参照され、諸バーチャルマシンに使用されている諸タイプの解釈からなる。各タイプθについてソースコードについての解釈と、変換済みコードについての解釈と、2つの解釈の間の関係について1つの解釈が定義される。これらの関係は論理的関係と呼ばれて、諸タイプの構造を満足する。単純なタイプについては、それらは明示的に定義され、構造化されたタイプについては、それらは構造の構成要素から推論される。例えば、下記の諸ペアについて、これらの関係で、θ1とθ2はタイプであり、またa、b、a’、b’はタイプの要素である。同様に諸関数について、論理的諸関係が観察可能な諸タイプについて同定される関係であるはずであり、すなわち、2つのコードが同じ結果になることが望ましい。印刷可能なタイプおよび/または情報ディスプレイに表示可能なタイプが習慣的に問題になっている。問題になるのは基本的なタイプであろうが、しかし例えばスタックすなわち所与のプログラムの諸変数を表現する構造化されたタイプも問題であろう。第4のステップはバーチャルマシン内で使用される補助関数の解釈からなる。各補助関数fについて、と記されるソースコードについての解釈と、と記される変換済みコードについての解釈が与えられる。等価の決定は、補助関数の定義が論理的関係を満足することを示すことからなる。一層正確には、各補助関数f:θ→θ’について、下記のように示される。2つのバーチャルマシンは下記の関係にあることになる。観察可能な諸タイプについて関係が同定されるように、ソースコードと変換済みコードが対話的に同定される。最後のステップは、論理的関係を満足する変換器Γ図1:2が存在することを示すことから構成される。それは、Γ:S→Tがその論証のタイプに連合した論理的関係を、ソースコードS図1:1と変換済みコードT図1:3によって満足することを検証することで為される。それを行なうには、下記の関係に従うことが必要である。論理的関係が制約の集合を明示することが今や示された、従って、変換器2を図面によって、洗練と抽出の技法を適用して、適当な証明の助けを求めながら、正しく読み取ることができる。したがって本発明による方法は、検証のプロセスの大きな機械化を可能にするので重要な利点を提供し、特にこの検証が複雑さの一層少ない部分集合上で行われるので、それを良好に実行することができる。ソースコード1の変換は一層簡単な変換の連続のように書かれ得るが、この方法は各変換を独立に示すために応用され得る。結局それはモジュール化の大きな利点を提供する。図2Bに示すように物理的装置または論理的装置である装置6の助けを借りて、補助機能10と同30の部分集合上だけで、検証を実行できる。n個の補助関数が存在して、それぞれ10a、10b、10i、10n1、10nおよび20a、20b、20i、20n1、20nと参照されるものと仮定する。装置6が物理的装置であれば、検証回路60a、60b、60i、60n1、60nコンバータの記号により図2Bに任意に表現されると同様に、たとえば関数10iおよび30iのペアのための検証回路60iのように検証のための補助関数のペアを含む。この装置6の出力または諸出力を一つの参照記号61で示すが、ソースコード1および変換済みコード3に対応する補助関数の全ての可能なペアの中の論理的関係が満足されることを指示する。この一連の操作は、二つのコードの等価の正式な証明を、そのグローバル性においてもたらすのに充分である。注意すべきは、本発明による方法はアポステリオリすなわち既存の変換器を検証するために同様に、アプリオリに新しい変換器の開発の援助として使用できる。特にこれは後者の場合に、正しく機能するための、言いかえればこの変換器によってソースコードから生成される変換済みコードが前記の等価の要求を満足するための、その特性を決定することができる。これからICカードの範囲内で説明する。図3は、ICカード7のアーキテクチャを図式的に示す。この図には本発明による方法を良く理解するために必要な要素のみを示している。ICカード7は特に、外部世界との通信を可能にする入出力装置70、固定またはプログラム可能のROM、PROM、EPROM、またはEEPROMタイプの1次メモリ装置71、およびランダムアクセスメモリ装置72を含んでいる。ICカード7はまたバスを介してICカード7の他の構成要素と対話するマイクロプロセッサまたはマイクロコントローラ73を含んでいる。このようなICカード7の論理的アーキテクチャはISO規格7816-3に従って、プロトコル層によって翻訳されて入出力装置70に結合された最下層につながり、さらにICカード内に登録された論理アプリケーションに結合した最上層につながっている。これらの規格は伝送が直列モードで実行されることを予想している。ソースコード1は変換器によってコード2へ変換されると、ICカード7へ伝送されてそこへ登録されるが、一般に入出力装置70を介して固定または半固定のメモリ装置71内に登録される。ICカード7により取扱われる単数または複数の論理アプリケーションはICカード7内、すなわちメモリ装置71内に常駐として登録されるか、またはランダムアクセスメモリ72内に一時的な仕方で登録され得る。後者の場合はアプリケーションは入出力装置70を介して通信回線によってロードされる。説明している例ではICカード7がマルチアプリケーションタイプであって、そのうえマルチユーザのタイプであると仮定している。したがってICカード7はm個の論理アプリケーションを取扱い、A1ないしAmは変換された言語3で記述される。ICカードのために現在使用されている言語の一つはJavaCardと呼ばれてきた。それはICカードのプログラム作成の専用の言語であって、言語Java登録商標の制約によって構成される。同様にICカード7はコードの諸部分にローディングを現場で変換するように働く補助コンバータをストックすることができる。本発明による方法の諸ステップを一般的な範囲において以下に説明するが、この好ましいアプリケーションの範囲以内で特に詳しく例示する。知られているように言語JavaCardの設立は、ファイルCAP内のdeClassesと呼ばれるファイルを変換するコンバータによってコンバータを呼び出す。クラスの一つのファイルは、コンパイルの単位でありまたプログラムJavaのオブジェクトコードの表現である。ファイルCAPは同一のpackageJavaCardの全てのクラスを再グループして、唯一のconstantpoolしか含まない。packageJavaCardはクラスを再グループして、名称の種類を創設するためのJava構成である。constantpoolの役割はテーブルであって、Javaのためのクラスの各ファイルに結合されたテーブルであり、またJavaCardのために各ファイルCAPに結合されたテーブルである。このテーブルは定数文字、実体などのストリングを再グループする。それはJavaとJavaCardのバーチャルマシン内で使用される。変換はトリビアルでなくグローバルである。すなわちそれはトークンと呼ばれる実体、すなわち全部で7または8ビットの数字により、全てのパッケージ、クラス、フィールド、方法の名称を取りかえる。これらのトークンはテーブルにアクセスするための索引の役をする。そのうえ変換はファイルCAP内の同一のパッケージのクラスの全てのファイルを、constantpoolの併合と方法のテーブルの再組織化によって再グループする。言語JavaCardは特に銀行用ICカード上で使用されるのを目的としている。したがって、言語Javaのバーチャルマシン内に書かれたプログラムすなわちバイトコードから言語JavaCardのバーチャルマシン内に書かれたプログラムへの変換の修正を検証すること、すなわちこれら二つのプログラムの等価の証明をもたらすことが非常に重要である。この正式な証明は、本発明による方法の諸ステップを実行することによりもたらされる。第1のステップは操作的意味論の定義からなる。バイトコードの各命令に一つまたは複数の意味論的規則が結合される。バイトコードはポータブルなアセンブラコードである。それは、バーチャルマシンJavaまたはJavaCardのためのオブジェクトコードである。たとえばこのコードの命令の一つに結合された意味論的規則である命令getfieldは下記のように記述される。例において状態は、最初にカレントな命令getfieldi;bcと共に実行されるコード、オペランドのスタックr::ops、ローカル変数l、カレントのクラスの参照cおよびスタックhから構成される。getfieldiの実行時に実行される操作を規則が規定する。-補助関数constant_poolはインデックスiを使用するが、これは該当するconstant_pool内のフィールドソースコードまたは変換済みコードがそれによって動かされる署名またはトークンの参照f_refを得るためである。-参照τはオブジェクトを示し、それはスタックstackの頂上で読まれて読み出されるべき領域のオブジェクトである。この参照により、ヒープheaphrの中にc_refそれによってソースコードまたは変換済みコードが動かされる資格ある名称またはトークンのペアの動的クラスおよびオブジェクトivのフィールドのリストを発見することができる。-あらかじめ計算された参照とフィールドのリストを使用することによりフィールドが、v:=ivf_refと読まれる。-命令getfieldはフィールドの値によってオブジェクトの参照を置換えて状態を変更して、コードbcの続きにより実行が継続される。第2のステップはタイプの定義により構成される。JavaCard言語の場合は貯蔵場所の統一を表現するためにタイプWordを定義する。構築されるタイプの例としてconstantpoolのタイプは下記の通りである。これと共に例においてconstantpoolはインデックスCP_indexは基本的と考えられるを取り、また入力ここでは一つのクラス、一つの方法、または一つのフィールドへの参照を返す関数と見られる。bytecodeのタイプは、下記の通りである。bytecodeは命令のシーケンスである。タイプInstructionは、JavaCardのbytecode内に使用される全ての命令を列挙する。第3ステップは諸タイプの解釈からなる。JavaCardの場合において、ソースコードについての解釈は、名称を使用するクラスのファイルの形式のもとにと記され、tokensを使用するファイルCAPの形式のもとに変換されたコードについての解釈はと記される。例としてタイプは、下記の通りソースコードについて検証される。名称の基礎へのモデルにおいて、constantpoolはクラスの名称参照されるconstantpoolを指示するためおよび一つのindexの名称からなる。タイプは、下記の通り変換済みコードについて検証される。constantpoolのインデックスはpackageのtoken説明する例においては、packageまたはファイルCAPごとに唯一のconstantpoolが存在するおよび一つのインデックスにより構成される。関係Rcp_indexは、下記の式16のような全単射として定義される。名称の基礎へのモデル内で参照されるconstantpoolを含むクラスのpackageの名称は、tokensをベースとするモデル内で参照されるconstantpoolを含むpackageのtokenと関係があるはずである。indexiおよびi’上の唯一の制約は、Rcpindexが全単射であるべきことだけである。したがってconstantpoolsの入力は再グループされ、再配列され得る。第4ステップは補助関数の解釈で構成される。たとえば名称の基礎へのモデルについての補助関数constant_poolのバージョンは、下記の通りである。これと共に関数pack_nameはクラスの名称を取ってpackageの名称を介し、また関数env_nameはパッケージの名称とクラスの名称を取って、指定されたクラスのファイルを表現する構造を、クラスの階層の中に発見する。constantpoolはクラスのファイルから抽出される。tokensをベースとするモデルについて、補助関数のバージョンはは、下記の通りである。これと共にconstantpoolは関数env_tokとパッケージのtokenを使って環境すなわちファイルCAP内に発見される。第5のステップは、補助関数が論理的関係を尊重することの証明からなる。もしconstantpoolへのアクセスの関数の例が新しく参照されるならば下記の通り決定することが必要である。は関係Rcpindexと関係Rcpinfoの関数で完全に定義される。この定義を使用して下記のように検証するのに充分であることが示される。これにともに証明はRcpinfoおよび下の式24から想起される特性に基く。この方法の最後の第6ステップは、このコンバータによるコードとデータの変換が、決定された論理的関係を尊重するように変換器を決定することからなる。たとえばpackagesへの参照は、モデルによって名称であったりtokenesであったりする。Rpackagerefに結合した論理的関係はpackageの名称とpackageのtokensの間の全単射のように定義される。tokens内のパッケージの名称の変換を実現するコンバータの関数が実際に全単射であることを検証するだけで充分である。以上のことを読めば本発明が定めた目的を本発明が充分に達成することを容易に認められる。しかしながらとくに図2と図3に関して明示的に説明した実施例だけに本発明を限定すべきではない。最後に、ICカードまたは類似のタイプのアプリケーションのためにとくに関係がある言語JavaCardのバーチャルマシンのプログラムにおける言語Javaのバーチャルマシンのプログラムの変換の場合についての詳細の仕方でこの方法を説明してきたが、本発明はいかなる場合もこの特別なアプリケーションに限定されない。含まれる装置が比較的に限定された情報資源しか処理しない場合のたびに、本発明を応用することができ、特にRAMまたはROMのメモリ容量および/または使用されるプロセッサの計算能力が比較的限定される場合には本発明を利用することができる。例としては電子的な書物、たとえばインターネットサイトの出所のデータを送信し貯蔵するためのいわゆるe-book、たとえばいわゆるorganiserタイプのポケット電卓、インターネットネットワークに接続できるある種の移動電話などを例としてあげることができる。これら全ての場合において総合情報資源をより良く使用するためには最適な言語で処理する必要がある。"