ダフニー
ダフニー
パラダイム命令形、機能的
デザイン：K. ルスタン M. レイノ
開発者マイクロソフトリサーチ
初登場2009 （2009年）
安定版リリース
4.11.0 / 2025年8月25日 ( 2025-08-25 )
タイピングの規律静的、強力、安全
ライセンスマサチューセッツ工科大学
ファイル名拡張子.dfy
Webサイトダフニー.org

Dafnyは命令型で関数型のコンパイル言語であり、 C#、Java、JavaScript、Go、Pythonなどの他のプログラミング言語にコンパイルできます。事前条件、事後条件、ループ不変条件、ループバリアント、終了仕様、読み取り/書き込みフレーミング仕様を通じて形式仕様をサポートしています。この言語は、関数型プログラミングと命令型プログラミングのパラダイムのアイデアを組み合わせ、オブジェクト指向プログラミングをサポートしています。機能には、ジェネリッククラス、動的割り当て、帰納的データ型、および副作用についての推論のための暗黙の動的フレーム[ 1 ]と呼ばれる分離ロジックのバリエーションが含まれます。 [ 2 ] Dafnyは、ESC/ Modula-3、ESC/Java、Spec# の開発に携わった後、Microsoft ResearchのRustan Leinoによって作成されました。

Dafnyはソフトウェア検証コンテスト（例：VSTTE'08、[ 3 ] VSCOMP'10、[ 4 ] COST'11、[ 5 ] VerifyThis'12 [ 6 ]）に定期的に参加しています。

Dafnyは検証を考慮したプログラミング言語として設計されており、コード開発と並行して検証を必要とします。そのため、Correct by Construction（構築による修正）というソフトウェア開発パラダイムに適合しています。検証証明は、数学的な整数と実数、ビットベクトル、シーケンス、集合、多重集合、無限シーケンスと集合、帰納法、共帰納法、計算証明を含む数学ツールボックスによってサポートされています。十分な仕様が与えられれば、検証義務は自動的に果たされます。Dafnyはプログラム解析を用いて多くの仕様アサーションを推論することで、仕様記述の負担を軽減します。一般的な証明フレームワークはHoare論理に基づいています。

Dafnyは、証明義務を果たすためにZ3自動定理証明器を使用するBoogie中間言語を基盤としています。 [ 7 ] [ 8 ]

データ型

Dafnyは、副作用がある可能性のある実装用のメソッドと、仕様で使用するための純粋な関数を提供します。[ 9 ]メソッドは、一般的な命令型スタイルに従った文のシーケンスで構成されますが、対照的に、関数の本体は単なる式です。メソッド内の副作用のある文（配列パラメータの要素の割り当てなど）は、句を使用して、どのパラメータが変更可能であるかに注意することで考慮する必要があります。Dafnyは、シーケンス（例：）、セット（例：）、マップ（）、タプル、帰納的データ型、可変配列（例：） など、さまざまな不変コレクションmodifies型も提供します。seq<int>set<int>map<int,int>array<int>

命令型機能

以下は、前提条件、事後条件、ループ不変条件、ループバリアントの使用を含む、Dafny の多くの機能を示しています。 

method max ( arr : array < int > ) returns ( max : int ) // 配列には少なくとも 1 つの要素が必要です。requires arr.Length > 0 // 戻り値は配列内のどの要素よりも小さくすることはできません。ensures forall j : int :: j >= 0 && j < arr.Length ==> max >= arr [ j ] // 戻り値は配列内のある要素と一致する必要があります。ensures exists j : int :: j > = 0 && j < arr.Length && max == arr [ j ] { max : = arr [ 0 ] ; var i : int : = 1 ; // while ( i < arr.Length ) // インデックスは最大で arr.Length (ループ後に i==arr.Length であることを示すために必要) invariant i < = arr . Length // これまでに max より大きい要素は見つかりません(不変条件) forall j : int :: j >= 0 && j < i ==> max >= arr [ j ] // これまでに見つかった要素の中に max と一致するものがあります(不変条件が存在します) j : int :: j >= 0 && j < i && max == arr [ j ] // arr.Length - i はステップごとに減少し、下限は 0 です (減少) arr . Length - i { // より大きい要素が見つかった場合は max を更新しますif ( arr [ i ] > max ) { max : = arr [ i ] ; }// 配列iまで続行: = i + 1 ; } }

この例では、配列の最大要素を計算します。メソッドの事前条件と事後条件は、それぞれrequiresandensures節で指定します。同様に、ループ不変条件とループバリアントは、それぞれinvariantanddecreases節で指定します。

ループ不変量

Dafnyにおけるループ不変式の扱いは、従来のHoare論理とは異なります。ループ内で変化する変数は、ループ開始前に既知の情報（のほとんど）が破棄されるように扱われます。このような変数の特性を証明するために必要な情報は、ループ不変式で明示的に表現する必要があります。一方、ループ内で変化しない変数は、ループ開始前に既知の情報をすべて保持します。次の例は、ループの使用例を示しています。 

