Attached types
Contents
Introduction
Attached types are introduced in the language by the ECMA/ISO standard to get rid of a common program error caused by a call of a feature on a Void target. The existing code base cannot be changed overnight to follow the new safety standards. Therefore there is a task to perform the smooth transition from non-void-safe code to void-safe code. This can be done by systematic application of the following steps:
- Identification. The code is analyzed to find some common patterns that assume that the target of the feature call is not void. They can be explicit, such as
require a /= Void
as well as implicit, such as
a.f
- Selection. Usually there is more than one way to change the existing code to make it void-safe. The correct replacement depends on the semantics of the piece of code and may rely on expert knowledge of a user. But there are still many "common" cases that require the same kind of modification which allows for automation of the process.
- Modification. After selection among the possible variants is completed, the actual code modification is performed. In order to avoid breaking all the code, the backup of the original as well as a journal of the changes can be kept.
The steps above can be performed manually, semi-automatically or automatically. The sections below discuss the variants that involve the tools to automate the transition to void-safe code.
Suggested Attachment Pattern (SAP)
Suggested Attachment Pattern (SAP) in non-void-safe code is similar to Certified Attachment Pattern (CAP) in void-safe code. Moreover, SAP is a superset of CAP, i.e. it includes all CAP code snippets as well as some other variants. SAP stands for the code patterns that expect that there is no feature calls on void target if they themselves do not trigger any exception. The most simple SAP includes the condition x /= Void
. In this case the type of x
can be declared to be attached, so that the condition can be optimized by substituting the value True
, or non-attached, so that the condition is not affected.
SAP |
---|
require x /= Void
|
ensure x /= Void
|
invariant x /= Void
|