Название: Доказательство правильности программ - Конспект лекций (Веретельникова Е.Л.)

Жанр: Экономика

Просмотров: 1604


3.4. особенности доказательства правильности программ, написанных на языках программирования visual basic и си

 

Нельзя не отметить, что в последнее время наиболее распространенными языками написания программ стали VisuaL Basic, Паскаль и Си. Поскольку, как уже было сказано выше, метод доказательства правильности программ, написанных на различных языках программирования, в принципе один и тот же, остановимся на некоторых особенностях используемых в них управляющих структур, неявно определяющих порядок выполнения программы, а также способах передачи параметров в подпрограммы, влияющих на доказательство правильности программ.

 

Особенности языка VisuaL Basic

 

Доказывая конечность и правильность программы на Visual Basic, в которой используются один или несколько видов циклов, необходимо помнить их основные особенности, а также обращать внимание на способ передачи параметров в подпрограммы:

1. Порядок действий при выполнении цикла. Так, в циклах Do While … Loop, Do Until … Loop и For … Next (циклы с предпроверкой условия или циклы, проверяемые вначале) проверка истинности условия происходит до выполнения операторов, составляющих тело цикла. Поэтому возможна ситуация, когда тело цикла не выполнится ни разу в случае невыполнения условия. В циклах Do … Loop While, Do … Loop Until (циклы с постпроверкой условия или циклы, проверяемые в конце) сначала выполняется тело цикла, после чего происходит проверка условия. Это означает, что данный цикл выполнится как минимум один раз, независимо от того, выполнено условие или нет.

2. Влияние истинности условия цикла. Циклы Visual Basic можно разделить также на две группы: Циклы Do While … Loop, Do … Loop While выполняются до тех пор, пока условие истинно (сюда же можно отнести и цикл For … Next, выполняемый, пока переменная цикла не достигнет конечного значения), и циклы, выполняющиеся до тех пор, пока условие ложно: Do Until … Loop и Do … Loop Until.

3. Способ передачи аргументов. при доказательстве правильности программ, содержащих обращение к подпрограммам, необходимо обращать внимание на способ передачи аргументов. Напомним, что в Visual Basic аргументы могут передаваться либо как ссылки (Byref), либо как значение (ByVal). В первом случае в подпрограмме возможно изменение значения этого аргумента и при доказательстве правильности необходимо проверять, было ли произведено такое изменение (см. пример 3.3). Во втором случае

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

 

Особенности языка Си

 

Доказывая конечность и правильность программы на Си, также необходимо обращать внимание на особенности языка, существенные для проверки правильности написанных на нем программ.

1. Циклы. В Си выделяют три вида циклов:

а) for (инициализация; проверка условия; изменение) оператор. Цикл for похож на аналогичные циклы в других языках программирования и выполняется до тех пор, пока условное выражение истинно, но в то же время этот оператор в языке Си стал гораздо более гибким и мощным. Так, в качестве параметра цикла теперь необязательно использовать целочисленный счетчик, поскольку можно получить цикл, из которого нет выхода (так называемый бесконечный цикл). Пример: for(I = 10; I > 6; I++). Появление

таких ситуации необходимо предупреждать при проверке конечности программы.

б) while (условие) оператор. Этот оператор цикла, как и в других языках, выполняется до тех пор, пока условие истинно и, как и цикл for, является циклом с предпроверкой условия. Соответственно тело цикла может не выполниться ни разу.

в) do-while. В отличие от вышеописанных, является циклом с постусловием (с постпроверкой условия) и тело цикла обязательно выполняется хотя бы один раз. Формат оператора

do {

последовательность операторов

} while (условие);

2. Способ передачи параметров. В Си возможна передача параметров в процедуру по значению, по ссылке и по адресу. Только в первом случае их значения в вызывающей программе не изменяются. Во втором и в третьем случаях при доказательстве правильности программ, содержащих обращение к подпрограммам, необходимо отдельно проверять, было ли произведено в подпрограмме изменение параметров.

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

Для закрепления полученных навыков рекомендуем выполнить вариант индивидуального задания по теме «Доказательство правильности методом индуктивных утверждений» c использованием любого языка программирования высокого уровня (visual Basic, Си, Паскаль или др.)