Уточнение — это общий термин в информатике, который охватывает различные подходы к созданию правильных компьютерных программ и упрощению существующих программ для обеспечения их формальной проверки.
В формальных методах уточнение программы — это проверяемое преобразование абстрактной (высокоуровневой) формальной спецификации в конкретную (низкоуровневую) исполняемую программу . [ нужна цитация ] Пошаговая доработка позволяет выполнять этот процесс поэтапно. Логично, что уточнение обычно предполагает импликацию , но могут возникнуть дополнительные сложности.
Постепенная своевременная подготовка журнала невыполненных работ (списка требований) в рамках гибких подходов к разработке программного обеспечения, таких как 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, может быть записан как . Типы уточнения, таким образом, связаны с поведенческими подтипами .
