Правило языка

Правило языка

Правило Утверждений Переобъявления, так как оно сформулировано, является концептуальным руководством. Как преобразовать его в безопасное и проверяемое правило языка?

В принципе, чтобы убедиться в том, что старые предусловия влекут новые, а новые постусловия - старые, следует провести логический анализ тех и других утверждений. К сожалению, это требует наличия сложного механизма доказательства теорем (несмотря на десятилетия исследований в области искусственного интеллекта). Его применение в компиляторе пока не реально.

К счастью, возможно простое техническое решение. Нужное нам правило можно сформулировать через простое лингвистическое соглашение, основанное на том наблюдении, что для любых утверждений a и b:

[x]. влечет or ? независимо от значения ?;

[x]. ? and влечет ? независимо от значения .

Итак, гарантируется, что новое предусловие слабее исходного либо равно ему, если оно имеет вид or ?. Гарантируется, что новое постусловие сильнее исходного ? либо равно ему, если оно имеет вид ? and . Отсюда следует искомое языковое правило:

Правило (2) Утверждения Переобъявления

При повторном объявлении подпрограммы нельзя использовать предложения require или ensure. Вместо них следует использовать предложение, начинающееся с:

[x]. require else, объединенное с исходным предусловием логической связкой or

[x]. ensure then, объединенное с исходным постусловием логической связкой and.

При отсутствии таких предложений действуют исходные утверждения.

Заметим, что используются нестрогие булевы операторы and then и or else, а не обычные and и or, хотя чаще всего это различие несущественно.

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

invert (epsilon: REAL) is

-- Обращение текущей матрицы с точностью epsilon

require

epsilon >= 10 ^ (-6)

...

ensure

((Current * inverse) |-| One) <= epsilon

мы не вправе в повторном объявлении использовать require и ensure, поэтому результат

примет вид

...

require else

epsilon >= 10 ^ (-20)

...

ensure then

((Current * inverse) |-| One) <= (epsilon / 2)

а стало быть, предусловие формально станет таким: (epsilon >= 10 ^ (-20)) or else (epsilon >= 10 ^ (-6)).

Ситуация с постусловием аналогична. Такое расширение не имеет особого значения, поскольку преобладает более слабое предусловие или более сильное постусловие. Если ? влечет , то or else ? имеет то же значение, что и . Если ? влечет , то ? and then имеет то же значение, что и ?. Поэтому математически предусловие повторного объявления есть: epsilon >= 10 ^ (-20), а его постусловие есть: ((Current * inverse) |-| One) <= (epsilon / 2), хотя запись утверждений в программе (а также, вероятно, их расчет во время выполнения при отсутствии средств символьных преобразований) является более сложной.

Поделитесь на страничке

Следующая глава >

Похожие главы из других книг

3.1. Назначение языка UML

Из книги Самоучитель UML автора Леоненков Александр

3.1. Назначение языка UML Язык UML предназначен для решения следующих задач: 1. Предоставить в распоряжение пользователей легко воспринимаемый и выразительный язык визуального моделирования, специально предназначенный для разработки и документирования моделей сложных


9. Константы языка СИ

Из книги Программирование автора Козлова Ирина Сергеевна

9. Константы языка СИ Константы – это перечисление величин в программе. В языке СИ можно выделить четыре вида констант: целые константы, константы с плавающей запятой, символьные константы и строковые литералы.Целая константа – это десятичное, восьмеричное или


23. Операции языка СИ++

Из книги Язык программирования С# 2005 и платформа .NET 2.0. [3-е издание] автора Троелсен Эндрю

23. Операции языка СИ++ C++ обладает богатым набором операций, которые позволяют в выражениях образовывать новые значения и изменять значения переменных. Поток управления в программе определяется с помощью операторов, а описания применяются для введения в программе имен


Роль языка C#

Из книги Искусство программирования для Unix автора Реймонд Эрик Стивен

Роль языка C# С учетом того, что принципы .NET так радикально отличаются от предшествующих технологий, Microsoft разработала новый язык программирования, C# (произносится "си-диез"), специально для использования с этой новой платформой. Язык C# является языком программирования, по


17.5.1. Переносимость и выбор языка

Из книги Windows Script Host для Windows 2000/XP автора Попов Андрей Владимирович

