抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
この報告書では,APDC(’Area Pr’atica de Desenvolvimento Curricle)コースのための研究プロジェクトのために開発された予備的研究を提示する。このプロジェクトの主な目標は,Why3ツールのトップで,効果のある高次プログラムの検証のためのフレームワークを開発することである。高次OCaml実装から1次への中間体変換として脱官能化を用いた。この翻訳の目標はWhyML,Why3のプログラミング言語である。脱機能化は高次プログラムの自動検証のための興味深い経路であり,これは,生成された1次プログラムの正当性を証明するために,オフライン自動プログラム検証者を採用することができるので,より高次のプログラムの自動検証のための興味深い経路であると信じる。また,この報告書は,演繹的プログラム検証の主題に読者を導入し,そして,高次効果のあるプログラムを証明するために使用するツールと概念のいくつかを紹介する。【JST・京大機械翻訳】
