Усовершенствование — это общий термин в компьютерной науке, который охватывает различные подходы к созданию корректных компьютерных программ и упрощению существующих программ для обеспечения возможности их формальной проверки.
В формальных методах уточнение программы — это проверяемое преобразование абстрактной ( высокоуровневой) формальной спецификации в конкретную (низкоуровневую) исполняемую программу . [ требуется ссылка ] Пошаговое уточнение позволяет выполнять этот процесс поэтапно. Логически уточнение обычно подразумевает импликацию , но могут быть и дополнительные осложнения.
Последовательная своевременная подготовка бэклога продукта (списка требований) в гибких подходах к разработке программного обеспечения, таких как Scrum , также часто описывается как уточнение. [1]
Уточнение данных используется для преобразования абстрактной модели данных ( например , в терминах множеств ) в реализуемые структуры данных (например, массивы ). [ требуется ссылка ] Уточнение операций преобразует спецификацию операции в системе в реализуемую программу (например, процедуру ). Постусловие может быть усилено и/или предусловие ослаблено в этом процессе. Это уменьшает любой недетерминизм в спецификации, как правило, до полностью детерминированной реализации.
Например, x ∈ {1,2,3} (где x — значение переменной x после операции) можно уточнить до x ∈ {1,2}, затем x ∈ {1} и реализовать как x := 1. Реализации x := 2 и x := 3 были бы одинаково приемлемы в этом случае, используя другой маршрут для уточнения. Однако мы должны быть осторожны, чтобы не уточнить до x ∈ {} (эквивалентно false ), поскольку это нереализуемо; невозможно выбрать член из пустого множества .
Термин «реификация» также иногда используется (введен Клиффом Джонсом ). Сокращение — это альтернативный метод, когда формальная детализация невозможна. Противоположностью детализации является абстракция .
Исчисление уточнения — это формальная система (вдохновленная логикой Хоара ), которая способствует уточнению программ. Система преобразований FermaT — это промышленная реализация уточнения. B-метод также является формальным методом , который расширяет исчисление уточнения с помощью компонентного языка: он использовался в промышленных разработках.
В теории типов тип уточнения [2] [3] [4] — это тип, наделенный предикатом, который, как предполагается, выполняется для любого элемента уточненного типа. Типы уточнения могут выражать предусловия при использовании в качестве аргументов функции или постусловия при использовании в качестве возвращаемых типов : например, тип функции, которая принимает натуральные числа и возвращает натуральные числа больше 5, может быть записан как . Таким образом, типы уточнения связаны с поведенческим подтипированием .
