Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
|
Ключевые концепции. [x]. Утверждения - это булевы выражения, задающие семантические свойства класса и вводящие аксиомы и предусловия соответствующего абстрактного типа данных
[x]. Утверждения - это булевы выражения, задающие семантические свойства класса и вводящие аксиомы и предусловия соответствующего абстрактного типа данных. [x]. Утверждения используются в предусловиях (требования, при выполнении которых программы применимы), постусловиях (свойства, гарантируемые на выходе программ), и инвариантах класса (свойства, характеризующие экземпляры класса во время их жизни). Другими конструкциями, включающими утверждения, являются инварианты цикла и инструкции check. [x]. Предусловие и постусловие программы описывают контракт между программой и ее клиентами. Контракт связывает программу, только при условии ее вызова, в состоянии, где предусловие выполняется; в этом случае программа гарантирует выполнимость постусловия на выходе. Понятие заключения контрактов между программами обеспечивает мощную метафору при построении надежного ПО. [x]. Инвариант класса выражает семантические ограничения экземпляров класса. Инвариант неявно добавляется к предусловиям и постусловиям каждой экспортируемой программы класса. [x]. Класс описывает одну возможную реализацию АТД; отображение класса в АТД выражается функцией абстракции, обычно частичной. Обратное отношение, обычно, не задается функцией. [x]. Инвариант реализации, - часть инварианта класса - выражает корректность представления классом соответствующего АТД. [x]. Цикл может иметь инвариант цикла, позволяющий вывести результат выполнения цикла, и вариант, позволяющий доказать завершаемость цикла. [x]. Если класс поставляется с утверждениями, то можно формально определить, что означает корректность класса. [x]. Утверждения служат четырем целям: помогают в конструировании корректных программ; помогают в создании документации, помогают в отладке, являются основой механизма исключений. [x]. Язык утверждений в нашей нотации не включает логику предикатов первого порядка, но может выражать многие свойства высокого уровня благодаря вызову функций. Функции, включаемые в утверждения должны быть простыми и безупречно корректными. [x]. Комбинация инвариантов и динамических псевдонимов приводит к Непрямому Эффекту Инварианта, который может стать причиной нарушения инварианта при корректности самого класса.
|