<p>I've been struggling with understanding of the proofs showing that implementation statements are extensional.</p>

<p>Basically I am referring to material described in <a href="http://www.eden-study.org/articles/2006/abstraction-classes-sw-design_ieesw.pdf" rel="nofollow noreferrer">Abstraction Classes in Software Design</a> paper.</p>

<p>As an example, let us take the following proof for class diagram Figure 13:</p>

<p><a href="https://i.sstatic.net/3tV24.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/3tV24.png" alt=""></a></p>

<blockquote>
  <p><strong>Proposition 11.</strong> The class diagram in Figure 13 is extensional.</p>
  
  <p><strong>Proof:</strong> Let us show that Figure 13 is preserved under expansion. Let <em>M</em> designate a structure that satisfies Figure 13. Any such structure shall include, 
  among others, the following entities and relations:</p>
  
  <ul>
  <li>Class entities, such as <em>Creator</em> and <em>ConcreteCreator</em>, as well as 
  Method entities, such as <em>Creator::FactoryMethod</em> and 
  <em>ConcreteCreator::FactoryMethod</em>. </li>
  <li>The binary relation <em>Member</em>, which associates every method with one 
  class, such as the pair (<em>Creator::FactoryMethod</em>, <em>Creator</em>)</li>
  <li>The binary relation <em>Inherit</em>, which includes the pairs 
  (<em>ConcreteCreator</em>, <em>Creator</em>) and (<em>ConcreteProduct</em>, <em>Product</em>)</li>
  </ul>
  
  <p>Additional information in Figure 13 is represented informally. For
  example, the  relation <em>Invoke(AnOperation,FactoryMethod)</em> is
  represented by the note <em>product=FactoryMethod()</em> at the top right
  corner of the diagram.</p>
  
  <p>Note that every element in the diagram
  explicitly represents a specific entity (e.g., class <em>Creator</em>) or a
  specific relation (e.g., <em>Inherit(ConcreteCreator, Creator)</em>). Thus,
  expanding <em>M</em> with any number of Class entities cannot violate Figure
  13.</p>
  
  <p>Let us show that Figure 13 is preserved under reduction. There are two types of entities that can be removed from <em>M</em>:</p>
  
  <ul>
  <li>Entities that are explicitly mentioned in Figure 13.</li>
  <li>Entities that are not explicitly mentioned in Figure 13.</li>
  </ul>
  
  <p>By the Intension criterion, we
  only consider reductions removing entities  that are not explicitly
  mentioned in Figure 13 from the universe of <em>M</em>. Obviously, any such
  reduction will continue to satisfy Figure 13.</p>
</blockquote>

<p>My specific question is about preserving Figure 13 under reduction. How can we remove entities that are not explicitly mentioned in Figure 13? What are these entities that are not explicitly mentioned in Figure 13? Just don't get how can we remove something that is not present on the diagram.</p>

CC BY-SA 3.0
2013-04-10T04:54:52.060Z
I am not sure if the question is on-topic here, have you read our [FAQ]? Also please read the description of tags before using them.
Kaveh
CC BY-SA 3.0
2013-04-10T05:06:55.327Z
Hi Kaveh. This topic is related to computer science, so I've chosen this place to ask it. Which place would you suggest?
Volodymyr Tsukur
CC BY-SA 3.0
2013-04-10T06:14:58.800Z
I am not an expert on programming languages so I don't know if the question is on-topic here or not, hopefully PL people will comment (generally cstheory is mainly for professional researchers in *theoretical* computer science). There is also [cs.se] which has a broader scope.
Kaveh
CC BY-SA 4.0
2019-08-26T07:00:28.147Z
http://cs.stackexchange.com seems more appropriate for this question, as it's not research-level. It's just asking how to understand an example. When and if you move your question, please make sure the paper you linked to works. The link seems to be broken, and the question hinges on what precisely can be found in that paper. In fact, did you look there, as the paper should explain how to "remove entities that are not there".
Andrej Bauer
<lo.logic><se.software-engineering>
Proofs for Implementation Statements
Volodymyr Tsukur
# Proofs for Implementation Statements

(Asked by: username_0 on 2013-04-10)

I've been struggling with understanding of the proofs showing that implementation statements are extensional.

Basically I am referring to material described in [Abstraction Classes in Software Design](http://www.eden-study.org/articles/2006/abstraction-classes-sw-design_ieesw.pdf) paper.

As an example, let us take the following proof for class diagram Figure 13:

[![](https://i.sstatic.net/3tV24.png)](https://i.sstatic.net/3tV24.png)

> **Proposition 11.** The class diagram in Figure 13 is extensional.
>
> **Proof:** Let us show that Figure 13 is preserved under expansion. Let *M* designate a structure that satisfies Figure 13. Any such structure shall include,
> among others, the following entities and relations:
>
> * Class entities, such as *Creator* and *ConcreteCreator*, as well as
>   Method entities, such as *Creator::FactoryMethod* and
>   *ConcreteCreator::FactoryMethod*.
> * The binary relation *Member*, which associates every method with one
>   class, such as the pair (*Creator::FactoryMethod*, *Creator*)
> * The binary relation *Inherit*, which includes the pairs
>   (*ConcreteCreator*, *Creator*) and (*ConcreteProduct*, *Product*)
>
> Additional information in Figure 13 is represented informally. For
> example, the relation *Invoke(AnOperation,FactoryMethod)* is
> represented by the note *product=FactoryMethod()* at the top right
> corner of the diagram.
>
> Note that every element in the diagram
> explicitly represents a specific entity (e.g., class *Creator*) or a
> specific relation (e.g., *Inherit(ConcreteCreator, Creator)*). Thus,
> expanding *M* with any number of Class entities cannot violate Figure
> 13.
>
> Let us show that Figure 13 is preserved under reduction. There are two types of entities that can be removed from *M*:
>
> * Entities that are explicitly mentioned in Figure 13.
> * Entities that are not explicitly mentioned in Figure 13.
>
> By the Intension criterion, we
> only consider reductions removing entities that are not explicitly
> mentioned in Figure 13 from the universe of *M*. Obviously, any such
> reduction will continue to satisfy Figure 13.

My specific question is about preserving Figure 13 under reduction. How can we remove entities that are not explicitly mentioned in Figure 13? What are these entities that are not explicitly mentioned in Figure 13? Just don't get how can we remove something that is not present on the diagram.

**Tags:** lo.logic, se.software-engineering

> **Comments:**
> **username_1**: I am not sure if the question is on-topic here, have you read our [FAQ]? Also please read the description of tags before using them.  
> **username_0**: Hi username_1. This topic is related to computer science, so I've chosen this place to ask it. Which place would you suggest?  
> **username_1**: I am not an expert on programming languages so I don't know if the question is on-topic here or not, hopefully PL people will comment (generally cstheory is mainly for professional researchers in *theoretical* computer science). There is also [cs.se] which has a broader scope.  
> **username_2**: http://cs.stackexchange.com seems more appropriate for this question, as it's not research-level. It's just asking how to understand an example. When and if you move your question, please make sure the paper you linked to works. The link seems to be broken, and the question hinges on what precisely can be found in that paper. In fact, did you look there, as the paper should explain how to "remove entities that are not there".  

---

## 0 answers

