 | Эта статья требует дополнительных ссылок для проверки . ( сентябрь 2010 г. ) ( Узнайте, как и когда удалить это сообщение-шаблон ) |
| Преобразование данных |
|---|
| Концепции |
| Языки трансформации |
| Техники и трансформации |
| Приложения |
| Связанный |
Уточнение - это общий термин информатики, который охватывает различные подходы к созданию правильных компьютерных программ и упрощению существующих программ для обеспечения их формальной проверки.
Уточнение программы [ править ]
В формальных методах , программа уточнение является проверяемой трансформацией абстрактной (высокого уровня) формальной спецификации в бетон (низкий уровень) исполняемый файл программа . [ необходима цитата ] Пошаговое уточнение позволяет выполнять этот процесс поэтапно. Логично, что уточнение обычно подразумевает подтекст , но могут возникнуть дополнительные сложности.
Постепенная своевременная подготовка отставания по продукту (списка требований) в гибких подходах к разработке программного обеспечения , таких как Scrum , также обычно называют доработкой. [1]
Уточнение данных [ править ]
Уточнение данных используется для преобразования абстрактной модели данных (например, в терминах наборов ) в реализуемые структуры данных (например, массивы ). [ необходима цитата ] Уточнение операции преобразует спецификацию операции в системе в реализуемую программу (например, процедуру ). Постусловие можно усилить и / или предпосылка ослаблена в этом процессе. Это снижает любой недетерминизм в спецификации, как правило, до полностью детерминированной реализации.
Например, x ∈ {1,2,3} (где x - значение переменной x после операции) может быть уточнено до x ∈ {1,2}, тогда x ∈ {1} и реализовано как x : = 1. Реализации x : = 2 и x : = 3 будут в равной степени приемлемы в этом случае, используя другой маршрут для уточнения. Однако мы должны быть осторожны, чтобы не уточнить x ∈ {} (эквивалентно false ), поскольку это нереализуемо; невозможно выбрать член из пустого набора .
Иногда также используется термин « овеществление» (придуман Клиффом Джонсом ). Восстановление - это альтернативный метод, когда формальное уточнение невозможно. Противоположность изысканности - абстракция .
Исчисление уточнения [ править ]
Исчисление уточнения - это формальная система (вдохновленная логикой Хоара ), которая способствует уточнению программы. Система трансформации FermaT - это промышленное воплощение усовершенствований. В-метод также формальный метод , который расширяет утонченность исчисление с компонентом языка: он был использован в промышленных разработках.
Типы уточнения [ править ]
В теории типа , A тип уточнения [2] [3] [4] представляет собой тип , наделенный предикат , который , как предполагается, для удержания любого элемента рафинированного типа. Типы уточнения могут выражать предварительные условия при использовании в качестве аргументов функции или постусловия при использовании в качестве возвращаемых типов : например, тип функции, которая принимает натуральные числа и возвращает натуральные числа больше 5, может быть записан как . Таким образом, типы уточнения связаны с поведенческими подтипами .
См. Также [ править ]
- Реификация (информатика)
Ссылки [ править ]
- Перейти ↑ Cho, L (2009). «Принятие Agile-культуры - путь команды взаимодействия с пользователем». Agile конференции : 416. DOI : 10,1109 / AGILE.2009.76 . ISBN 978-0-7695-3768-9.
- ^ Freeman, T .; Пфеннинг, Ф. (1991). «Типы уточнения для ML» (PDF) . Труды конференции ACM по проектированию и реализации языков программирования . С. 268–277. DOI : 10.1145 / 113445.113468 .
- Перейти ↑ Hayashi, S. (1993). «Логика видов уточнения». Материалы семинара по типам для доказательств и программ . С. 157–172. CiteSeerX 10.1.1.38.6346 . DOI : 10.1007 / 3-540-58085-9_74 .
- ^ Денни, Э. (1998). «Виды уточнения по спецификации». Труды Международной конференции ИФИП по концепциям и методам программирования . 125 . Чепмен и Холл. С. 148–166. CiteSeerX 10.1.1.22.4988 .
