用于程序验证的 ML 系语言 FStar

用于程序验证的 ML 系语言 FStar

Apache
跨平台
微软
2017-03-15
王练

F* (发音 Fstar) 是一种用于程序验证的 ML 系语言,它的类型系统包括:

  • polymorphism

  • dependent types

  • monadic effects

  • refinement types

  • a weakest precondition calculus 

这些特性允许为程序表达精确而紧凑的规范,包括功能正确性和安全属性。以 F * 编写的程序可以转换为 OCaml、F#或 C 以供执行。

最新版本的 F * 完全用 F * 编写,在 OCamlF# 中引导。F * 正在使用的主要用例是在 Everest 项目中为整个 HTTPS 堆栈建立一个经过验证的插入式替换。

加载中

评论(0)

暂无评论

暂无资讯

暂无问答

暂无博客

返回顶部
顶部