17.5.1. Переносимость и выбор языка Первым вопросом в программировании, обеспечивающем переносимость, является выбор языка реализации. Все основные языки, рассмотренные в главе 14, являются высоко переносимыми в том смысле, что совместимые реализации доступны на всех


ЭЛЕМЕНТЫ ЯЗЫКА СИ

Из книги Самоучитель Skype. Бесплатная связь через Интернет автора Яковлева Е. С.

ЭЛЕМЕНТЫ ЯЗЫКА СИ Под элементами языка понимаются его базовые конструкции, используемые при написании программ. В этом разделе описываются следующие элементы языка Си:– алфавит;– константы;– идентификаторы;– ключевые слова;– комментарии.Компилятор языка Си


Выбор языка

Из книги Linux: Полное руководство автора Колисниченко Денис Николаевич

Выбор языка Для того чтобы выбрать или изменить существующий язык интерфейса, используется команда основного меню программы Skype Инструменты | Выбор языка (language). В раскрывающемся списке данной команды (рис. 6.1) укажите язык, и тогда интерфейс программы будет


21.1.3. Опции языка

Из книги Firebird РУКОВОДСТВО РАЗРАБОТЧИКА БАЗ ДАННЫХ автора Борри Хелен

21.1.3. Опции языка Из всех опций языка мне пригодилась лишь опция ANSI, которая выключает все функции GNU С, несовместимые со стандартом ANSI. К таким функциям относятся asm, inline, typeof и


Элементы языка

Из книги Язык Си - руководство для начинающих автора Прата Стивен

Элементы языка В табл. 29.1 показаны элементы языка PSQL, доступные в Firebird.Таблица 29.1. Расширения PSQL для хранимых процедур и триггеров Оператор Описание В. 1.5 В. 1.0.x BEGIN ... END Определяет блок операторов, которые выполняются как одно целое. Зарезервированное слово BEGIN начинает


ПРОИСХОЖДЕНИЕ ЯЗЫКА СИ

Из книги Мир InterBase. Архитектура, администрирование и разработка приложений баз данных в InterBase/FireBird/Yaffil автора Ковязин Алексей Николаевич

ПРОИСХОЖДЕНИЕ ЯЗЫКА СИ Сотрудник фирмы Bell Labs Деннис Ритчи создал язык Си в 1972 г. во время совместной работы с Кеном Томпсоном над операционной системой UNIX. Ритчи не выдумал Си просто из головы — прообразом послужил язык Би, разработанный Томпсоном, который в свою


ДОСТОИНСТВА ЯЗЫКА СИ

Из книги автора

ДОСТОИНСТВА ЯЗЫКА СИ Язык Си быстро становится одним из наиболее важных и популярных языков программирования. Его использование все более расширяется, поскольку часто программисты предпочитают язык Си всем другим языкам после первого знакомства с ним. Когда вы изучите


БУДУЩЕЕ ЯЗЫКА СИ

Из книги автора

БУДУЩЕЕ ЯЗЫКА СИ Язык Си уже занимает доминирующее положение в мире мини-компьютеров, работающих под управлением ОС UNIX. Сейчас он распространяется на область персональных ЭВМ. Многие фирмы, производящие программное обеспечение, все чаще обращаются к Си, как к удобному


ИСПОЛЬЗОВАНИЕ ЯЗЫКА СИ

Из книги автора

ИСПОЛЬЗОВАНИЕ ЯЗЫКА СИ Си — язык "компилируемого" типа. Не огорчайтесь, если это звучит для вас пока как непонятный набор слов; вы поймете, что это значит, когда мы опишем этапы процесса создания работающей Си-программы.Если вы привыкли использовать какой-нибудь язык


11. Препроцессор языка Си

Из книги автора

11. Препроцессор языка Си ДИРЕКТИВЫ ПРЕПРОЦЕССОРА   СИМВОЛЬНЫЕ КОНСТАНТЫ    МАКРООПРЕДЕЛЕНИЯ И "МАКРОФУНКЦИИ"   ПОБОЧНЫЕ ЭФФЕКТЫ МАКРООПРЕДЕЛЕНИИ    ВКЛЮЧЕНИЕ ФАЙЛОВ    УСЛОВНАЯ