論文の概要: A Minimal Executable Proof for Multi-Language Contract Traceability

• arxiv url: http://arxiv.org/abs/2605.28546v1
• Date: Wed, 27 May 2026 14:37:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:56.121859
• Title: A Minimal Executable Proof for Multi-Language Contract Traceability
• Title（参考訳）: 多言語契約トレーサビリティのための最小実行可能性証明
• Authors: Werner Kasselman,
• Abstract要約: 本報告ではDAG-TOML契約の検証を意図的に行う。 コントラクト、実装グラフ、トレーサビリティチェーン、レビューゲートが実行可能な目撃者に対してどのようにチェックできるかを示している。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper reports a deliberately small executable proof for a DAG-TOML contract: six "Hello, world!" implementations in Rust, Go, C, Java, TypeScript, and AWK are linked to one observable-output contract, one implementation DAG, one traceability file, one readiness gate, and one evidence matrix. The load-bearing contract requires the exact UTF-8 byte sequence `Hello, world!\n`, zero stderr bytes, and exit code 0. On the runner used for this paper, the witness harness reported five PASS outcomes, one SKIP for Java because `javac/java` was not on `PATH`, and zero FAIL outcomes. Two sidecar witnesses exercise narrower source-analysis claims: a convoluted Go rewrite hides the contiguous greeting literal but remains visible to sqry at the declared AST symbol and simple-edge level, while an indirect AWK rewrite uses a declared source profile because AWK is not in the repository's sqry-backed validator language set. The contribution is not a benchmark, a claim of general semantic equivalence, or a production assurance system. It is a compact, falsifiable artifact that shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.
• Abstract（参考訳）: Rust, Go, C, Java, TypeScript, AWKの6つの"Hello, world!"実装は、観測可能な出力コントラクト、DAG1実装、トレーサビリティファイル1つ、準備ゲート1つ、エビデンスマトリックス1つにリンクされている。 ロードバリング契約には、正確なUTF-8バイトシーケンス `Hello, world! n`, 0 stderr bytes, and exit code 0。 この論文で使用されたランナーでは、目撃者のハーネスがPASSの結果を5つ報告した。 2つのサイドカーの目撃者はソース分析の主張をより狭くしている: 複雑なGoリライトは、簡潔な挨拶リテラルを隠すが、宣言されたASTシンボルと単純なエッジレベルでsqryに表示され、間接的なAWKリライトは、AWKがリポジトリのsqry-backed Validator言語セットにはないため、宣言されたソースプロファイルを使用する。 この貢献は、ベンチマークや一般的な意味的等価性の主張、生産保証システムではない。 これは、契約、実装グラフ、トレーサビリティチェーン、レビューゲートが実行可能な目撃者に対してどのようにチェックできるかを示す、コンパクトで偽造可能なアーティファクトである。

関連論文リスト

• An Execution-Verified Multi-Language Benchmark for Code Semantic Reasoning [10.815335026032377]
  TraceEvalは、コードセマンティック推論のための最初の実行検証されたマルチ言語ベンチマークである。 TraceEvalは、Python、JavaScript、Javaにまたがる1,600以上のオープンソースリポジトリから抽出された10,583の現実世界プログラムで構成されている。 最も強いClaude-Opus-4.6は、3つの言語で平均72.9%のF1に達する。
  論文  参考訳（メタデータ） (2026-05-10T07:17:00Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
  論文  参考訳（メタデータ） (2025-05-20T05:15:47Z)
• Verified invertible lexer using regular expressions and DFAs [0.0]
  本稿では,シリアライズおよびレキシングフレームワークに適用する可逆性の概念について検討する。 シリアライゼーションはデータ構造をビット配列に書き込むプロセスであり、レキシングは文字のストリームを読み取ってトークンに分割するプロセスである。
  論文  参考訳（メタデータ） (2024-12-18T08:03:17Z)
• Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study [0.0]
  ASN.1は地上および宇宙通信で広く使われているデータ構造を記述するための言語である。 ACN は ASN.1 に沿って、複雑なバイナリフォーマットとレガシプロトコルを記述するために使用できる。 ASN.1/ACNコードジェネレータをScalaコードに移植する方法を示す。 次に、生成元を拡張して、実行可能コードだけでなく、十分な事前条件、後条件、帰納的証明のための補題を出力します。
  論文  参考訳（メタデータ） (2024-12-10T06:54:42Z)
• Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
  仮説文書埋め込み(英: hypothetical Document Embeddings, HyDE)は、ゼロショット高密度検索システムである。 我々は,HyDEが最先端の非教師付き高密度検索器であるContrieverを著しく上回っていることを示す。
  論文  参考訳（メタデータ） (2022-12-20T18:09:52Z)

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

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