Ssreflect拡張
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/12/22 04:50 UTC 版)
Georges GonthierのチームがSsreflect(small scale reflectionの略)というCoqの拡張を開発している。拡張はreflection用の機能にとどまらず、Coqの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。Ssreflectの機能には下のようなものがある。 保守性を高めるための機能Coqが自動生成した識別子をユーザが指定できなくなって、Coqのバージョンアップによって証明が通らなくなることを防止する機能 証明の枝を完結させることを明示して、軽微な証明を自動で行わせられる上に、証明が通らなくなったときに修正するべき範囲がわかりやすくなる機能 主張を直接証明する代わりに、Coq内で検証済みの判定機を実行するreflectionという技法に特化した証明タクティク 有限集合上の和や積などの大きな演算子を扱う機能 代数のライブラリ SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く。
※この「Ssreflect拡張」の解説は、「Coq」の解説の一部です。
「Ssreflect拡張」を含む「Coq」の記事については、「Coq」の概要を参照ください。
ウィキペディア小見出し辞書の「Ssreflect拡張」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- Ssreflect拡張のページへのリンク
