Уточнение программного обеспечения: методы и подходы.
Refinement (computing)
Уточнение программного обеспечения: формальная верификация, разработка по методу Scrum, поэтапное преобразование спецификаций в код. Повышение качества ПО.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Усовершенствование — это общий термин в информатике, охватывающий различные подходы к разработке корректных компьютерных программ и упрощению существующих программ с целью обеспечения их формальной верификации.
Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.
Уточнение программы
В формальных методах усовершенствование программы — это верифицируемое преобразование абстрактной (высокоуровневой) формальной спецификации в конкретную (низкоуровневую) исполняемую программу. Пошаговое усовершенствование позволяет выполнять этот процесс поэтапно. Логически, усовершенствование обычно связано с импликацией, но могут возникать дополнительные сложности. Прогрессивная детализация бэклога продукта (списка требований) в гибких методологиях разработки программного обеспечения, таких как Scrum, также часто называется усовершенствованием.
In formal methods, program refinement is the verifiable transformation of an abstract (high level) formal specification into a concrete (low level) executable program. Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication, but there can be additional complications. The progressive just in time preparation of the product backlog (requirements list) in agile software development approaches, such as Scrum, is also commonly described as refinement.
Уточнение данных
Уточнение данных используется для преобразования абстрактной модели данных (например, представленной в виде множеств) в реализуемые структуры данных (такие как массивы). Уточнение операции преобразует спецификацию операции над системой в реализуемую программу (например, процедуру). В этом процессе пост-условие может быть усилено и/или предусловие ослаблено. Это уменьшает недетерминированность в спецификации, обычно приводя к полностью детерминированной реализации. Например, x ∈ {1,2,3} (где x – значение переменной x после операции) может быть уточнено до x ∈ {1,2}, затем до x ∈ {1} и реализовано как x := 1. В этом случае реализации x := 2 и x := 3 также были бы допустимы, используя другой путь уточнения. Однако следует избегать уточнения до x ∈ {} (что эквивалентно ложному), поскольку это нереализуемо; невозможно выбрать элемент из пустого множества. Термин "реификация" также иногда используется (введённый Клиффом Джонсом). Альтернативной техникой, когда формальное уточнение невозможно, является ретре́нчмент. Противоположностью уточнению является абстракция.
Data refinement is used to convert an abstract data model (in terms of sets for example) into implementable data structures (such as arrays). Operation refinement converts a specification of an operation on a system into an implementable program (e. g., a procedure). The postcondition can be strengthened and/or the precondition weakened in this process. This reduces any nondeterminism in the specification, typically to a completely deterministic implementation. For example, x ∈ {1,2,3} (where x is the value of the variable x after an operation) could be refined to x ∈ {1,2}, then x ∈ {1}, and implemented as x := 1. Implementations of x := 2 and x := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to x ∈ {} (equivalent to false) since this is unimplementable; it is impossible to select a member from the empty set. The term reification is also sometimes used (coined by Cliff Jones). Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction.
Рафинированный анализ
Исчисление уточнения — это формальная система (вдохновлённая логикой Хоара), способствующая уточнению программ. Система преобразований FermaT — промышленная реализация уточнения. Метод B также является формальным методом, расширяющим исчисление уточнения языком компонентов: он применялся в промышленных разработках.
Refinement calculus is a formal system (inspired from Hoare logic) that promotes program refinement. The FermaT Transformation System is an industrial strength implementation of refinement. The B Method is also a formal method that extends refinement calculus with a component language: it has been used in industrial developments.
Типы очистки
В теории типов, уточняющий тип — это тип, снабжённый предикатом, который предполагается истинным для любого элемента этого типа. Уточняющие типы могут выражать предусловия при использовании в качестве аргументов функций или постусловия при использовании в качестве типов возвращаемых значений: например, тип функции, принимающей натуральные числа и возвращающей натуральные числа, большие 5, может быть записан как. Таким образом, уточняющие типы связаны с поведенческим подтипированием.
In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as Refinement types are thus related to behavioral subtyping.