Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
|
Правило (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), хотя запись утверждений в программе (а также, вероятно, их расчет во время выполнения при отсутствии средств символьных преобразований) является более сложной.
Date: 2015-12-13; view: 389; Нарушение авторских прав |