dafny - 错误：无法编译假设语句

Question

我正在尝试一次从文件中读取一定数量的字节（如果我一次读取整个文件，则效果很好）。我ReadLemma在下面的代码中添加了引理 ( 以帮助摆脱 while 循环中的修饰符子句错误，但现在我得到了Error: an assume statement cannot be compiled. 关于如何解决此问题的任何想法？

include "Io.dfy"
lemma ReadLemma(fs: FileStream, file_offset: nat32, buffer: array?<byte>, num_bytes: int32)
    requires fs.IsOpen();
    requires fs.env.Valid();
    requires fs.env.ok.ok();
    requires fs.Name() in fs.env.files.state();
    ensures fresh(buffer);
{ 
    assume false;
}
method {:main} Main(ghost env: HostEnvironment?)
    requires env != null && env.Valid() && env.ok.ok()
    modifies env.ok
    modifies env.files
{
    var argc := HostConstants.NumCommandLineArgs(env);
    if argc != 3 {
       print "[USAGE]: mono cp.exe SrcFilename DstFilename!\n";
       return;
    }

    var src := HostConstants.GetCommandLineArg(1, env);
    var dst := HostConstants.GetCommandLineArg(2, env);
    var srcResult := FileStream.FileExists(src, env);
    var dstResult := FileStream.FileExists(dst, env);
    if !srcResult {
       print "Source File Does Not Exist!\n";
       return;
    }
    if dstResult {
       print "Destiny File Already Exist!\n";
       return;
    }

    var srcSuccess, srcFs := FileStream.Open(src, env);
    if !srcSuccess {
       print "Failed to open src file!\n";
       return;
    }
    var dstSuccess, dstFs := FileStream.Open(dst, env);
    if !dstSuccess {
       print "Failed to open dst file!\n";
       return;
    }

    var success, len: int32 := FileStream.FileLength(src, env);
    if !success {
       print "Couldn't get stream size!\n";
       return;
    }

    var BYTES_TO_READ := 256;
    var file_offset, buffer, start, srcOk, dstOk := 0, new byte[BYTES_TO_READ], 0, true, true;

    while file_offset as int + BYTES_TO_READ as int < len as int
       decreases len as int - (file_offset as int + BYTES_TO_READ as int);
       invariant srcFs.IsOpen() && srcFs.env.Valid() && srcFs.env.ok.ok()
       invariant srcFs.Name() in srcFs.env.files.state()
    {
       ReadLemma(srcFs, file_offset as nat32, buffer, BYTES_TO_READ);
       srcOk := srcFs.Read(file_offset as nat32, buffer, start, BYTES_TO_READ);
       dstOk := dstFs.Write(file_offset as nat32, buffer, start, BYTES_TO_READ);
       file_offset := file_offset + BYTES_TO_READ;
    }
}

Read 函数是从文件中读取的函数。正如我所说，如果我阅读文件的全部内容，它工作正常。没有引理，我得到这个错误call may violate context's modifies clause。

标签： dafny