在另一个模块中调用函数时不满足前提条件
提问于 2019-11-18 03:21:12
我正在尝试调用另一个模块中的函数，该模块负责确保保留堆上的前/后条件。具体地说，它确保在调用read之前传入的字符串是“可读的”：
val readableFiles : ref fileList
let readableFiles = ST.alloc []
let checkedRead f =
if canRead !readableFiles f
then read f
else failwith "unreadable"这允许它满足读取前提条件，该前提条件的定义如下：
let canRead (readList : fileList) (f : filename) =
Some? (tryFind (function x -> x = f) readList)
type canRead_t f h = canRead (sel h readableFiles) f == true
val read : f:filename -> All string
(requires (canRead_t f)) (ensures (fun h x h' -> True))
let read f = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f当我创建一个主函数并调用checkedRead "file"时，它工作得很好，但是当我试图在另一个模块中使用这个模块时，它报告以下错误：
TestAccess.fst(34,11-34,19): (Error 19) assertion failed (see also <fstar_path>/fstar/ulib/FStar.All.fst(36,40-36,45))
Verified module: TestAccess (3912 milliseconds)如果您尝试在不使用checkedRead的情况下直接调用read (在主文件中)，则会看到相同的错误，这意味着编译器不相信前提条件得到满足。
如果我在另一个文件中复制checkedRead (并且只复制该函数)，它就能正常工作。因此，编译器似乎无法推断这是否满足跨越模块边界的条件。
如何使用其他文件中的checkedRead函数，而不必在本地重新定义它？
回答 2
Stack Overflow用户
回答已采纳
发布于 2019-11-18 15:44:15
遵循Nik Swamy的建议，我向checkedRead添加了一个类型注释，解决了这个问题：
val checkedRead : filename -> All string
(requires (fun h -> True)) (ensures (fun h x h' -> True))
let checkedRead f =
if canRead !readableFiles f
then read f
else failwith "unreadable"Stack Overflow用户
发布于 2019-11-18 15:10:16
你能发布一个完整的例子吗？
提示:注释顶级函数的类型是一个很好的实践。这将帮助您确认F*推断的类型是您期望的类型，这在诊断这些类型的验证失败时会很有帮助。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/58907581
复制相关文章
点击加载更多
相似问题
如何在Angular JS中用gridOption-enableRowselection动态改变ui-grid
如何在angular.js ui-grid中动态更改子网格url
动态输入添加Angular.js
滚动到end to grid UI-Grid Angular js
如何动态更新angular ui-grid列的columnDef
添加站长 进交流群
领取专属 10元无门槛券
AI混元助手 在线答疑
关注 腾讯云开发者公众号
洞察 腾讯核心技术
剖析业界实践案例
腾讯云开发者
