From 1c0ec7b9c568696e35c3cf47e3b38d1807fe54d2 Mon Sep 17 00:00:00 2001 From: halw Date: Fri, 30 Oct 2009 20:12:01 +0000 Subject: [PATCH] Author:halw Date:2009-10-30T20:12:01.000000Z git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@343 abb3cda0-5349-4a8f-a601-0c33ac3a8c38 --- .../external-compilation-pane.wiki | 3 + ...afety-background-definition-and-tools.wiki | 4 +- ...at-makes-certified-attachment-pattern.wiki | 64 +++++++++++++++++++ 3 files changed, 68 insertions(+), 3 deletions(-) diff --git a/documentation/current/eiffelstudio/eiffelstudio-reference/outputs-tool/external-compilation-pane.wiki b/documentation/current/eiffelstudio/eiffelstudio-reference/outputs-tool/external-compilation-pane.wiki index 1a09b164..9386dd51 100644 --- a/documentation/current/eiffelstudio/eiffelstudio-reference/outputs-tool/external-compilation-pane.wiki +++ b/documentation/current/eiffelstudio/eiffelstudio-reference/outputs-tool/external-compilation-pane.wiki @@ -1,6 +1,9 @@ [[Property:title|External compilation pane]] [[Property:weight|3]] [[Property:uuid|26525412-e8e5-8b1c-1074-58e00aed4c76]] +{{underconstruction}} + + The external compilation pane is where C compilation output is shown. [[Image:coutput1|C output tool]] diff --git a/documentation/current/method/void-safe-programming-eiffel/void-safety-background-definition-and-tools.wiki b/documentation/current/method/void-safe-programming-eiffel/void-safety-background-definition-and-tools.wiki index 2a5364b0..2129a7c5 100644 --- a/documentation/current/method/void-safe-programming-eiffel/void-safety-background-definition-and-tools.wiki +++ b/documentation/current/method/void-safe-programming-eiffel/void-safety-background-definition-and-tools.wiki @@ -129,9 +129,7 @@ When building void-safe software in Eiffel it is best, in virtually every case, ====Attachment and conformance==== -The distinction between attached and detachable types results in a small but important addition to the rules of conformance. - -Because features declared as attached types can never be void, then it is important not to allow any assignment of a detachable source to an attached target, as shown below, assuming types are attached by default. +The distinction between attached and detachable types results in a small but important addition to the rules of conformance. Because variables declared as attached types can never be void, then it is important not to allow any assignment of a detachable source to an attached target. However, assigning an attached source to a detachable target is permissible. The following code shows both cases and assumes types are attached by default. my_attached_string: STRING my_detachable_string: detachable STRING diff --git a/documentation/current/method/void-safe-programming-eiffel/what-makes-certified-attachment-pattern.wiki b/documentation/current/method/void-safe-programming-eiffel/what-makes-certified-attachment-pattern.wiki index 260ac7f3..93dbab5d 100644 --- a/documentation/current/method/void-safe-programming-eiffel/what-makes-certified-attachment-pattern.wiki +++ b/documentation/current/method/void-safe-programming-eiffel/what-makes-certified-attachment-pattern.wiki @@ -109,5 +109,69 @@ But, if l_string had been a target of an assignment in which the so ... +==Common CAPs== + +We've already seen the simple test for void as a CAP: + + local + l_str: detachable STRING + + ... + + if l_str /= Void then + l_str.append ("xyz") + end + + +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: + + local + l_str: detachable STRING + do + create l_str.make_empty + l_str.append ("xyz") + ... + + + +==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 and then: + + if x /= Void and not x.is_empty then -- Invalid + ... + + if x /= Void and then not x.is_empty then -- Valid + ... + +Assuming that x is CAP-able, the first line of code is invalid because the expression x.is_empty could always be evaluated even in the case in which x is void. + +In the second line of code, the non-strict boolean is used, guaranteeing that x.is_empty will not be evaluated in cases in which x is void. Therefore, x.is_empty falls within the scope of the void test on x. + +In contracts, multiple assertion clauses are treated as if they were separated by and then. This allows preconditions like the one in the following example: + +my_routine (l_str: detachable STRING) + require + l_str /= Void + not l_str.is_empty -- Valid + ... + + +Another not-so-obvious CAP is related to the use of the logical implication: + + local + l_str: detachable STRING + do + if l_str /= Void implies some_expression then + ... + else + l_str.append ("xyz") -- Valid + end + + + +