Подход к разработке программ по правилу Design by contract
Design by Contract - основан на формальной верификации, формальной спецификации и логике Хоара.
Проектирование по контракту - это установление отношений между классом и его клиентами в виде формального соглашения, недвусмысленно устанавливающие права и обязанности сторон.
Логика Хоара — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ (предложена в 1969 г.). Пусть A – это некоторая операция, тогда формула корректности (correctness formula) – это выражение вида: {P} A {Q}
Формула корректности (триада Хоара) говорит: любое выполнение А, начинающееся в состоянии, где Р истинно, обязательно завершится и в заключительном состоянии будет истинно Q, где P и Q – это утверждения, при этом P является предусловием, а Q – постусловием.
Пример: {x = 5} x = x ^ 2 {x > 0}
Эта триада корректна, так как если перед выполнением операции x^2 предусловие выполняется и значение x равно 5, то после выполнения этой операции постусловие (x больше нуля) будет гарантировано выполняться.
Формальная спецификация — это математическое описание программной системы, которая может быть реализована в соответствии с этим описанием (описывается, что должна делать система).
Формальная верификация — доказательство соответствия алгоритмы, программы верификации его формальному описанию. Под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы.
|
|
|
Контрактное программирование предполагает, что проектировщик должен определить формальные, точные и верифицируемые спецификации интерфейсов для компонентов системы. При этом, кроме обычного определения абстрактных типов данных, также используются предусловия, постусловия и инварианты.
Автоматного программирование. Особенности.
Автоматное программирование — это парадигма программирования, при использовании которой программа или её фрагмент осмысливается как модель какого-либо формального автомата.
Определяющими для автоматного программирования являются следующие особенности:
1. Временной период выполнения программы разбивается на шаги автомата, каждый из которых представляет собой выполнение определённой (одной и той же для каждого шага) секции кода с единственной точкой входа; такая секция может быть оформлена, например, в виде отдельной функции и может быть разделена на подсекции, соответствующие отдельным состояниям или категориям состояний.
2. Передача информации между шагами автомата осуществляется только через явно обозначенное множество переменных, называемых состоянием автомата; между шагами автомата программа не может содержать неявных элементов состояния, таких как значения локальных переменных в стеке, адреса возврата из функций, значение текущего счётчика команд и т. п..
|
|
|
3. Полностью выполнение кода в автоматном стиле представляет собой цикл шагов автомата.
Интернационализация программного обеспечения.
Интернационализация(internationalization) — технологические приёмы разработки ПО, упрощающие адаптацию продукта к языковым и культурным особенностям региона , отличного от того, в котором разрабатывался продукт.
Есть два подхода - интернационализация и локализация.
Интернационализация — это адаптация продукта для потенциального использования практически в любом месте.
Локализация — это добавление специальных функций для использования в некотором определённом регионе. Интернационализация производится на начальных этапах разработки, в то время как локализация — для каждого целевого языка.
Существует три уровня локализации:
1. Обеспечить поддержку языка и национальных стандартов
2. Перевод текстов в интерфейсе программы на целевой язык
3. Тонкая настройка под целевую страну
Для интернационализации используют следующие приемы:
1. Текстовые строки хранятся в отдельных файлах
|
|
|
2. Активно используется Unicode.
3. Поскольку строки в процессе перевода могут удлиняться и укорачиваться, в диалоговых окнах применяют такие меры: окна специально компонуют «с запасом», в языковые ресурсы вносят компоновку диалоговых окон, диалоговые окна сами устанавливают свой размер в зависимости от длин строк.
4. Стараются использовать стандартные и проверенные оконные компоненты, избегая «самописных».
5. Делают конфигурируемыми все параметры, которые можно было бы изменять в другой стране. Для вывода на экран чисел, дат, времени и т. д. используют стандартные, а не «самописные» функции
Дата добавления: 2018-06-01; просмотров: 405; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!