論文の概要: DSpec2Test: Specification-Driven Test Generation in Dafny

• arxiv url: http://arxiv.org/abs/2609.29713v1
• Date: Mon, 31 Aug 2026 13:59:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-28 05:09:56.116564
• Title: DSpec2Test: Specification-Driven Test Generation in Dafny
• Title（参考訳）: DSpec2Test: Dafnyの仕様駆動テスト生成
• Abstract要約: DSpec2TestはDafnyの仕様駆動テスト生成ツールである。 実装の詳細を考慮せずに、正式な仕様からテストを引き出す。 We evaluate DSpec2Test on programs from DafnyBench muted using MutDafny。
• 参考スコア（独自算出の注目度）: 40.51767490231935
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verification-aware languages, such as Dafny, integrate logical constructs into code and enable automatic verification of program correctness. However, tests remain helpful in scenarios that verification alone does not address (e.g., to support test-driven development). Existing Dafny test generation tools are implementation-based, limiting their applicability in this context. We present DSpec2Test, a specification-driven test generation tool for Dafny that automatically derives tests from formal specifications, without considering implementation details. Our tool extends Dafny's generate-tests command with a new blackbox mode based on Disjunctive Normal Form (DNF) equivalence class partitioning and optional Boundary Value Analysis (BVA). DSpec2Test relies on the Z3 SMT solver to synthesize inputs and expected outputs that meet the specification-derived constraints. We evaluate DSpec2Test on programs from DafnyBench mutated using MutDafny and compare it against Dafny's existing implementation-driven Block mode. DSpec2Test achieves a 93.9% mutation kill rate on a dataset of 131 mutants, outperforming Block's 82.4%, and uniquely killing 17 mutants. These results suggest that specification-driven testing is an effective and complementary approach for testing Dafny programs.
• Abstract（参考訳）: Dafnyのような検証対応言語は、論理構造をコードに統合し、プログラムの正確性の自動検証を可能にする。 しかし、検証だけでは対処できない(例えば、テスト駆動開発をサポートする)シナリオでは、テストは役に立ちます。 既存のDafnyテスト生成ツールは実装ベースであり、このコンテキストにおける適用性を制限する。 Dafnyの仕様駆動テスト生成ツールであるDSpec2Testを紹介します。 我々のツールは、DNF(Disjunctive Normal Form)同値クラスパーティショニングとオプション境界値解析(BVA)に基づいて、新しいブラックボックスモードでDafnyのジェネレーションテストコマンドを拡張する。 DSpec2Testは、仕様由来の制約を満たす入力と期待出力を合成するためにZ3 SMTソルバに依存している。 我々は、MutDafnyを用いて変異したDafnyBenchのプログラム上でDSpec2Testを評価し、Dafnyの既存の実装駆動ブロックモードと比較した。 DSpec2Testは131個の変異株のデータセット上で93.9%の突然変異率を獲得し、ブロックの82.4%を上回り、17個の変異株を独自に殺している。 これらの結果は、仕様駆動テストがDafnyプログラムのテストに効果的で補完的なアプローチであることを示唆している。

関連論文リスト

• Intention-Driven Generation of Project-Specific Test Cases [45.2380093475221]
  検証意図の記述からプロジェクト固有のテストを生成するIntentionTestを提案する。 13のオープンソースプロジェクトから4,146件のテストケースで,最先端のベースライン(DA, ChatTester, EvoSuite)に対してIntentionTestを広範囲に評価した。
  論文  参考訳（メタデータ） (2025-07-28T08:35:04Z)
• Learning to Generate Unit Tests for Automated Debugging [52.63217175637201]
  ユニットテスト(UT)は、コードの正確性を評価するだけでなく、大きな言語モデル(LLM)にフィードバックを提供する上でも重要な役割を果たします。 提案するUTGenは,LLMに対して,予測出力とともにエラーを示す単体テスト入力を生成することを教える。 UTGen は他の LLM ベースラインを7.59% 上回っていることを示す。
  論文  参考訳（メタデータ） (2025-02-03T18:51:43Z)
• CasModaTest: A Cascaded and Model-agnostic Self-directed Framework for Unit Test Generation [5.450831103980871]
  CasModaTestは、カスケードされた、モデルに依存しない、エンドツーエンドのユニットテスト生成フレームワークである。 テストプレフィックスを生成し、オークルをテストし、それらの有効性をチェックするためにコンパイルまたは実行します。
  論文  参考訳（メタデータ） (2024-06-22T05:52:39Z)
• LLM-Powered Test Case Generation for Detecting Bugs in Plausible Programs [37.48856389469826]
  TrickCatcherは、可算プログラムでバグを発見するためのテストケースを生成する。 TrickCatcherは1.80x、2.65x、1.66xのリコール、精度、F1スコアを達成する。
  論文  参考訳（メタデータ） (2024-04-16T06:20:06Z)
• Observation-based unit test generation at Meta [52.4716552057909]
  TestGenは、アプリケーション実行中に観察された複雑なオブジェクトのシリアライズされた観察から作られたユニットテストを自動的に生成する。 TestGenは518のテストを本番環境に投入し、継続的統合で9,617,349回実行され、5,702の障害が見つかった。 評価の結果,信頼性の高い4,361のエンドツーエンドテストから,少なくとも86%のクラスでテストを生成することができた。
  論文  参考訳（メタデータ） (2024-02-09T00:34:39Z)
• An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation [3.9762912548964864]
  本稿では,自動単体テスト生成における大規模言語モデルの有効性について,大規模な実証評価を行った。 これはJavaScript用のテスト生成ツールで、npmパッケージ内のすべてのAPI関数のユニットテストを自動的に生成します。 TestPilotの生成されたテストの92.8%は、既存のテストと50%以上の類似性を持っていない。
  論文  参考訳（メタデータ） (2023-02-13T17:13:41Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。