論文の概要: Flexible Correct-by-Construction Programming

• arxiv url: http://arxiv.org/abs/2211.15261v4
• Date: Tue, 6 Jun 2023 14:35:21 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-24 14:08:28.379303
• Title: Flexible Correct-by-Construction Programming
• Title（参考訳）: フレキシブル・バイ・コンストラクション・プログラミング
• Authors: Tobias Runge, Tabea Bordis, Alex Potanin, Thomas Th\"um, Ina Schaefer
• Abstract要約: CbC と CbC-Block と TraitCbC を比較した。 CbCは、ソフトウェアを構造化されたインクリメンタルな方法で開発することで、正確性を保証する。 我々は、CbCと同様のプログラミングガイドラインを両方のアプローチで提供し、十分に構造化されたプログラムへと導く。
• 参考スコア（独自算出の注目度）: 2.8798933523190327
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top of the programming language. Each refinement rule introduces a specific programming statement and developers cannot depart from these rules to construct programs. CbC allows to develop software in a structured and incremental way to ensure correctness, but the limited flexibility is a disadvantage of CbC. In this work, we compare classic CbC with CbC-Block and TraitCbC. Both approaches CbC-Block and TraitCbC, are related to CbC, but they have new language constructs that enable a more flexible software construction approach. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs. CbC-Block extends CbC by adding a refinement rule to insert any block of statements. Therefore, we introduce CbC-Block as an extension of CbC. TraitCbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce TraitCbC and prove soundness of the construction strategy. All three development approaches are qualitatively compared regarding their programming constructs, tool support, and usability to assess which is best suited for certain tasks and developers.
• Abstract（参考訳）: correctness-by-struction (cbc) は、機能的に正しいプログラムを構築するためのインクリメンタルなプログラム構築プロセスである。 プログラムは、本質的に満足が保証される仕様とともに段階的に構築されます。 cbcは、プログラム言語の上に追加のルールである固定粒度の事前定義された修正ルールを必要とするため、特別なツールサポートなしで使うのが複雑である。 各リファインメントルールは特定のプログラミングステートメントを導入し、開発者はこれらのルールから離れてプログラムを構築することはできない。 CbCはソフトウェアを構造化されたインクリメンタルな方法で開発することで、正確性を保証することができるが、柔軟性の制限はCbCの欠点である。 本研究では,従来のCbCとCbC-Block,TritCbCを比較した。 CbC-BlockとTritCbCはどちらもCbCに関連しているが、より柔軟なソフトウェア構築アプローチを可能にする新しい言語構造を持っている。 我々は、CbCと同様のプログラミングガイドラインを両方のアプローチで提供し、十分に構造化されたプログラムを生み出す。 CbC-BlockはCbCを拡張し、ステートメントのブロックを挿入する精細化ルールを追加する。 そこで我々はCbCの拡張としてCbC-Blockを導入する。 TraitCbCは、特定のメソッドによる特性に基づいて、コンストラクションの正確性を実装する。 正式にTraitCbCを導入し,建設戦略の健全性を証明する。 これら3つの開発アプローチは、プログラム構成、ツールサポート、特定のタスクや開発者に適したものを評価するユーザビリティについて質的に比較されている。

関連論文リスト

• CGP++ : A Modern C++ Implementation of Cartesian Genetic Programming [0.0]
  カルテシアン遺伝プログラミング(CGP)の参照実装はC言語で記述された。 本稿では,オブジェクト指向設計と汎用プログラミングパラダイムを追求するCGPのC++実装を初めて提案する。
  論文  参考訳（メタデータ） (2024-06-13T12:22:08Z)
• The Road to Near-Capacity CV-QKD Reconciliation: An FEC-Agnostic Design [53.67135680812675]
  コードワードに基づく新しいQKD調停方式を提案する。 認証された古典チャネル(ClC)と量子チャネル(QuC)は、それぞれ別々の前方誤り訂正(FEC)符号スキームによって保護される。 提案システムは,広範囲のFECスキームとQKD和解を両立させる。
  論文  参考訳（メタデータ） (2024-03-24T14:47:08Z)
• Strong Priority and Determinacy in Timed CCS [0.0]
  プロセス代数の標準理論を優先して構築し、「構成的還元」と呼ばれる新しいスケジューリング機構を同定する。 大規模な「コヒーレント」プロセスが構成的還元の共役性であることを示す。
  論文  参考訳（メタデータ） (2024-03-07T16:02:31Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• Contextualization Distillation from Large Language Model for Knowledge Graph Completion [51.126166442122546]
  我々は、差別的かつ生成的なKGCフレームワークと互換性のあるプラグイン・アンド・プレイ方式であるContextualization Distillation戦略を導入する。 提案手法は,大規模言語モデルに対して,コンパクトで構造的な三重項を文脈に富んだセグメントに変換するように指示することから始まる。 多様なデータセットとKGC技術にわたる総合的な評価は、我々のアプローチの有効性と適応性を強調している。
  論文  参考訳（メタデータ） (2024-01-28T08:56:49Z)
• Structured Code Representations Enable Data-Efficient Adaptation of Code Language Models [45.588949280419584]
  プログラム構造を用いて事前学習および微調整を行うことにより、事前訓練済みのコードモデルのデータ効率適応について検討する。 適応するモデルはプログラムの表面形式にのみ事前学習されているが,CST上での連続的な事前学習や微調整は,モデルアーキテクチャを変更することなく,様々なコードタスクのベースラインアプローチよりも改善されている。
  論文  参考訳（メタデータ） (2024-01-19T14:27:44Z)
• CSL: Class-Agnostic Structure-Constrained Learning for Segmentation Including the Unseen [62.72636247006293]
  クラス非依存構造制約学習(Class-Agnostic Structure-Constrained Learning)は、既存のメソッドと統合可能なプラグインフレームワークである。 OODオブジェクトセグメンテーションを強化するソフトアサインとマスク分割手法を提案する。 実証的な評価は、OODセグメンテーション、ZS3、DAセグメンテーションにまたがる既存のアルゴリズムの性能を向上させるCSLの進歩を示している。
  論文  参考訳（メタデータ） (2023-12-09T11:06:18Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。 コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。 即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
  論文  参考訳（メタデータ） (2023-07-05T16:58:39Z)
• C-rusted: The Advantages of Rust, in C, without the Disadvantages [0.0]
  C-rustedは、言語、システム、およびユーザ定義リソースのオーナシップ、排他性、共有性を表現するために(部分的に)Cプログラムに注釈を付けることができる革新的な技術である。 注釈付きCプログラムは、ISO Cコードを処理することができるコンパイルツールチェーンの修正されていないバージョンで変換することができる。
  論文  参考訳（メタデータ） (2023-02-10T15:48:09Z)
• Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
  予測アライメントの望ましい特性を強制するためにベイズリスクCTC(BRCTC)を提案する。 BRCTCを他の早期排出の選好と組み合わせることで、オンラインモデルの性能・遅延トレードオフが改善される。
  論文  参考訳（メタデータ） (2022-10-14T03:55:36Z)

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

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