メソッドsumAndZero ( arr : array < int > )は( sum : nat )を返します。forall i :: 0 <= i < arr . Length ==> arr [ i ] >= 0はarr を変更します。{ var i : int : = 0 ; sum : = 0 ; // while ( i < arr . Length ) { sum : = sum + arr [ i ] ; arr [ i ] : = arr [ i ] ; i : = i + 1 ; } }

これはDafnyが(sum + arr[i]) >= 0代入において成立することを証明できないため検証に失敗します。前提条件から直感的に、forall i :: 0 <= i < arr.Length ==> arr[i] >= 0ループ内では成立します。なぜなら、はNOParr[i] := arr[i];だからです。しかし、この代入により、Dafnyは を可変変数として扱い、ループ開始前からの既知の情報を削除してしまいます。このプログラムをDafnyで検証するには、(a)冗長な代入を削除するか、(b)ループ不変式を追加するかのいずれかを行います。arrarr[i] := arr[i];invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

Dafnyは、可能な限り単純なループ不変条件を推論するために、限定的な静的プログラム解析も行います。上記の例では、ループ内でinvariant i >= 0変数iが変更されるため、ループ不変条件も必要であるように見えます。基盤となるロジックではこのような不変条件が必要ですが、Dafnyはこれを自動的に推論するため、ソースレベルでは省略できます。

証明の特徴

Dafny には、証明支援ツールとしての使用をさらにサポートする機能が含まれています。functionまたは内の単純なプロパティの証明method（上記参照）は、この種のツールでは珍しくありませんが、Dafny では、ある または 別の 間のプロパティの証明も可能です。証明支援ツールfunctionでは一般的ですが、このような証明は帰納的な性質を持つことが多いです。Dafny は、帰納的仮説を適用するためのメカニズムとしてメソッド呼び出しを採用している点で、珍しいかもしれません。以下は、その例です。 

データ型List = Nil | Link ( data : int , next : List )関数sum ( l : List ): int { l に一致する場合Nil => 0 の場合Link ( d , n ) => d + sum ( n ) }述語isNatList ( l : List ) {一致l の場合Nil => true の場合Link ( d , n ) => d >= 0 && isNatList ( n ) }補題NatSumLemma ( l : List , n : int )はisNatList ( l ) && n == sum ( l )がn >= 0 であることを保証します{ match l case Nil => // 自動的に解除されますcase Link ( data , next ) => { // 帰納的仮説を適用しますNatSumLemma ( next , sum ( next )); // Dafny によって知られていることを確認しますassert data >= 0 ; } }

ここで、は との間のNatSumLemma有用な性質（つまり）を証明します。Dafnyでは、補題や定理をエンコードするために が標準的に使用され、帰納法（典型的には構造帰納法）には再帰が用いられます。場合分けは文を用いて行われ、帰納的でない場合には多くの場合自動的に処理されます。検証者は、必要に応じて展開するために、 またはの内容に完全にアクセスできる必要があります。これは、アクセス修飾子と組み合わせて使用​​する場合に影響を及ぼします。具体的には、 修飾子を用いての内容を非表示にすると、について確立できる性質が制限される可能性があります。 sum()isNatList()isNatList(l) ==> (sum(l) >= 0)ghost methodmatchfunctionpredicatefunctionprotected

参照

参考文献

  1. ^ Smans, Jan; Jacobs, Bart; Piessens, Frank (2009).暗黙的動的フレーム：動的フレームと分離ロジックの結合(PDF) . ヨーロッパオブジェクト指向プログラミング会議議事録. pp.  148– 172. doi : 10.1007/978-3-642-03013-0_8 .
  2. ^ Leino, Rustan (2010). Dafny: 機能的正しさを検証する自動プログラム検証ツール. プログラミング、人工知能、推論のための論理に関する会議論文集. pp.  348– 370. doi : 10.1007/978-3-642-17511-4_20 .
  3. ^ Leino, Rustan; Monahan, Rosemary (2010). Dafny が検証ベンチマークの課題に対応(PDF) . 検証済みソフトウェアに関する国際会議：理論、ツール、実験. pp.  112– 116. doi : 10.1007/978-3-642-15057-9_8 .
  4. ^ Klebanov, Vladimir; et al. (2011).第1回検証済みソフトウェアコンペティション：体験レポート. 形式手法に関する会議の議事録. pp.  154– 168. CiteSeerX 10.1.1.221.6890 . doi : 10.1007/978-3-642-21437-0_14 . 
  5. ^ Bormer, Thorsten; et al. (2011). COST IC0701 検証コンペティション 2011 . オブジェクト指向ソフトウェアの形式検証に関する会議議事録. pp.  3– 21. CiteSeerX 10.1.1.396.6170 . doi : 10.1007/978-3-642-31762-0_2 . 
  6. ^ Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary (2015). 「VerifyThis 2012」(PDF) .国際技術移転ソフトウェアツールジャーナル. 17 (6): 647– 657. doi : 10.1007/s10009-015-0396-8 . S2CID 14301377 . 
  7. ^ 「Z3ホームページ」 . GitHub . 2019年2月7日.
  8. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Z3: 効率的なSMTソルバー. 構築と解析のためのツールとアルゴリズムに関する会議議事録. pp.  337– 340. doi : 10.1007/978-3-540-78800-3_24 .
  9. ^ 「Dafnyプログラミング言語」 . 2022年7月14日.

さらに読む

  • マイヤー、ベルトラン、ノルディオ、マーティン編 (2012).実践的ソフトウェア検証ツール：国際サマースクール、LASER 2011、エルバ島、イタリア、改訂版チュートリアル講義. Springer . ISBN 978-3642357459。
  • Sitnikovski, Boro (2022). Dafny言語によるソフトウェア検証入門：プログラムの正しさの証明. Apress. ISBN 978-1484279779。
「 https://en.wikipedia.org/w/index.php?title=Dafny&oldid=1308161017」から取得