У меня возникли проблемы с поиском инварианта для приведенного ниже алгоритма. Кроме того, мне нужно выполнить все шаги, чтобы доказать, как я нахожу конкретный инвариант, и я не знаю, как я могу это продемонстрировать. Я видел, что этот алгоритм представляет собой умножение сложением.
Алгоритм:
alg1(integer a,b)
x<-a
y<-b
z<-0
while y>0 do
z<-z+x
y<-y-1
end while
return z
Я надеюсь, что кто-то может помочь мне пролить свет на это, поскольку подобных случаев, которые я нашел здесь, было недостаточно.
Большое спасибо заранее за ваше время.
