ダフニー

ダフニー

パラダイム	命令形、機能的
デザイン：	K. ルスタン M. レイノ
開発者	Microsoft Research、AWS [要出典]
初登場	2009年; 15年前 （2009年）
安定リリース	4.9.0 / 2024年10月31日; 49日前 ( 2024-10-31 )
タイピングの規律	静的、強力、安全
ライセンス	MITライセンス
ファイル名拡張子	.dfy
Webサイト	dafny.org

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

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 ] // 戻り値は配列内のいずれか 1 つの要素と一致する必要があります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 ; } }        
  

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

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 ; } }     
                
   

      
    
  
     
        
      
        
  

(sum + arr[i]) >= 0これは、Dafny が代入時に が成り立つことを証明できないため、検証に失敗します。前提条件から、直感的には、 はNOPなのでforall i :: 0 <= i < arr.Length ==> arr[i] >= 0ループ内で が成り立ちます。ただし、この代入により、Dafny は を可変変数として扱い、ループ前からわかっている情報を削除します。このプログラムを Dafny で検証するには、(a) 冗長な代入を削除するか、(b) ループ不変式を追加します。arr[i] := arr[i];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 (データ: 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 ) }   
   
       
            


lemma NatSumLemma ( l : List , n : int ) requires isNatList ( l ) && n == sum ( l ) guarantees 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

• 契約による設計

• Meyer, Bertrand; Nordio, Martin 編 (2012)。実践的なソフトウェア検証のためのツール: 国際サマースクール、LASER 2011、エルバ島、イタリア、改訂版チュートリアル講義。Springer。ISBN 978-3642357459。
• Sitnikovski, Boro (2022). Dafny 言語によるソフトウェア検証の紹介: プログラムの正しさの証明. Apress. ISBN 978-1484279779。

• Dafny: 機能の正確性を確認するための言語およびプログラム検証ツール - Microsoft Research
• GitHub - dafny-lang/dafny: Dafny は検証を考慮したプログラミング言語です