在F* (FStar)中验证简单程序时出错
提问于 2020-06-13 16:00:18
我使用的是F* 0.9.6.0，我无法让这个简单的程序通过子类型检查：
module Test
open FStar.String
let minlen s n = strlen s >= n
let maxlen s n = strlen s <= n
let isLanguageValid s = (minlen s 2) && (maxlen s 8)
type language = s : string { isLanguageValid s }
let english : language = "en"
let invalid : language = "abcdefghi"我希望english通过，但invalid失败。我尝试过的每一件事都会导致他们两人都被拒绝，或者两者都被接受。我做错了什么？对于这种类型，我只想接受一定长度的字符串。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-06-13 16:39:51
关于F*中字符串的推理是相当有限的。大多数证明要么要求将像strlen这样的函数视为未解释的函数，要么触发规范化的明智使用。
备注
[@@expect_failure]
let test = assert (strlen "English" == 7)
let test = assert_norm (strlen "English" == 7)这就是说，第一个断言在F*中是不可证明的--它辜负了验证者。
然而，第二个断言成功地要求F*使用规范化而不是SMT来证明它。
为了让您的程序进行验证，我将其修改如下：
let minlen s n = strlen s >= n
let maxlen s n = strlen s <= n
let isLanguageValid s = (minlen s 2) && (maxlen s 8)
type language = s : string { normalize_term #bool (isLanguageValid s) }
let english : language = "en"
[@@expect_failure]
let invalid : language = "abcdefghi"注意normalize_term在language定义中的使用。
您可以在这里阅读一些关于规范化等方面的内容：https://github.com/FStarLang/FStar/wiki/Using-SMT-fuel-and-the-normalizer
FYI，我的例子是关于F*的最新构建。最近的二进制构建可以在这里找到https://github.com/FStarLang/binaries/tree/master/weekly。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/62366907
复制相关文章
腾讯云开发者
