Элементы доказательного программирования - часть 4

·         разбор случаев;

·         подбор контрпримеров;

·         выделение лемм;

·         индуктивный вывод.

Разбор случаев применяется для анализа результатов выполнения конструкций альтернативного выбора. В качестве примера проведем анализ приведенного выше алгоритма «выбора» максимума трех чисел, содержащего выбор альтернатив.

 

алг «у = тах(а, b,с)»                                     Результаты

нач

если а > b то                                            при а > b

у := а                                                        у = а

инес b > с то                                            при b > с

у

:= b                                                        у = b

инес с > а то                                            при с > а

у

:= с                                                        у = с

кесли                                                          при не (b > с)

кон

 

Справа от алгоритма приведены результаты вычислений с указа­нием условий, при которых они получаются. На основании этих фактов можно заключить, что конечные результаты вычисления имеют три варианта:

а, при а > b,

у =       b, при b > с и b ³ а,

с, при с > а и с ³ b.

В то же время значение максимума должно быть равно:

а, при а ³ b и а ³ с,

mах =  b, при b ³

с и b ³

а,

с, при с ³ а и с ³ b.

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

Для опровержения общего утверждения достаточно указать хотя бы один контрпример. В данном случае утверждение о правильности алгоритма гласило бы: для любых значений переменных а, b, с конечным было бы значение mах (а, b, с).

Начало  Назад  Вперед