鍵

鍵

KeY 1.4 のスクリーンショット
開発者	カールスルーエ工科大学、ダルムシュタット工科大学、チャルマース工科大学
安定版リリース	2.10.0 / 2021年12月23日[1] ( 2021-12-23 )
書かれた	ジャワ
オペレーティング·システム	Linux、Mac、Windows、Solaris
利用可能	英語
タイプ	形式検証
ライセンス	ライセンス
Webサイト	キープロジェクト

KeYツールは、Javaプログラムの形式検証に使用されます。このツールは、Java モデリング言語で記述された仕様をJava ソース ファイルに受け​​入れます。これらは動的ロジックの定理に変換され、同様に動的ロジックで定義されたプログラム セマンティクスと比較されます。KeY は、対話型 (つまり手動) および完全自動の正しさ証明の両方をサポートしている点で非常に強力です。失敗した証明の試みは、より効率的なデバッグや検証ベースのテストに使用できます。Cプログラムまたはハイブリッド システムの検証に適用するために、KeY にはいくつかの拡張機能があります。KeYは、ドイツのカールスルーエ工科大学、ドイツのダルムシュタット工科大学、スウェーデンのヨーテボリにあるシャルマース工科大学によって共同開発され、 GPLに基づいてライセンスされています。

KeY への通常のユーザー入力は、JML の注釈が付いた Java ソース ファイルです。両方とも、KeY の内部表現である動的ロジックに変換されます。指定された仕様から、実行する必要があるいくつかの証明義務が発生します。つまり、証明を見つける必要があります。このために、プログラムは記号的に実行され、その結果としてプログラム変数に加えられた変更は、いわゆる更新に格納されます。プログラムが完全に処理されると、1 階の論理証明義務が残ります。KeY システムの中心には、証明を終了するために使用される、シーケント計算に基づく1 階の定理証明器があります。干渉ルールは、シーケントへの変更を記述するための独自の単純な言語で構成される、 いわゆるタクレットにキャプチャされます。

KeY の理論的基礎は、 Java Card DL と呼ばれる形式論理です。DL は Dynamic Logic (動的論理) の略で、Java Card プログラムに合わせた 1 階動的論理のバージョンです。そのため、たとえば のようなステートメント (式) が許可されます。これは、事後条件 が、事前条件 を満たす任意の状態でJava Card プログラムを実行することによって到達可能なすべてのプログラム状態で成立する必要があることを直感的に示しています。これは、および が純粋に 1 階である場合、 Hoare 計算におけると同等です。ただし、動的論理は、式に などのネストされたプログラム モダリティを含めることができる点、またはモダリティを含む式に対する量化が可能である点で、Hoare 論理を拡張しています。また、終了 を含むデュアルモダリティもあります。この動的論理は、各 Java ブロックにモダリティと がある、特別なマルチモダリティ ロジック (モダリティの数が無限) と見なすことができます。 ${\displaystyle \phi \rightarrow [\alpha ]\psi }$${\displaystyle \psi}$${\displaystyle \alpha}$${\displaystyle \phi}$${\displaystyle \{\phi \}\alpha \{\psi \}}$${\displaystyle \phi}$${\displaystyle \psi}$${\displaystyle [\alpha ]}$${\displaystyle \langle \alpha \rangle }$${\displaystyle \alpha}$${\displaystyle [\alpha ]}$${\displaystyle \langle \alpha \rangle }$

KeY システムの中心には、シークエント計算に基づく一階定理証明器があります。シークエントは、(仮定) と(命題)が、真となる直感的な意味を持つ式の集合である形式です。演繹によって、証明義務を表す初期シークエントは、基本的な一階公理 (等式 など) のみから構築可能であることが示されます。 ${\displaystyle \Gamma \vdash \Delta }$${\displaystyle \ガンマ}$${\displaystyle \Delta }$${\displaystyle \bigwedge _{\gamma \in \Gamma }\gamma \rightarrow \bigvee _{\delta \in \Delta }\delta }$${\displaystyle e\ {\dot {=}}\ e}$

その間、プログラム モダリティはシンボリック実行によって排除されます。たとえば、式は論理的に と同等です。この例が示すように、動的ロジックにおけるシンボリック実行は、最も弱い前提条件を計算することに非常に似ています。と はどちらも本質的に同じものを表しますが、次の 2 つの例外があります。第 1 に、はメタ計算の関数であるのに対し、 は実際には特定の計算の式です。第 2 に、シンボリック実行は実際の実行と同じようにプログラムを順方向に実行します。割り当ての中間結果を保存するために、KeY は更新と呼ばれる概念を導入します。これは置換に似ていますが、プログラム モダリティが排除された後にのみ適用されます。構文的には、更新はモダリティの前に中括弧で記述された並列 (副作用のない) 割り当てで構成されます。更新を含むシンボリック実行の例:は最初のステップでに変換され、 2 番目のステップで に変換されます。その後、モダリティは空になり、事後条件への更新の「逆方向適用」により、任意の値を取ることができる前提条件が生成されます。 ${\displaystyle x\ {\dot {=}}\ 0\rightarrow [x++;]x\ {\dot {=}}\ 1}$${\displaystyle x\ {\dot {=}}\ 0\rightarrow x\ {\dot {=}}\ 0}$${\displaystyle [\alpha ]\psi }$${\displaystyle wp(\alpha ,\psi )}$${\displaystyle wp}$${\displaystyle [\alpha ]\psi }$${\displaystyle [x=3;x=x+1;]x\ {\dot {=}}\ 4}$${\displaystyle \{x:=3\}[x=x+1;]x\ {\dot {=}}\ 4}$${\displaystyle \{x:=4\}[]x\ {\dot {=}}\ 4}$${\displaystyle x}$

