私は最近、契約による設計とテスト駆動開発を比較した論文を読みました。DbCとTDDの間には、多くの重複、ある程度の冗長性、および少しの相乗効果があるようです。たとえば、契約に基づいてテストを自動的に生成するシステムがあります。
DbCは現代の型システム（haskellや依存型言語の1つなど）とどのように重複しており、両方を使用する方がどちらよりも優れている点はありますか？
2997 次
5 に答える
19
Ralf Hinze、Johan Jeuring、Andres Löh による論文Typed Contracts for Functional Programmingには、「チェック」の設計範囲に位置情報契約が含まれていることを示す次の便利な表がありました。
| static checking | dynamic checking
-------------------------------------------------------------------
simple properties | static type checking | dynamic type checking
complex properties | theorem proving | contract checking
于 2011-05-11T14:26:20.377 に答える
7
ほとんどの回答は、契約が動的にチェックされると想定しているようです。一部のシステムでは、コントラクトが静的にチェックされることに注意してください。このようなシステムでは、コントラクトは、自動的にチェックできる依存型の制限された形式と考えることができます。これを、Coq などのインタラクティブにチェックされる、より豊富な依存型と比較してください。
Haskell と OCaml のコントラクトの静的およびハイブリッド チェック (静的に続いて動的) に関する論文については、 Dana Xu のページの「Specification Checking」セクションを参照してください。Xu のコントラクト システムには、従属型である洗練型と従属矢印が含まれます。依存型が制限され、自動的にチェックされる初期の言語には、Pfenning と XiのDMLとATSが含まれます。DML では、Xu の作品とは異なり、依存する型が制限されているため、自動チェックが完了します。
于 2012-04-30T00:56:37.917 に答える
5
主な違いは、テストは動的で不完全であり、測定に依存して、テストしているプロパティが何であれ完全に検証されたという証拠を提供するのに対し、型と型チェックは、可能なすべてのコード パスがどのプロパティに対しても検証されていることを保証する正式なシステムです。種類で述べます。
プロパティのテストは、同じプロパティの型チェックがすぐに提供する保証レベルの限界に近づくことしかできません。コントラクトは、動的チェックのベースラインを増やします。
于 2011-05-11T15:59:56.543 に答える
4
型 systen 自体ですべての仮定を表現できない限り、DBC は価値があります。簡単な Haskell の例:
take n [] = []
take 0 _ = []
take n (a:as) = take (n-1) as
タイプは次のようになります。
take :: Int -> [a] -> [a]
ただし、n には 0 以上の値のみを使用できます。これは、DBC が介入して、たとえば、適切なクイックチェック プロパティを生成できる場所です。
(もちろん、この場合、負の値もチェックして未定義以外の結果を修正するのは簡単すぎますが、もっと複雑なケースもあります。)
于 2011-05-11T13:44:48.573 に答える