Докажи, как работает алгоритм

Question

Учитывая псевдокод

MUL(a,b) 
    x=a 
    y=0 
    WHILE x>=b DO 
     x=x-b 
     y=y+1 
    IF x=0 THEN 
     RETURN(true) 
    ELSE 
     RETURN(false) 

Я должен доказать, как алгоритм работы.

До сих пор я только объяснил, как это работает, но я не уверен, как вы должны доказать , как это работает.

Редактировать: Просто уточнить. Я задал вопрос this в другой теме. Но два вопроса разделены. Задача, над которой я работаю, состоит из 3-х вопросов. Первый вопрос заключается в том, где я объяснил, как работает алгоритм. Второй вопрос касается моего другого thread, и третий вопрос (этот поток) - это то, где я должен доказать, как работает алгоритм, который я объяснил в вопросе 1. Причина, по которой я задал этот вопрос, заключается не в том, чтобы получить ответ на этот вопрос, а просто в объяснении того, что меня просят сделать, поскольку я не могу понять это сам. Лично я бы сделал то же самое, что и первый вопрос, но это не имело бы большого смысла.

Answer 1

Попробуйте показать предварительное условие и послесловие алгоритма. Предварительное условие предикаты исходного состояния перед исполнением, а пост-условие предикаты конечного состояния после выполнения.

Алгоритм правилен, если можно доказать, что если предварительное условие истинно, пост-условие должно быть истинным.

проверить это для более подробной информации: prove how algorithm works