Найти инвариант цикла этого простого алгоритма

#algorithm #nested-loops #pseudocode #discrete-mathematics #loop-invariant

#алгоритм #вложенные циклы #псевдокод #дискретная математика #инвариант цикла

Вопрос:

Я уверен, что это действительно простой вопрос, но, похоже, я не могу его взломать. Докажите правильность вашего алгоритма; т. Е. Укажите его инвариант цикла и докажите это с помощью индукции.

Ниже приведен мой алгоритм. Я знаю, как выполнить вторую часть (доказать индукцией), но я просто не могу определить инвариант цикла на всю жизнь.

 procedure intersection(A,B: list of integers)

  C= empty list
  for i:=1 to n:
    for j:= 1 to m:
      if Ai = Bj
        if Ai not in C
          C.append(Ai)
  return C

Ответ №1:

Чтобы вы начали, я просто указываю один из инвариантов цикла, чтобы не отказываться от решения полностью. Инвариант для внешнего цикла равен:

 C = intersection (B, {a1, ..., ai})

Вам также понадобится инвариант для внутреннего цикла.