Я пытаюсь прочитать из файла определенное количество байтов за раз (если я прочитаю весь файл за один раз, это нормально работает). Я добавил лемму (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;
}
}
Функция чтения - это функция, которая читает из файла. Как я уже сказал, все работает нормально, если я прочитаю все содержимое файла. Без леммы я получаю эту ошибку call may violate context's modifies clause
.
Выход состоит в том, чтобы убрать утверждение assume
и доказать лемму. В вашем случае это будет невозможно, потому что постусловие леммы обещает выделить новый buffer
, а леммам не разрешено выделять состояние. (Об этом должно быть предупреждение.) Вероятно, вы хотите полностью избавиться от леммы и выяснить, что изменяется в цикле, что не может быть изменено включающим методом. Я предлагаю вам взглянуть на пункты modifies
в Read
и Write
.
Спасибо, @RustanLeino!
Утверждение
assume
предписывает верификатору слепо принять указанное вами условие. Это полезно в качестве временной меры, чтобы заставить верификатора сосредоточиться на определенных частях или путях вашей программы.assume false
похож на "TODO". Пока у вас естьassume
где-то в вашей программе (в том числе в лемме), значит, вы не проверили правильность своей программы, и компилятор жалуется на это.