1611678431-0e68e83522cb9d960ac896aa5d90854d (826635), страница 10
Текст из файла (страница 10)
Пусть дляфрагмента программы имеет место{}, и пусть утверждениеТогда имеет место {оператора присваиваниясильнее, а утверждениеслабее}. Например, из рассмотренных выше свойствможно вывести свойства:.,.Правило вывода свойств последовательности операторов имеет следующийвид. Пусть и-- последовательности операторов, обладающие соответственносвойствами {}и{последовательности}. Тогда дляимеет место свойство {}.В качестве примера применения метода промежуточных утверждений покажем,чтолюбых целых чисел A и BдляПо аксиоме оператора присваивания имеем следующие свойства операторов,составляющих анализируемую последовательность:.Применяя правило вывода следствий, из последнего свойства получаем.Отсюда и из первых двух свойств по правилу вывода свойствпоследовательности операторов получаем: сначала -,а затем -.Аналогичными правилами можно доказывать правильность программ.
Дляэтого в ходе доказательства следует проверять, что представленные программойпоследовательности операций на соответствующих состояниях памяти могутбыть выполнены. Такая проверка для всех рассмотренных языковыхконструкций сводится к анализу значений выражений на состояниях памяти,заданных с помощью утверждений, и во многих конкретных случаях легкореализуется.В дальнейшем в тексты программ мы будем включать утверждения, размещаяих в скобках комментариев.
Такие формализованные комментарииназываются аннотациями; они определяют те свойства состояний, которыесправедливы в соответствующие моменты выполнения программы.Аннотированная программа может выступать в качестве доказательства своейправильности. Например, программувозведения в десятую степень можнодополнить следующими аннотациями:module X10D;var A,B : integer;begin (*read(A);*)(* {}*)B := A A; (* {}*)B := B B; (*{}*)B := B A; (* {}*)B := B B; (*{write(B) (* {end X10D.}*)}*)Нетрудно убедиться, что программа удовлетворяет спецификации "Быстроевозведение в десятую степень", просто показав для каждой тройки (аннотация1,оператор, аннотация2) справедливость свойства {утверждение1} оператор{утверждение2} и соответствующего свойства завершаемости. Вместе с темследует отметить, что программа Xперегружена утверждениями и часть ееаннотаций очевидна и легко восстановима из текста программы.
Это говорит отом, что не обязательно включать в текст программы все известные вамутверждения о программе; нужно вставлять достаточно утверждений, чтобыпрограмма стала понимаемой, однако не так много, чтобы она затерялась в них.Следующий пример показывает, что иногда при описании свойств программудобно использовать дополнительные ("внепрограммные") переменные.Рассмотрим следующую старинную задачу о переправе на другой берег волка,козы и капусты. На левом берегу реки находятся лодочник с лодкой, волк, козаи капуста.
Их нужно переправить на правый берег. Лодка, помимо лодочника,вмещает лишь одного из троих (волка, козу или капусту). При этом нельзяоставлять наедине волка с козой, а также козу с капустой. Правильностьследующего решения этой задачи очевидна из аннотаций, использующих дведополнительные переменные ЛевыйБерег и ПравыйБерег:module ПЕРЕПРАВА;begin(*{ЛевыйБерег=(лодочник, волк, коза, капуста), ПравыйБерег=()}*)writeln('Перевезти козу.');(*{ЛевыйБерег=(волк, капуста), ПравыйБерег=(лодочник, коза)}*)writeln('Переправиться без груза.');(*{ЛевыйБерег=(лодочник, волк, капуста), ПравыйБерег=(коза)}*)writeln('Перевезти волка.');(*{ЛевыйБерег=(капуста), ПравыйБерег=(лодочник, волк, коза)}*)writeln('Перевезти козу.');(*{ЛевыйБерег=(лодочник, коза, капуста), ПравыйБерег=(волк)}*)writeln('Перевезти капусту.');(*{ЛевыйБерег=(коза), ПравыйБерег=(лодочник, волк, капуста)}*)writeln('Переправиться без груза.');(*{ЛевыйБерег=(лодочник, коза), ПравыйБерег=(волк, капуста)}*)writeln('Перевезти козу.')(*{ЛевыйБерег=(), ПравыйБерег=(лодочник, волк, коза, капуста)}*)end ПЕРЕПРАВА.24.
Механизм подпрограмм, простая структура вызовов-возвратов, задачи, сопрограмма иподпрограммы прерыванияПодпрограммы: функции и процедуры6.1.1 Описание и вызов процедурыМожет случиться, что некоторый составной оператор должен появиться внескольких местах программы. Чтобы программисту не приходилось тратитьвремя на повторную запись этого оператора, в языке Zonnonпредусматриваются средства для оформления оператора в видеподпрограммы, называемой процедурой. Программист имеет возможностьприписать составному оператору некоторый идентификатор (имя процедуры) ииспользовать это имя в качестве сокращенной записи в тех местах, где долженпоявиться (исполниться) составной оператор. Процедура задается описанием,которое должно находиться в программе после раздела описаний переменных.Использование имени процедуры в качестве сокращенной записиназывается оператором процедуры (или вызовом процедуры).Ниже приводится пример программы, которая осуществляет сложение двухвещественных чисел с хорошим оформлением печати (линия разделяетслагаемые и результат, по две линии рисуется выше и ниже слагаемых ирезультата) и включает в себя процедуру Линия.
Цель этой процедуры -рисование линии многократной выдачей символа "минус".module СуммаДвухЧисел;const N = 100;var Число1, Число2, Сумма : Real; I : 1..N;procedure Линия;beginfor I := 1 to N do write('-') end;writelnend Линия;beginread(Число1, Число2);Сумма := Число1 + Число2; Линия; Линия;writeln(Число1); writeln(Число2); Линия;writeln(Сумма); Линия; Линияend СуммаДвухЧисел.Здесь, как и обычно, описание процедуры состоит из двух частей: заголовкапроцедуры (первая строка в описании процедуры Линия) и тела процедуры(составной оператор в описании процедуры Линия).
Процедура Линиядостаточно проста, но она позволила сделать программу короче текстуально; спроцедурой программу стало легче читать, понимать и модифицировать.Например, пусть требуется рисовать не линию, а строку с чередующимисясимволами "звездочка" и "минус". Тогда, хотя имеются пять вызовов процедурыЛиния, изменение в программу необходимо внести только в одно место в телепроцедуры:procedure Линия;beginfor I := 1 to N div 2 do write(' -') end;if Odd(N) then write(' ')end;writelnend Линия;Другой вид подпрограммы в языке Zonnon -- это уже использованные намиранее функции (подробно мы будем рассматривать функции в п. 6.1.5).
Важноеотличие подпрограммы-функции от подпрограммы-процедуры состоит в том,что обращения к функциям являются выражениями, а вызовы процедур -операторами. Другими словами, функция -- это новая операция, определяемаяпрограммистом в своей программе, а процедура -- это новый (определенныйпрограммистом) оператор.Механизм подпрограмм -- это мощное средство абстракции, позволяющеерасширить язык путем включения новых операций и операторов. В языкеZonnon мы часто сталкиваемся со средствами абстракции. Например, когда ввыражении нами используется операция сравнения двух целых чисел, мы, какправило, совсем не интересуемся тем, как она выполняется на конкретной ЭВМ,предполагая только, что она выполняется правильно.
Подобным же образом,записывая вызов подпрограммы, мы исходим лишь из того, что подпрограммаделает, и не уделяем внимания тому, как она это делает реально. Другимисловами, при описании подпрограммы основное выделяемое свойство -- это то,что делает подпрограмма, а главное из тех свойств, которые желательноопустить из рассмотрения, -- это то, как она это делает. Если рассматриватьпрограмму как конструктивное доказательство теоремы о том, что внешняяспецификация непротиворечива и вычислима, то подпрограмма -- это лемма,используемая в таком конструктивном доказательстве.Подпрограмма (англ.
subroutine) — поименованная или иным образом идентифицированнаячасть компьютерной программы, содержащая описание определённого набора действий.Подпрограмма может быть многократно вызвана из разных частей программы. В языкахпрограммирования для оформления и использования подпрограмм существуют специальныесинтаксические средства.Назначение подпрограмм.Подпрограммы изначально появились как средство оптимизации программ по объёму занимаемойпамяти — они позволили не повторять в программе идентичные блоки кода, а описывать иходнократно и вызывать по мере необходимости.
К настоящему времени данная функцияподпрограмм стала вспомогательной, главное их назначение — структуризация программы сцелью удобства её понимания и сопровождения.Выделение набора действий в подпрограмму и вызов её по мере необходимости позволяетлогически выделить целостную подзадачу, имеющую типовое решение. Такое действие имеетещё одно (помимо экономии памяти) преимущество перед повторением однотипных действий:любое изменение (исправление ошибки, оптимизация, расширение функциональности),сделанное в подпрограмме, автоматически отражается на всех её вызовах, в то время как придублировании каждое изменение необходимо вносить в каждое вхождение изменяемого кода.Даже в тех случаях, когда в подпрограмму выделяется однократно производимый набордействий, это оправдано, так как позволяет сократить размеры целостных блоков кода,составляющих программу, то есть сделать программу более понятной и обозримой...Механизм подпрограмм, их описание и вызовВ простейшем случае (в ассемблерах) подпрограмма представляет собой последовательностькоманд (операторов), отдельную от основной части программы и имеющую в конце специальнуюкоманду выхода из подпрограммы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
