mirror of
https://github.com/EiffelSoftware/eiffel-org.git
synced 2025-12-08 07:42:33 +01:00
452919f733
Date:2009-09-18T18:49:11.000000Z git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@302 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
62 lines
3.4 KiB
Plaintext
62 lines
3.4 KiB
Plaintext
[[Property:title|What makes a Certified Attachment Pattern]]
|
|
[[Property:weight|8]]
|
|
[[Property:uuid|1a20197d-5a88-59c3-9a04-512399125661]]
|
|
{{underconstruction}}
|
|
|
|
|
|
|
|
==A little background on CAPs==
|
|
|
|
Certified Attachment Patterns (CAPs) were described in the section on [[Void-safety: Background, definition, and tools#Certified attachment patterns (CAPs)|void-safety tools]]. To review, a CAP is a code pattern for a certain expression, say <code>exp</code> of a detachable type that ensures that <code>exp</code> will never have a void run-time value within the covered scope.
|
|
|
|
A simple example is the familiar test for void reference:
|
|
<code>
|
|
if l_x /= Void then
|
|
l_x.do_something
|
|
end
|
|
</code>
|
|
We know that after the explicit check to make sure <code>l_x</code> is not <code>Void</code>, that the feature application <code>l_x.do_something</code> is void-safe.
|
|
Of course, you should remember from previous discussions that <code>l_x</code> must be a local variable, a formal argument, or a [[Void-safety: Background, definition, and tools#Stable attributes|stable attribute]].
|
|
|
|
When void-safety was first envisioned for Eiffel, it was intended that individual CAPs would be proven or certified and documented. This would produce a "catalog" of CAPs.
|
|
|
|
What happened instead is that the members of the Eiffel standards committee have been able to produce and publish as part of the [http://www.ecma-international.org/publications/standards/Ecma-367.htm standard] a definition of the nature of a CAP from which a determination can be made as to whether a particular code pattern is or is not a CAP.
|
|
|
|
The definition in the standard document is not easily readable by most developers. So, in this documentation, you will see various examples of CAPs and the rationale behind them.
|
|
|
|
|
|
==The standard CAP definition==
|
|
|
|
The Eiffel standard (2nd edition, June 2006) defines a CAP as follows:
|
|
----
|
|
'''''A Certified Attachment Pattern (or CAP) for an expression <code>exp</code> whose type is detachable is an occurrence of <code>exp</code> in one of the following contexts: '''''
|
|
|
|
|
|
'''''1. <code>exp</code> is an Object-Test Local and the occurrence is in its scope. '''''
|
|
|
|
'''''2. <code>exp</code> is a read-only entity and the occurrence is in the scope of a void test involving <code>exp</code>.'''''
|
|
----
|
|
|
|
The terminology used in the definition is precise. For example, terms like "read-only entity" and "scope of a void test" have specific meanings that are supported by their own definitions in the standard.
|
|
|
|
The discussion here will be less formal (and less precise) than that in the standard, and is intended to be a practical guide. Of course, the [http://www.ecma-international.org/publications/standards/Ecma-367.htm standard document] is available for download if you wish to follow the specifics.
|
|
|
|
|
|
==CAP-able expressions==
|
|
|
|
In the first context, the definition states that the expression <code>exp</code> can be an '''Object-Test Local'''. An Object-Test Local is the identifier specified for a fresh local entity in an '''object test'''. Remember, object tests are coded using the '''attached syntax'''.
|
|
<code>
|
|
attached x as l_x
|
|
</code>
|
|
In the object test expression above, the identifier <code>l_x</code> is an Object-Test Local.
|
|
|
|
In the second context, the expression can be a read-only entity. Read-only entities are:
|
|
# Constant attributes
|
|
# formal arguments
|
|
# Object-Test Locals
|
|
# <code>Current</code>
|
|
|
|
|
|
|
|
|