鍵
鍵
開発者カールスルーエ工科大学、ダルムシュタット工科大学、チャルマース工科大学
安定版リリース
2.12.3 / 2024年9月8日[ 1 ] ( 2024-09-08 )
書かれたジャワ
オペレーティング·システムLinux、Mac、Windows、Solaris
入手可能な英語
タイプ形式検証
ライセンスGPLバージョン2
Webサイトwww.key-project.org​​

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

概要

KeYへの通常のユーザー入力は、JMLで注釈が付けられたJavaソースファイルです。これらは両方ともKeYの内部表現である動的ロジックに変換されます。[ 5 ]与えられた仕様から、達成しなければならない証明義務、すなわち証明を見つける義務がいくつか生じます。[ 6 ]この目的のために、プログラムは記号的に実行され、その結果として生じたプログラム変数への変更は、いわゆるアップデートに格納されます。[ 7 ]プログラムが完全に処理されると、一階論理の証明義務が残ります。KeYシステムの中核には、証明を完結させるために使用される、シーケント計算に基づく一階定理証明器があります。 [ 8 ]干渉規則は、シーケントへの変更を記述するための独自の単純な言語で構成される、いわゆるタクレットに記録されます。 [ 9 ]

JavaカードDL

KeYの理論的基礎はJava Card DLと呼ばれる形式論理である。 [ 10 ] DLはDynamic Logicの略で、Java Cardプログラムに合わせた一次動的論理のバージョンである。そのため、例えば のようなステートメント（式）が許可され、これは直感的に、事後条件は、事前条件 を満たす任意の状態でJava Cardプログラムを実行することによって到達可能なすべてのプログラム状態で成立する必要があることを示している。これは、およびが純粋に一次である場合、 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 \Gamma}Δ{\displaystyle \Delta }⋀γ∈Γγ→⋁δ∈Δδ{\displaystyle \bigwedge _{\gamma \in \Gamma }\gamma \rightarrow \bigvee _{\delta \in \Delta }\delta }e ＝˙ e{\displaystyle e\ {\dot {=}}\ e}

Javaコードのシンボリック実行

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

例

次の方法がいくつかの非負整数と の積を計算することを証明したいとします。 ×{\displaystyle x}y{\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 ; }

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

結果として得られる証明木

追加機能

シンボリック実行デバッガー

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

テストケースジェネレーター

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

KeYシステムの分布と変種

KeYはJavaで書かれたフリーソフトウェアで、GNU General Public Licenseバージョン2に基づいてライセンスされています。プロジェクトのウェブサイトからソースコードまたはコンパイル済みJARファイルをダウンロードできます。[ 11 ]

キー・ホーア

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

KeYmaera/KeYmaeraX

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

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

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

CのKeyY

KeY for Cは、KeYシステムをCプログラミング言語のサブセットであるMISRA Cに適合させたものです。[ 3 ]このバリアントは現在サポートされていません。

ASMキー

抽象ステートマシンのシンボリック実行にKeYを使用する適応版も存在します。これはETHチューリッヒで開発されました。このバリアントは現在サポートされていません。

参考文献

  1. ^ 「リリース KeY-2.12.3 (2024-09-08) · KeYproject/key」 . github.com . 2025年4月26日閲覧。
  2. ^ヴォルフガング、アーレント;ベッカート、ベルンハルト。ビューベル、リチャード。ハーンレ、ライナー。シュミット、ピーター H.ウルブリッヒ、マティアス編。 （2016年）。演繹的ソフトウェア検証 – KeY Book。コンピューターサイエンスの講義ノート。 Vol. 10001.土井: 10.1007/978-3-319-49812-6。ISBN 978-3-319-49811-9. ISSN  0302-9743 .
  3. ^ a b Mürk, Oleg; Larsson, Daniel; Hähnle, Reiner (2007). 「KeY-C: Cプログラムの検証ツール」 . Pfenning, Fr​​ank (編). Automated Deduction – CADE-21 . Lecture Notes in Computer Science. Vol. 4603. ベルリン、ハイデルベルク: Springer. pp.  385– 390. doi : 10.1007/978-3-540-73595-3_27 . ISBN 978-3-540-73595-3。
  4. ^ a b Platzer, André; Quesel, Jan-David (2008). 「KeYmaera: ハイブリッドシステム向けハイブリッド定理証明器（システム解説）」 . Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (編). Automated Reasoning . Lecture Notes in Computer Science. Vol. 5195. ベルリン、ハイデルベルク: Springer. pp.  171– 178. doi : 10.1007/978-3-540-71070-7_15 . ISBN 978-3-540-71070-7。
  5. ^ベッケルト、ベルンハルト;クレバノフ、ウラジミール。ヴァイス、ベンヤミン (2016)、アーレント、ヴォルフガング。ベッカート、ベルンハルト。ビューベル、リチャード。 Hähnle, Reiner (編)、「Dynamic Logic for Java」、演繹的ソフトウェア検証 – The KeY Book: From Theory to Practice、Cham: Springer International Publishing、pp.  49–106、doi : 10.1007/978-3-319-49812-6_3、ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  6. ^ Grahl, Daniel; Ulbrich, Mattias (2016), Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner (eds.) 「From Specification to Proof Obligations」 , Deductive Software Verification – The KeY Book: From Theory to Practice , Cham: Springer International Publishing, pp.  243– 287, doi : 10.1007/978-3-319-49812-6_8 , ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  7. ^ワッサー、ネイサン;ハーンレ、ライナー。リチャード・ビューベル（2016）、ヴォルフガング・アーレント、ベッカート、ベルンハルト。ビューベル、リチャード。 Hähnle、Reiner (編)、「Abstract Interpretation」、Deductive Software Verification – The KeY Book: From Theory to Practice、Cham: Springer International Publishing、pp.  167–189、doi : 10.1007/978-3-319-49812-6_6、ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  8. ^ Schmitt, Peter H. (2016), Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner (eds.), "First-Order Logic" , Deductive Software Verification – The KeY Book: From Theory to Practice , Lecture Notes in Computer Science, vol. 10001, Cham: Springer International Publishing, pp.  23– 47, doi : 10.1007/978-3-319-49812-6_2 , ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  9. ^フィリップ・ルンマー;ウルブリッヒ、マティアス (2016)、アーレント、ヴォルフガング。ベッカート、ベルンハルト。ビューベル、リチャード。 Hähnle, Reiner (編)、「Proof Search with Taclets」、Deductive Software Verification – The KeY Book: From Theory to Practice、Cham: Springer International Publishing、pp.  107–147、doi : 10.1007/978-3-319-49812-6_4、ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  10. ^ Mostowski, Wojciech (2016), Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner (eds.)、「Java Cardプログラムの検証」、演繹的ソフトウェア検証 - KeYブック：理論から実践へ、Lecture Notes in Computer Science、vol. 10001、Cham: Springer International Publishing、pp.  353– 380、doi : 10.1007/978-3-319-49812-6_10、ISBN 978-3-319-49812-6、 2025年4月26日取得{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  11. ^ 「ダウンロード – KeYプロジェクト」 。 2025年4月26日閲覧。

出典

ウィキメディア コモンズには、KeY プログラム検証ツールに関連するメディアがあります。
「 https://en.wikipedia.org/w/index.php?title=KeY&oldid=1310647206」から取得