Difference between revisions of "Minor-ECMA-problems"

(Unfolding)
(Restored page content)
 
(9 intermediate revisions by 3 users not shown)
Line 1: Line 1:
=Unfolding=
+
[[Category:ECMA]]
 
+
When class ''D'' inherits from class ''B'' there is one very critical question. What form (in respect to unfolding) of ''B'' is taken into account for the inheritance semantics. Without an argument I state that it should be its completely unfolded form.
+
 
+
This said we can state that ''D'' inherits from the completely unfolded class ''B''. It remains to be specified in what order ''D'' is unfolded.
+
 
+
We list all the possible unfoldings that occur in the standard:
+
 
+
* 8.5.24 Definition: Unfolded form of a possibly multiple declaration
+
* 8.6.6 Definition: Unfolded Inheritance Part of a class
+
* Pre post conditions and invariants?
+
* 8.9.13 Definition: Unfolded feature list of an Only clause
+
* 8.9.14 Definition: Unfolded Only clause
+
* 8.9.24 Definition: Local unfolded form of an assertion
+
* 8.10.2 Definition: Unfolded form of an assertion
+
* 8.10.11 Definition: Relative unfolded form of a Precursor
+
* 8.10.13 Definition: Unfolded form of a Precursor
+
* 8.10.30 Definition: Unfolded redeclaration
+
* 8.17.9 Definition: Unfolded form of a multi-branch
+
* 8.17.10 Definition: Unfolded form of an interval
+
* 8.20.5 Definition: Unfolded Creators part of a class
+
* 8.20.14 Definition: Unfolded form of a creation instruction
+
 
+
 
+
 
+
==Definition: Coupled name==
+
 
+
====Motivation====
+
There are several situations in which the ECMA standard uses unfolded forms as a vehicle to describe semantics. When this unfolded forms need names, like in Precursor, inline agents and not isolated features. These names have an influence on the semantics of the system. An example:
+
 
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  B
+
feature
+
  f
+
      do
+
        (agent do g := g + 1; print (g) end).call ([])
+
      end
+
  g: INTEGER
+
end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  D
+
inherit
+
  B
+
      rename f as f1, g as g1, select f1, g1 end
+
  B
+
      rename f as f2, g as g2 end
+
end
+
</code>
+
|}
+
 
+
It feels natural to unfold class ''B'' first and then inherit ''D'' from its unfolded form before ''D'' is unfolded:
+
 
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  B
+
feature
+
  f
+
      do
+
        (agent fict_name).call ([])
+
      end
+
  g: INTEGER
+
 
+
  fict_name
+
      do
+
        g := g + 1; print (g)
+
      end
+
end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  D
+
inherit
+
  B
+
      rename f as f1, g as g1, select f1, g1 end
+
  B
+
      rename f as f2, g as g2 end
+
end
+
</code>
+
|}
+
The call-equivalent of the inline-agent (here named fict_name) has a call to ''g'' which has several
+
potential versions in ''D''. Hence this is not a valid system.
+
The same problem can occur with calls to ''Precursor''. The programmer cannot do anything about it since he has no knowledge of the fictitious name of the call-equivalent.
+
There should have been some coupling between the name ''f'' and the name of the call-equivalent of the inline-agent. The unfolded form of a renaming would then also rename all the coupled name (a precise definition follows). Our final example would become:
+
 
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  B
+
feature
+
  f
+
      do
+
        (agent fict_name).call ([])
+
      end
+
  g: INTEGER
+
 
+
  fict_name
+
      do
+
        g := g + 1; print (g)
+
      end
+
end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  D
+
inherit
+
  B
+
      rename f as f1, fict_name1, g as g1
+
      redefine f1, fict_name1, g1
+
      select f1, fict_name1, g1 end
+
  B
+
      rename f as f2, fict_name as fict_name2, g as g2
+
      redefine f2, fict_name2, g2 end
+
feature
+
  f1 do (agent fict_name1).call ([]) end
+
  fict_name1 do g1 := g1 + 1; print (g1) end
+
  g1: INTEGER
+
 
+
  f2 do (agent fict_name2).call ([]) end
+
  fict_name2 do g2 := g2 + 1; print (g2) end     
+
  g2: INTEGER
+
end
+
</code>
+
|}
+
 
+
The redefinitions of ''f1'', ''fict_name1'', ''g1'', ''f2'', ''fict_name2'' and ''g2'' come with the unfolded form of not isolated features.
+
Please note that the unfolded form of ''D'' needs to select ''fict_name1'' or ''fict_name2'' for the system to be valid. But this select has no semantic influence.
+
 
+
====Definition====
+
 
+
A feature name n can be '''coupled''' to another feature name .
+
 
+
====Change on renaming====
+
 
+
The unfolded form of a renaming introduces renamings to new fictitious names for all the names coupled to one of the renamed names.
+
 
+
Informal:
+
*Example Let feature names fc1 and fc2 be coupled to name f and feature name gc be coupled to g. The following renaming:
+
rename f as f', g as g'
+
 
+
Has the unfolded form:
+
 
+
rename f as f', fc1 as fc1', fc2 as fc2', g as g', gc as gc'
+
 
