文献

J-GLOBAL ID：201902219896532799   整理番号：19A2420761

形式的仕様記述言語によるGOSPEL提供OCAML【JST・京大機械翻訳】

GOSPEL-Providing OCaml with a Formal Specification Language

著者 (4件)： Chargueraud Arthur (Inria Nancy - Grand Est, Strasbourg, France) ,  Filliatre Jean-Christophe (Inria Saclay - Ile de France, Palaiseau, France) ,  Lourenco Claudio (Inria Saclay - Ile de France, Palaiseau, France) ,  Pereira Mario (NOVA LINCS & DI, FCT, Universidade Nova de Lisboa, Lisbon, Portugal)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 11800  ページ： 484-501  発行年： 2019年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 本論文では,OCamlのための行動仕様言語であるゴールを紹介した。データ構造とアルゴリズムのモジュール検証を可能にするように設計した。ゴスペルは,セparation論理への翻訳によって定義された形式的意味論によって,契約ベースの,強く分類された言語である。分離論理における直接書込み仕様と比較して,ゴールは,簡潔性を大いに改善する高水準構文を提供し,そして,分離論理によるfamiliのないプログラマにアクセスすることができる。OCamlコードを指定するためにゴールが開発されているが,その設計の多くの側面が他のプログラミング言語に適用できると信じる。本論文では,ゴールの設計と意味論を提示し,汎用のOCamlデータ構造の形式的に検証されたライブラリの開発への応用について報告する。Copyright 2019 Springer Nature Switzerland AG Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 形式的仕様記述言語 ,  プログラミング言語 ,  データ構造 ,  意味論 ,  アルゴリズム ,  *言語 ,  *仕様記述言語 ,  プログラマ
準シソーラス用語： 構文 ,  分離論理 ,  形式的意味論 , 【Automatic Indexing@JST】

分類 (1件)： 人工知能  (JE08000Z)

タイトルに関連する用語 (1件)： 形式的仕様記述言語