Уточнение (вычисления)

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

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

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

Постепенная своевременная подготовка журнала невыполненных работ (списка требований) в рамках гибких подходов к разработке программного обеспечения, таких как 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, может быть записан как $f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}$ . Типы уточнения, таким образом, связаны с поведенческими подтипами .

См. также

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

Ссылки

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

Эта программной инженерии, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее .

[1] Чо, Л. (2009). «Внедрение гибкой культуры — путь команды по улучшению пользовательского опыта». 2009 Agile-конференция . стр. 416–421. дои : 10.1109/AGILE.2009.76 . ISBN 978-0-7695-3768-9 . S2CID 38580329 .

[2] Фриман, Т.; Пфеннинг, Ф. (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 .

[1]

[2]

[3]

[4]