Реификация в формальных методах: превращение абстрактных идей в явные данные и объекты программирования. Оптимизация, манипуляции, "first-class citizen".
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Формальные методы: терминология
Formal methods terminology
Реификация – это процесс, посредством которого абстрактная идея о компьютерной программе преобразуется в явную модель данных или другой объект, созданный на языке программирования. Вычислимый/адресуемый объект – ресурс – создается в системе как заместитель для невычислимого/неадресуемого объекта. С помощью реификации то, что ранее было неявным, невыраженным и, возможно, невыразимым, становится явно сформулированным и доступным для концептуальных (логических или вычислительных) манипуляций. Неформально реификация часто называется "предоставлением чего-либо статуса полноправного объекта" в контексте конкретной системы. Некоторые аспекты системы могут быть реифицированы на этапе проектирования языка, что связано с рефлексией в языках программирования. Реификация может применяться как поэтапная детализация на этапе проектирования системы. Реификация является одним из наиболее часто используемых методов концептуального анализа и представления знаний.
Reification is the process by which an abstract idea about a computer program is turned into an explicit data model or other object created in a programming language. A computable/addressable object—a resource—is created in a system as a proxy for a non computable/addressable object. By means of reification, something that was previously implicit, unexpressed, and possibly inexpressible is explicitly formulated and made available to conceptual (logical or computational) manipulation. Informally, reification is often referred to as "making something a first class citizen" within the scope of a particular system. Some aspect of a system can be reified at language design time, which is related to reflection in programming languages. It can be applied as a stepwise refinement at system design time. Reification is one of the most frequently used techniques of conceptual analysis and knowledge representation.
Реификация данных против уточнения данных
Реификация данных (пошаговое уточнение) заключается в поиске более конкретного представления абстрактных типов данных, используемых в формальной спецификации. Реификация данных – это термин, принятый в Венском методе разработки (ВДМ), который большинство специалистов называют уточнением данных. Например, это может быть шаг к реализации, при котором представление данных, не имеющее прямого соответствия в целевом языке реализации (например, множества), заменяется представлением, которое такое соответствие имеет (например, отображения с фиксированными областями, которые могут быть реализованы массивами), или, по крайней мере, ближе к нему (например, последовательности). Сообщество ВДМ предпочитает термин "реификация" термину "уточнение", поскольку этот процесс больше связан с конкретизацией идеи, чем с её улучшением. См. также статью "Реификация (лингвистика)" для аналогичного использования термина.
Data reification (stepwise refinement) involves finding a more concrete representation of the abstract data types used in a formal specification. Data reification is the terminology of the Vienna Development Method (VDM) that most other people would call data refinement. An example is taking a step towards an implementation by replacing a data representation without a counterpart in the intended implementation language, such as sets, by one that does have a counterpart (such as maps with fixed domains that can be implemented by arrays), or at least one that is closer to having a counterpart, such as sequences. The VDM community prefers the word "reification" over "refinement", as the process has more to do with concretising an idea than with refining it. For similar usages, see Reification (linguistics).
В концептуальном моделировании
Реификация широко используется в концептуальном моделировании. Реификация отношения означает рассмотрение его как сущности. Цель реификации отношения – сделать его явным, когда необходимо добавить к нему дополнительную информацию. Рассмотрим тип отношения IsMemberOf (member:Person, Committee). Экземпляр IsMemberOf – это отношение, представляющее факт членства человека в комитете. На рисунке ниже показан пример заполнения отношения IsMemberOf в табличной форме. Лицо P1 является членом комитетов C1 и C2, а лицо P2 – только комитета C1. Однако тот же факт можно рассматривать и как сущность. Рассматривая отношение как сущность, можно сказать, что сущность реифицирует это отношение. Это называется реификацией отношения. Как и любая другая сущность, оно должно быть экземпляром типа сущности. В данном примере тип сущности назван Membership (Членство). Для каждого экземпляра IsMemberOf существует ровно один экземпляр Membership, и наоборот. Теперь становится возможным добавить больше информации к исходному отношению. Например, можно выразить факт, что "лицо p1 было выдвинуто на членство в комитет c1 лицом p2". Реифицированное отношение Membership может быть использовано в качестве источника нового отношения IsNominatedBy (Membership, Person). См. также Реификация (представление знаний) для связанных применений.
Reification is widely used in conceptual modeling. Reifying a relationship means viewing it as an entity. The purpose of reifying a relationship is to make it explicit, when additional information needs to be added to it. Consider the relationship type IsMemberOf(member:Person, Committee). An instance of IsMemberOf is a relationship that represents the fact that a person is a member of a committee. The figure below shows an example population of IsMemberOf relationship in tabular form. Person P1 is a member of committees C1 and C2. Person P2 is a member of committee C1 only. The same fact, however, could also be viewed as an entity. Viewing a relationship as an entity, one can say that the entity reifies the relationship. This is called reification of a relationship. Like any other entity, it must be an instance of an entity type. In the present example, the entity type has been named Membership. For each instance of IsMemberOf, there is one and only one instance of Membership, and vice versa. Now, it becomes possible to add more information to the original relationship. As an example, we can express the fact that "person p1 was nominated to be the member of committee c1 by person p2". Reified relationship Membership can be used as the source of a new relationship IsNominatedBy(Membership, Person). For related usages see Reification (knowledge representation).
В едином языке моделирования (UML)
UML предоставляет конструкцию "ассоциативный класс" для определения типов реифицированных связей. Ассоциативный класс — это единичный элемент модели, который является одновременно и ассоциацией, и классом. Ассоциация и тип сущности, который реифицируется, представляют собой один и тот же элемент модели. Следует отметить, что атрибуты не могут быть реифицированы.
UML provides an association class construct for defining reified relationship types. The association class is a single model element that is both a kind of association and a kind of a class. The association and the entity type that reifies are both the same model element. Note that attributes cannot be reified.
Противо котировки
Также важно отметить, что описанная здесь реификация не является тем же самым, что "цитирование", встречающееся в других языках. Вместо этого, реификация описывает взаимосвязь между конкретным экземпляром тройки и ресурсами, на которые эта тройка ссылается. Реификацию можно интуитивно понимать как утверждение "эта RDF-тройка говорит об этих вещах", а не (как при цитировании) "эта RDF-тройка имеет такую форму". Например, в примере реификации, приведенном в этом разделе, тройка: committee:membership12345 rdf:subject person:p1 описывает rdf:subject исходного утверждения, указывая, что субъект этого утверждения – это ресурс (человек), идентифицированный URIref person:p1. Она не утверждает, что субъект утверждения является самим URIref (то есть строкой, начинающейся с определенных символов), как это было бы при цитировании.
It is also important to note that the reification described here is not the same as "quotation" found in other languages. Instead, the reification describes the relationship between a particular instance of a triple and the resources the triple refers to. The reification can be read intuitively as saying "this RDF triple talks about these things", rather than (as in quotation) "this RDF triple has this form." For instance, in the reification example used in this section, the triple:
committee:membership12345 rdf:subject person:p1 describing the rdf:subject of the original statement says that the subject of the statement is the resource (the person) identified by the URIref person:p1. It does not state that the subject of the statement is the URIref itself (i. e., a string beginning with certain characters), as quotation would.