次の方法がいくつかの非負整数との積を計算することを証明したいとします。 ${\displaystyle x}$${\displaystyle y}$

int foo ( int x , int y ) { int z = 0 ; while ( y > 0 ) if ( y % 2 == 0 ) { x = x * 2 ; y = y / 2 ; } else { y = y / 2 ; z = z + x ; x = x * 2 ; } return z ; }      
       
       
              
              
              
          
              
              
              
        
     

したがって、証明は前提と示すべき結論から始まります。シークエント計算の表は通常「逆さま」に書かれることに注意してください。つまり、開始シークエントが下に表示され、演繹ステップが上に向かっていきます。証明は右の図に示されています。 ${\displaystyle x\geq 0\land y\geq 0}$${\displaystyle z\{\dot{=}}\x\cdoty}$

シンボリック実行デバッガーは、プログラムの制御フローを、特定のポイントまでのプログラムのすべての実行可能な実行パスを含むシンボリック実行ツリーとして視覚化します。これは、 Eclipse開発プラットフォームのプラグインとして提供されます。

KeY は、Java プログラムの単体テストを生成できるモデルベースのテストツールとして使用できます。テスト データとテスト ケースが派生するモデルは、正式な仕様 ( JMLで提供) と、KeY システムによって計算されるテスト対象の実装のシンボリック実行ツリーで構成されます。

KeY は Java で書かれ、 GPLライセンスのフリーソフトウェアです。プロジェクトの Web サイトからソースをダウンロードできますが、現在、コンパイル済みのバイナリは入手できません。別の方法として、コンパイルやインストールを必要とせずに、 Java Web Start経由で直接 KeY を実行することもできます。

KeY-Hoareは KeY 上に構築されており、状態更新を伴うHoare 計算を特徴としています。状態更新は、クリプキ構造における状態遷移を記述する手段です。この計算は、KeY のメイン ブランチで使用される計算のサブセットとして考えることができます。Hoare 計算は単純であるため、この実装は基本的に、学部クラスで形式手法を例示することを目的としています。

KeYmaera [1]（旧称HyKeY）は、微分動的論理dL [2]の計算に基づいたハイブリッドシステムの演繹検証ツールです。KeYツールをMathematicaなどのコンピュータ代数システムと対応するアルゴリズムおよび証明戦略で拡張し、ハイブリッドシステムの実用的な検証に使用できるようにします。

KeYmaera はオルデンブルク大学とカーネギーメロン大学で開発されました。このツールの名前は、古代ギリシャ神話の交雑動物で あるキメラと同音異義語として選ばれました。

カーネギーメロン大学で開発されたKeYmaeraX [3]はKeYmaeraの後継であり、完全に書き直されている。

KeY for C は、C プログラミング言語のサブセットであるMISRA Cに KeY システムを適応させたものです。このバリアントはサポートされなくなりました。

また、 ETH Zürichで開発された、抽象ステートマシンのシンボリック実行に KeY を使用する適応もあります。このバリアントはサポートされなくなりました。

• オブジェクト指向ソフトウェアの検証: KeY アプローチ。Bernhard Beckert、Reiner Hähnle、Peter H. Schmitt (編)。Springer 、2007年。ISBN 978-3-540-68977-5。 
• 演繹的ソフトウェア検証 - KeY ブック: 理論から実践まで。ヴォルフガング・アーレント、ベルンハルト・ベッケルト、リヒャルト・ブーベル、ライナー・ハーンレ、ピーター・H・シュミット、マティアス・ウルブリッヒ（編）。シュプリンガー、2016 年。ISBN 978-3-319-49812-6 
• 形式的ソフトウェア検証を指導するためのツールの比較。Ingo Feinerer と Gernot Salzer。Springer 、2008年
• 証明によるプログラミング: 完全に正しいソフトウェアへの言語ベースのアプローチ。Aaron Stump。検証済みソフトウェア: 理論、ツール、実験、2005 年。
• 高い保証（セキュリティまたは安全性）とフリー/オープンソースソフトウェア（FLOSS）。David Wheeler、2009

ウィキメディア・コモンズには、 KeY プログラム検証ツールに関連するメディアがあります。

• KeYプロジェクトのホームページ
• KeYmaeraホームページ
• KeYmaeraXホームページ