文件名称：FStar：有效程序的验证系统
文件大小：9.4MB
文件格式：ZIP
更新时间：2024-03-04 10:14:03
programming-language dependent-types ocaml theorem-proving verification
F *：有效程序的验证系统 F *网站 有关F *的更多信息，请访问 安装 参见 教程 提供了中经过验证的编程的初步体验，并通过示例进行了解释。 维基 包含有关其他（通常是更深入的）技术文档。 编辑F *代码 您可以使用自己喜欢的文本编辑器编辑F *代码，但是Emacs，Visual Studio Code，Atom和Vim的扩展添加了对F *的特殊支持，例如语法突出显示，代码完成，快速导航，类型提示和交互式发展。 上有关更多详细信息。 您也可以使用的器直接在浏览器中编辑简单示例。 提取并执行F *代码 默认情况下，F *仅验证输入代码，而不编译或执行输入代码。 要执行F *代码，需要使用F *的代码提取工具将其转换为OCaml或F＃，这是使用命令行参数--codegen OCaml或--codegen FSharp调用的。 有关在上更多详细信息。 此外，可以通过将编写在类似C的浅层嵌