Отсутствует инвариант в коде Дафни, включающем последовательности

Мне интересно, есть ли причина, по которой Дафни не может проверить мою программу?

https://rise4fun.com/Dafny/Ip1s

Я пропустил какой-то дополнительный инвариант?

Стоит ли изучать 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 называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
0
0
91
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Проблема в том, что ваше определение s и ваша конструкция o идут в «разных направлениях». Рекурсивный случай s определяет s(i) с точки зрения i[0] и то, что «ранее» определено s(i[1..]). Напротив, итерация цикла определяет новый o с точки зрения i[n] и предыдущего значения o. Потребуется индуктивно доказанная лемма, чтобы установить обязательства доказательства в вашей текущей программе, и Дафни не изобретает такие леммы сам по себе.

Для записи в этом ответе вот с чего вы начали:

function s(i: seq<int>): seq<int> {
  if |i| == 0 then [] else 
    if i[0] == 42 then [i[0]] + s(i[1..])
    else s(i[1..])
}

method q (i: seq<int>) returns (o: seq<int>)
  ensures o == s(i)
{
  var n := 0;
  o := [];

  while n < |i|
    invariant n <= |i| && o == s(i[..n])   
  {
    if i[n] == 42 {
      o := o + [i[n]];
    } 
    n := n + 1;
  } 
}

Есть четыре выхода.

Один из выходов — определить другую версию s, назовем ее s', которая рекурсирует с другого конца заданной последовательности. Затем замените s на s' в спецификации метода и инварианте цикла. Это прекрасное решение, если по какой-то причине вы действительно не предпочитаете s, а не s', в спецификации вашего метода.

Второй выход — определить такой s' и доказать лемму, что s(i) и s'(i) возвращают одно и то же значение. Это позволит вам сохранить s в спецификации метода за счет наличия двух определений функций и необходимости писать (и доказывать и использовать) лемму.

Третий выход — изменить цикл так, чтобы он выполнялся «вниз», а не «вверх». То есть запустите n с |i| и уменьшите значение n в теле цикла. (Как обычно, приращение n обычно лучше всего выполнять в конце тела цикла (пост-инкремент), тогда как уменьшение n обычно лучше всего выполнять в начале тела цикла (до декремента).)

Четвертый выход — изменить способ написания инварианта цикла для o. В настоящее время инвариант говорит о том, что вы уже вычислили, то есть o == s(i[..n]). Вместо этого вы можете написать инвариант с точки зрения того, что еще предстоит вычислить, как в o + s(i[n..]) == s(i), который вы можете прочитать как «как только я добавлю s(i[n..]) к o, у меня будет s(i)». Вот эта версия q:

method q(i: seq<int>) returns (o: seq<int>)
  ensures o == s(i)
{  
  var n := 0;
  o := [];

  while n < |i|
    invariant n <= |i| && o + s(i[n..]) == s(i)
  {
    if i[n] == 42 {
      o := o + [i[n]];
    } 
    n := n + 1;
  } 
}

Вам также может быть интересно посмотреть этот выпуск Verification Corner на эту тему.

Рустан

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