Метод Хора доказательства правильности программ.

Идеи Флойда нашли дальнейшее развитие в аксиоматическом подходе к доказательству ПП, предложенном К. Хором. Первоначально система Хора была ориентирована на доказательство правильности так называемых While-программ, для которых операторы goto недопустимы.

Следуя Флойду, Хоор вводит утверждения относительно состояний переменных программы до и после выполнения одного или нескольких операторов, называемые пред- и пост-условиями соответственно. Эта форма определения семантики получила название «индуктивных выражений».

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

71. Содержание

    • Сущность и актуальность дисциплины «Технологии программирования», основные понятия и определения дисциплины.
    • Жизненный цикл программного средства.
    • Модели жизненного цикла по.
    • Модель с промежуточным контролем
    • Спиральная модель
    • Спиральная или итерационная схема разработки программного обеспечения
    • Изменение жизненного цикла программного обеспечения при использовании case-технологий.
    • Качество программного обеспечения.
    • Модели качества по
    • Метрики качества программного обеспечения.
    • Измерение и оценка качества по, стандартный метод оценки значений показателей качества.
    • Управление качеством пс.
    • Требования стандарта к организации системы качества
    • Диалоговые программы, типы диалога, формы диалога.
    • Спецификация пс.
    • Определение требований к программному средству.
    • Спецификация качества программного средства.
    • Функциональная спецификация программного средства.
    • Методы контроля внешнего описания программного средства.
    • Способы записи алгоритмов.
    • Представление основных структур алгоритмов.
    • Псевдокоды.
    • Flow-формы.
    • Диаграммы Насси-Шнейдермана.
    • Классификация структур данных.
    • Файловые структуры, физическая организация файлов.
    • Логическая организация файлов.
    • Документирование файлов.
    • Модульные программы, модули и их свойства.
    • Сцепление и связность модулей.
    • Нисходящая и восходящая разработка программного обеспечения.
    • Программирование «с защитой от ошибок».
    • Основные подходы программирования, «стихийное» программирование.
    • Основные подходы программирования, структурный подход к программированию.
    • Основные подходы программирования, объектный подход к программированию.
    • Основные подходы программирования, компонентный подход и case-технологии.
    • 36. Процедурное (императивное) программирование
    • 37.Функциональное программирование.
    • 38. Декларативное программирование
    • 39. Объектно-ориентированное программирование
    • 40.Объектно-ориентированные языки программирования.
    • 41. Спецификация программного обеспечения при структурном подходе.
    • 42.Диаграммы переходов состояний.
    • 43. Функциональные диаграммы
    • 44. Диаграмма потоков данных
    • 45. Моделирование управляющих процессов с помощью диаграмм потоков данных
    • 46. Структуры данных и диаграммы отношений компонентов данных
    • 47. Диаграммы Джексона.
    • 48. Скобочные диаграммы Орра
    • 49. Сетевая модель данных
    • 50. Проектирование программного обеспечения при структурном подходе
    • 54. Метод пошаговой детализации для проектирования структуры по
    • 55. Структурные карты Констайна.
    • 56. Проектирование структур данных
    • 57. Представление данных в оперативной памят
    • 60. Проектирование программного обеспечения, основанное на декомпозиции данных Методикой Варнье-Орра
    • 61. Case-технологии, основанные на структурных методологиях анализа и проектирования
    • 63. Определение «вариантов использования»
    • 64. Диаграммы вариантов использования
    • 65. Построение концептуальной модели предметной области
    • 69. Проектирование программного обеспечения при объектном подходе
    • 70. Разработка структуры программного обеспечения при объектном подходе
    • Определение отношений между объектами.
    • Диаграммы последовательностей этапа проектирования.
    • Диаграммы кооперации.
    • Уточнение отношений классов.
    • Интерфейсы в uml.
    • Проектирование классов.
    • Проектирование методов класса.
    • Компоновка программных компонентов.
    • Проектирование размещения программных компонентов для распределенных программных систем.
    • Методы доказательства правильности программ.
    • Метод индуктивных утверждений Флойда.
    • Метод Хора доказательства правильности программ.
    • Виды контроля качества разрабатываемого программного обеспечения.
    • Формирование тестовых наборов, основные подходы.
    • Ручной контроль программного обеспечения, методы ручного контроля.
    • I. Контроль обращений к данным
    • 2. Контроль вычислений
    • 3. Контроль передачи управления
    • 4. Контроль межмодульных интерфейсов
    • Структурное тестирование, критерии формирования тестовых наборов.
    • Функциональное тестирование, методы формирования тестовых наборов.
    • Тестирование модулей и комплексное тестирование.
    • Оценочное тестирование.
    • Отладка программного обеспечения.
    • Классификация ошибок программного обеспечения.
    • Методы отладки программного обеспечения.
    • Методы и средства получения дополнительной информации об ошибках.
    • Общая методика отладки программного обеспечения.
    • Документирование и стандартизация.
    • Виды программных документов.
    • Основные правила оформления программной документации.
    • Основные инженерные подходы к созданию программ.
    • Классификация технологических подходов к созданию программ.
    • Классификация технологических подходов к созданию программ, подходы со слабой формализацией.
    • Классификация технологических подходов к созданию программ, строгие каскадные подходы.
    • Классификация технологических подходов к созданию программ, строгие каркасные подходы.
    • Классификация технологических подходов к созданию программ, генетические подходы.
    • Классификация технологических подходов к созданию программ, подходы на основе формальных преобразований.
    • Классификация технологических подходов к созданию программ, ранние подходы быстрой разработки.
    • Классификация технологических подходов к созданию программ, адаптивные технологические подходы.
    • Классификация технологических подходов к созданию программ, подходы исследовательского программирования.
    • Особенности и компоненты case-средств.
    • Объектно-ориентированные case-средства анализа и проектирования.
    • Структурные case-средства анализа и проектирования.
    • Case-средства компании ibm Rational Software, средство визуального моделирования Rational Rose.
    • Системы автоматизированного проектирования и их место среди других автоматизированных систем.
    • Структура сапр.
    • Разновидности сапр.
    • Понятие о cals-технологиях.