首页| JavaScript| HTML/CSS| Matlab| PHP| Python| Java| C/C++/VC++| C#| ASP| 其他|
购买积分 购买会员 激活码充值

您现在的位置是:虫虫源码 > 其他 > 一个翻译的火花/艾达软件验证条件

一个翻译的火花/艾达软件验证条件

资 源 简 介

Verification conditions (VCs) are logical statements that, if proven, formally guarantee the programs they are generated from satisfy certain correctness conditions. For example, the guarantees can be for the absence of run-time errors such as overflows and array bounds violations. SPARK is an Ada subset which adds in an annotation language for expressing program properties. Victor reads in VCs generated from SPARK programs using the SPARK toolset from Altran Praxis and AdaCore. It translates these VCs into the input formats of popular theorem provers, and can automatically run these provers on the translated VCs. Currently it translates to the standard SMT-LIB language used by many SMT solvers, API calls for the CVC3 and Yices SMT solvers, theory files for the Isabelle/HOL interactive theorem prover. The SPARK toolset includes tools for proving VCs. Victor augments and complements the capabilities of these tools.

文 件 列 表

vct-0.9.1
LICENSE.txt
run
doc
CHANGES.txt
COPYING.txt
src
bin
vc
README.txt

相 关 资 源

您 可 能 感 兴 趣 的

同 类 别 推 荐

VIP VIP