[[Property:title|What makes a Certified Attachment Pattern]]
[[Property:weight|8]]
[[Property:uuid|1a20197d-5a88-59c3-9a04-512399125661]]

==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    -- Valid for formal arguments, local variables, and stable attributes
            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 standard 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. 

Still, the standard does contain informative text that gives us a guideline that a CAP is a scheme to ensure that a particular expression of a detachable type will never have void run-time value in the scope covered by the CAP.

The discussion here will follow that guideline, and, as such, will be less formal (and consequently 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 investigate the specifics.


==CAP-able expressions==

In the first context in the definition above, 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 [[Void-safety: Background, definition, and tools#The attached syntax (object test)|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>

Additionally, the Eiffel Software compiler allows for [[Void-safety: Background, definition, and tools#Stable attributes|stable attributes]] and local variables to be protected by a CAP. 

===Stable attributes===

Stable attributes are the only class attributes which are CAP-able. This is because stable attributes, once attached at run-time, can never have a void value again. So, you use stable attributes safely by using them under the protection of a CAP. Consider this stable attribute:
<code>
    my_stable_string: detachable STRING
        note
            option: stable
        attribute
        end
</code>
The detachable attribute <code>my_stable_string</code>, because it is stable, is not required to be initialized during the creation of instances of the class in which it is a feature. That means that for each instance, <code>my_stable_string</code> can be initialized later during the instance's life-cycle or not at all. But because it is detachable, <code>my_stable_string</code> cannot be accessed in any context in which it cannot be determined that it is currently attached. For ordinary attributes, this means either using an object test and accessing the object through an object test local, or using using a local variable under the protection of a CAP. 

Stable attributes however, can be used directly in a CAP, as shown below: 

<code>
            if my_stable_string /= Void then
                my_stable_string.append ("abc")        -- Valid
                    ...
</code>

So using stable attributes can reduce the need to initialize rarely used attributes, and the need to code object tests.

===Local variables===

Local variables can be used in a CAP as long as they are not the target of an assignment whose source is <code>Void</code> or some expression which could possibly be void.

So, for a local variable <code>l_string</code>, the following is valid:
<code>
        local
            l_string: detachable STRING
        do
            if l_string /= Void then
                l_string.append ("abc")        -- Valid
                    ...
</code>

But, if <code>l_string</code> had been a target of an assignment in which the source could possibly have been void, then it could no longer be guaranteed that <code>l_string</code> is not void. So, assuming that <code>my_detachable_string</code> is an attribute declared as type <code>detachable STRING</code>, the second application of <code>append</code> in this example would be invalid:

<code>
        local
            l_string: detachable STRING
        do
            if l_string /= Void then
                l_string.append ("abc")        -- Valid
                l_string := my_detachable_string
                l_string.append ("xyz")        -- Invalid: my_detachable_string might have been void
                    ...
</code>

==Common CAPs==

We've already seen the simple test for void as a CAP:
<code>
    local
        l_str: detachable STRING

                ...

            if l_str /= Void then
                l_str.append ("xyz")        -- Valid
            end
</code>

Additionally, a creation instruction can serve as a CAP. After the execution of a creation instruction, the target of the creation instruction will be attached:
<code>
        local
            l_str: detachable STRING
        do
            create l_str.make_empty
            l_str.append ("xyz")        -- Valid
                ...
</code>


==Less obvious cases==

There are some situations that constitute CAPs that we might not think of immediately. 

For example, the case of the non-strict boolean operator <code>and then</code>: 
<code>
            if x /= Void and not x.is_empty then        -- Invalid
                ...

            if x /= Void and then not x.is_empty then        -- Valid
                ...
</code>
Assuming that <code>x</code> is CAP-able, the first line of code is invalid because the expression <code>x.is_empty</code> could always be evaluated even in the case in which <code>x</code> is void. 

In the second line of code, the non-strict boolean is used, guaranteeing that <code>x.is_empty</code> will not be evaluated in cases in which <code>x</code> is void. Therefore, <code>x.is_empty</code> falls within the scope of the void test on <code>x</code>.

In contracts, multiple assertion clauses are treated as if they were separated by <code>and then</code>. This allows preconditions like the one in the following example:
<code>
my_routine (l_str: detachable STRING)
        require
            l_str /= Void
            not l_str.is_empty        -- Valid
                ...
</code>

Another not-so-obvious CAP is related to the use of the logical implication:
<code>
        local
            l_str: detachable STRING
        do
            if l_str /= Void implies some_expression then
                ...
            else
                l_str.append ("xyz")        -- Valid
            end
</code>


==The bottom line on CAPs==

In summary, CAPs provide void-safe protection for certain types of detachable expressions. 

Possibly the characteristic of CAPs which is most important to developers is whether or not a particular CAP is supported by the compiler. In other words, from the developers viewpoint, the only opinion that matters in the argument of whether a particular pattern constitutes a CAP is that of the compiler. 

If the compiler can provide assurance that a certain code pattern guarantees void-safe protection, then the developer will have that pattern available as a CAP. Likewise, even if a pattern can be shown logically to be a CAP, but for some reason it is not supported by the compiler, then that pattern will not available as a CAP and the compiler will not allow its use.