Что такое индуктивный инвариант для этого куска кода?

Question

Для этого куска кода:

  // n is a user input that can be any integer
  s = 0
  i = 0

  while i < n:
    s = s + 1
    i = i + 1

  return s

Я хотел бы доказать, что условие публикации if n > 0 then s = sum(0, n) else s = 0, где sum(s,e) просто добавляет 1 из s в e эксклюзив, начиная с начальное значение 0.

Я думал, что инвариант if n > 0 and i < n then s = sum(0, i) else s = 0, но я не могу его доказать в Coq или z3. Есть намеки?

Answer 1

Вы, похоже, подразумеваете, что этот алгоритм вычисляет сумму, но на самом деле он этого не делает. Вместо этого он будет рассчитывать до n. Возможно, вы предполагали:

i = 0
s = 0
while i < n:
  i = i+1
  s = s+i

Обратите внимание, что мы увеличиваем s на i, а не на 1, как в вашей программе.

Предполагая, что это предполагаемая программа, тогда хорошим инвариантом будет:

• s - сумма всех чисел до и включая i
• i - самое большее n

В более программных c нотациях:

s == i*(i+1)/2 && i <= n

Чтобы понять почему, помните, что инвариант должен удерживаться до и после каждой итерации l oop; и когда условие l oop ложно, оно должно подразумевать ваше постусловие. Вот почему вам нужно соединение i <= n, чтобы при выходе из l oop, s действительно содержало сумму.

Answer 2

Как насчет этого решения:

// Function left unimplemented, for simplicity
function sum(s: Int, e: Int): Int
  ensures result == e - s

method foo(n: Int) returns (s: Int)
  requires 0 <= n
{
  var i: Int := 0
  s := 0

  while (i < n)
    invariant s == n - sum(i, n)
  {
    s := s + 1
    i := i + 1
  }
}

Язык и инструмент называются Viper . Вы можете попробовать ваш пример в Интернете (веб-интерфейс несколько медленный и нестабильный) или использовать плагин VSCode .