Уточнение (вычисление) - Refinement (computing)

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

Доработка программы

В формальные методы, уточнение программы это проверяемый преобразование Абстрактные (высокий уровень) формальная спецификация в бетон (низкий уровень) исполняемая программа.^{[нужна цитата ]} Пошаговое уточнение позволяет выполнять этот процесс поэтапно. Логично, что уточнение обычно включает значение, но могут быть дополнительные сложности.

Постепенная своевременная подготовка бэклога продукта (списка требований) в гибкая разработка программного обеспечения подходы, такие как Scrum, также обычно называют уточнением.^[1]

Уточнение данных

Уточнение данных используется для преобразования абстрактной модели данных (с точки зрения наборы например) в реализуемый структуры данных (такие как массивы ).^{[нужна цитата ]} Уточнение операции преобразует Технические характеристики операции в системе в реализуемую программа (например, процедура ). В постусловие могут быть усилены и / или предварительное условие ослаблены в этом процессе. Это снижает любые недетерминизм в спецификации, как правило, полностью детерминированный реализация.

Например, Икс ∈ {1,2,3} (где Икс стоимость переменная Икс после операции) может быть уточнено до Икс ∈ {1,2}, то Икс ∈ {1} и реализован как Икс : = 1. Реализации Икс : = 2 и Икс : = 3 будет в равной степени приемлемым в этом случае, используя другой маршрут для уточнения. Однако мы должны быть осторожны, чтобы не уточнять Икс ∈ {} (эквивалентно ложный), так как это нереализуемо; невозможно выбрать член от пустой набор.

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

Исчисление уточнения

Исчисление уточнения это формальная система (вдохновлено Логика Хоара ), что способствует уточнению программы. В Система трансформации FermaT представляет собой промышленное воплощение изысканности. В B-метод также формальный метод который расширяет исчисление уточнения с помощью компонентного языка: он использовался в промышленных разработках.

Типы уточнения

Основная статья: Тип уточнения

В теория типов, а тип уточнения^[2][3][4] - это тип, наделенный предикатом, который, как предполагается, выполняется для любого элемента уточненного типа. Типы уточнения могут выражать предварительные условия при использовании как аргументы функции или постусловия при использовании как возвращаемые типы: например, тип функции, которая принимает натуральные числа и возвращает натуральные числа больше 5, может быть записан как ${\displaystyle f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}}$. Таким образом, типы уточнений связаны с поведенческий подтип.

Смотрите также

• Реификация (информатика)

использованная литература

1. Чо, L (2009). «Внедрение гибкой культуры - путешествие команды по пользовательскому опыту». Agile конференция: 416. Дои:10.1109 / AGILE.2009.76. ISBN  978-0-7695-3768-9.
2. Freeman, T .; Пфеннинг, Ф. (1991). «Типы уточнений для ML» (PDF). Труды конференции ACM по проектированию и реализации языков программирования. С. 268–277. Дои:10.1145/113445.113468.
3. Хаяси, С. (1993). «Логика видов уточнения». Материалы семинара по типам для доказательств и программ. С. 157–172. CiteSeerX  10.1.1.38.6346. Дои:10.1007/3-540-58085-9_74.
4. Денни, Э. (1998). «Виды уточнения по спецификации». Труды Международной конференции ИФИП по концепциям и методам программирования. 125. Чепмен и Холл. С. 148–166. CiteSeerX  10.1.1.22.4988.