Ошибка: оператор предположения не может быть скомпилирован

Я пытаюсь прочитать из файла определенное количество байтов за раз (если я прочитаю весь файл за один раз, это нормально работает). Я добавил лемму (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 предписывает верификатору слепо принять указанное вами условие. Это полезно в качестве временной меры, чтобы заставить верификатора сосредоточиться на определенных частях или путях вашей программы. assume false похож на "TODO". Пока у вас есть assume где-то в вашей программе (в том числе в лемме), значит, вы не проверили правильность своей программы, и компилятор жалуется на это.

Rustan Leino 30.11.2018 19:40

Выход состоит в том, чтобы убрать утверждение assume и доказать лемму. В вашем случае это будет невозможно, потому что постусловие леммы обещает выделить новый buffer, а леммам не разрешено выделять состояние. (Об этом должно быть предупреждение.) Вероятно, вы хотите полностью избавиться от леммы и выяснить, что изменяется в цикле, что не может быть изменено включающим методом. Я предлагаю вам взглянуть на пункты modifies в Read и Write.

Rustan Leino 30.11.2018 19:46

Спасибо, @RustanLeino!

Rui Maranhao 01.12.2018 21:49
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
3
380
0

Другие вопросы по теме