Замечание математического характера

Повторное объявление функции как атрибута

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

Атрибут доступен всегда, а потому мы вправе считать, что его предусловие равно True. В итоге можно полагать, что предусловие атрибута, согласно правилу Утверждения Переобъявления, было ослаблено.

Но атрибут не имеет постусловий. Мы же должны гарантировать, что он наделен всеми свойствами, заданными исходной функцией. Поэтому (в дополнение к правилу Утверждения Переобъявления) будем считать, что в этом случае автоматически постусловие добавляется к инварианту класса. Плоская форма класса будет содержать это условие в составе своего инварианта.

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

Неформально, правило Утверждения Переобъявления гласит: "Повторное объявление утверждений может лишь сужать область допустимого поведения, не нарушая ее". Сейчас, завершая обсуждение этой темы, приведем строгую формулировку данного свойства.

Пусть подпрограмма реализует частичную функцию r, отображающую множество возможных входных состояний I в множество возможных выходных состояний O. Утверждения подпрограммы определяют правила действия r и ее возможных переопределений.

[x]. Предусловие задает область определения DOM функции r (подмножество I, на котором r гарантированно вырабатывает результат).

[x]. Постусловие задает для каждого x из DOM подмножество RESULTS(x) множества O, такое, что r (x)

RESULTS (x). Так как постусловие не всегда однозначно описывает результат, это подмножество может иметь больше одного элемента.

Правило Утверждения Переобъявления означает, что повторное объявление может расширять область определения и сужать множество результатов. Пометив новые множества знаком ', запишем требования, закрепленные этим правилом:

DOM' DOM

RESULTS' (x) RESULTS (x) для всех x из DOM

Предусловие устанавливает, что подпрограмма и ее повторные объявления, как минимум, должны принимать некоторые входы (DOM), хотя повторные объявления могут это множество и расширить. Постусловие говорит, что результаты, возвращаемые подпрограммой и ее повторными объявлениями, могут, самое большее, содержать значения из RESULTS(x), однако, постусловия при повторных объявлениях могут это множество сузить.

В этом описании состояние системы в период выполнения определяется состоянием (значениями) всех достижимых объектов. Кроме того, входные состояния (элементы I) также включают в себя значения аргументов. Более подробное введение в математическое описание программ и языков программирования см. в [M 1990].

Дата добавления: 2014-01-07