+
Whereas fc1', fc2' and gc' are new unique names.
+
 
+
====Change on select====
+
 
+
The unfolded form of a select introduces selects of all names coupled to one the originally selected names.
+
 
+
==A complex example with precursor==
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  A
+
feature
+
  a: INTEGER 
+
  f do a := a + 1 end
+
  g do f end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  B
+
inherit
+
  A redefine g end
+
feature
+
  g do Precursor end
+
end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  D
+
inherit
+
  B
+
      rename a as a1, f as f1, g as g1
+
      select a1, f1, g1 end
+
  B
+
      rename a as a2, f as f2, g as g2 end
+
feature
+
end
+
</code>
+
|}
+
 
+
Unfolded forms of ''A'' and ''B'':
+
 
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  A
+
feature
+
  a: INTEGER 
+
  f do a := a + 1 end
+
  g, gp do f end
+
</code>
+
|
+
<code>[eiffel, N]
+
class
+
  B
+
inherit
+
  A redefine g end
+
feature
+
  g do gp end
+
end
+
</code>
+
|}
+
 
+
Unfolded form of ''D'':
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|<code>[eiffel, N]
+
class
+
  D
+
inherit
+
  B
+
      rename a as a1, f as f1, g as g1, gp as gp1
+
      redefine f1, g1, gp1 end
+
      select a1, f1, g1, gp1 end
+
  B
+
      rename a as a2, f as f2, g as g2, gp as gp2
+
      redefine f2, g2, gp2 end
+
feature
+
  f1 do a1 := a1 + 1 end
+
  g1 do gp1 end
+
  gp1 do f1 end
+
 
+
  f2 do a2 := a2 + 1 end
+
  g2 do gp2 end
+
  gp2 do f2 end
+
end
+
</code>
+
|}
+
 
+
==New Behaviour of renaming and select==
+
The unfolded form of a renaming is the renaming itself plus the unfolded forms of the renamings of all the coupled names.
+
 
+
 
=Precursor=
 
=Precursor=
  
Line 301: Line 53:
 
f (STRING): ANY
 
f (STRING): ANY
  
==Stuff that is not correctly formulated=
+
==Stuff that is not correctly formulated==
 
Definition 8.5.1 should be changed to something with the following semantics:
 
Definition 8.5.1 should be changed to something with the following semantics:
  
Line 312: Line 64:
  
  
====8.9.5 Validity: Precondition Export rule=====
+
====8.9.5 Validity: Precondition Export rule====
A Precondition of a feature r of a class S is valid if and only if every feature f appearing[[ in every]]
+
A Precondition of a feature r of a class S is valid if and only if every feature f appearing in every
 
Assertion_clause of its unfolded form u satisfies the following two conditions for every class C to
 
Assertion_clause of its unfolded form u satisfies the following two conditions for every class C to
 
which r is available:
 
which r is available:
 
1 Iff appears as feature of a call in u or any of its subexpressions, f is available to C.
 
1 Iff appears as feature of a call in u or any of its subexpressions, f is available to C.

Latest revision as of 10:12, 30 May 2007

Precursor

The current definition of the Precursor semantics in the ECMA standard (8.10.11)

Agent types

Motivation

The classes ROUTINE, PROCEDURE, FUNCTION and the new class PREDICATE do not nicely fit in to the Eiffel language. Reasons:

  • They do not reflect the fact, that an agent can refer an attribute. An attribute is not a ROUTINE.
  • They do contradict the uniform access principle.
  • They are difficult to define. It is difficult to understand, why it is so difficult to define an agent type when it is so easy in functional languages!
    • Specially the first generic Parameter of ROUTINE is difficult to understand and, if I am not wrong, never used.
  • The standard conformance rules simply do not work nice for agent types. They introduce a type hole that can only be detected at runtime, and even then, only if precondition assertions are enabled. Other than cat calls this typing problem doesn't give the language more power.

An other mechanism:

I will give an example of an other mechanism:

Instead of writing

f: FUNCTION [ANY, TUPLE [STRING], INTEGER]

we could write

f (STRING): INTEGER

Calling this f would be easy:

i: INTEGER ... i := f ("hello")

We could also write:

i: INTEGER ... i := agent f ("hello")




Instead of writing:

f: FUNCTION [ANY, TUPLE [STRING], ANY]

we would write:

f (STRING): ANY

Stuff that is not correctly formulated

Definition 8.5.1 should be changed to something with the following semantics:

8.5.1 Definition: Inherited, immediate; origin; redeclared; replicated introduce

Any feature f of a class C is of one of the following four kinds:

  1. If C obtains f from one of its parents, f is an inherited feature of C. In this case any declaration of f in C (adapting the original properties of f for C) is a redeclaration.
  2. If a declaration appearing in C applies to a feature that is not inherited, the feature is said to be immediate in C. Then C is the origin (short for “class of origin”) of f, and is said to introduce f.


8.9.5 Validity: Precondition Export rule

A Precondition of a feature r of a class S is valid if and only if every feature f appearing in every Assertion_clause of its unfolded form u satisfies the following two conditions for every class C to which r is available: 1 Iff appears as feature of a call in u or any of its subexpressions, f is available to C.