Difference between revisions of "DynamicTypeSet"

m (CAT-Call freeness detection algorithms)
m (Remove 'is' keyword)
 
(17 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 +
[[Category:ECMA]]
 
Author: Matthias Konrad
 
Author: Matthias Konrad
 +
 +
{{UnderConstruction}}
  
 
====CAT-Call freeness detection algorithms====
 
====CAT-Call freeness detection algorithms====
Line 5: Line 8:
 
* Kind A: Report a system that has no CAT-call as NOT CAT-call free.
 
* Kind A: Report a system that has no CAT-call as NOT CAT-call free.
 
* Kind B: Report a system containing CAT-calls as CAT-call free.
 
* Kind B: Report a system containing CAT-calls as CAT-call free.
Algorithms making errors of kind B are of no use. An algorithm that only makes errors of kind A leads to type safety, but may be useless if it makes too many (the trivial algorithm, that reports every Eiffel system as NOT CAT-call free makes no errors of Kind B but is completely useless).
+
Algorithms making errors of kind B are of no use. An algorithm that only makes errors of kind A leads to type safety, but may be useless if it makes too many (the trivial algorithm, that reports every Eiffel system as NOT CAT-call free makes no errors of kind B but is completely useless).
The goal is thus to find the maximal subclass of the class of CAT-call free Eiffel systems that is decidable and fast enough to be used in practice.
+
The goal is thus to find the maximal (or most reasonable) subclass of the class of CAT-call free Eiffel systems that is decidable and fast enough to be used in practice.
  
 
====Dynamic type set algorithm====
 
====Dynamic type set algorithm====
The Dynamic type set algorithm (DTSA) as defined in ETL2 (combined with a system validity check) seems to make no errors of kind B (it remains to be proven) but certainly of kind A. By showing some of these errors we try to show what impact the DTSA has to the Eiffel language. The following system will be used for examples:
+
The Dynamic type set algorithm (DTSA) as defined in ETL2 (combined with a system validity check) seems to make no errors of kind B (it remains to be proven) but certainly of kind A. By showing some of these errors we try to show what impact the DTSA has to the Eiffel language.  
 
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
+
|-valign="top" -halign="center"
+
|
+
<code>[eiffel,N]
+
class
+
  LIST_ANY
+
feature
+
  put (i: ANY) is
+
      do
+
        item := i
+
      end
+
  item: ANY
+
end
+
</code>
+
|
+
<code>[eiffel,N]
+
class
+
  LIST_STRING
+
inherit
+
  LIST_ANY
+
      redefine put, item end
+
feature
+
  put (i: STRING) is
+
      do
+
        i.to_lower
+
      end
+
  item: STRING
+
end
+
</code>
+
|}
+
  
 
DTSA does not work well with generic algorithms. See feature ''merge'', that merges the list ''f'' into the list ''t'':
 
DTSA does not work well with generic algorithms. See feature ''merge'', that merges the list ''f'' into the list ''t'':
  
 
<code>[eiffel, N]
 
<code>[eiffel, N]
merge (f, t: LIST [ANY]) is
+
merge (f, t: LIST [ANY])
 +
  require
 +
      f /= Void
 +
      t /= Void
 +
      --f.G <= t.G
 
   do
 
   do
 
       from f.start until f.after loop
 
       from f.start until f.after loop
         t.extend (f.item)   --f.G <= t.G
+
         t.extend (f.item)  
 
         f.forth
 
         f.forth
 
       end
 
       end
Line 54: Line 30:
 
</code>
 
</code>
  
This feature might be used frequently in a bigger system. As a consequence, the dynamic type sets of both arguments become large. It is not the performance problem that interests us here, but the fact that the feature will become invalid very fast. A system containing the following two calls to ''merge'' (even if the calls are not in the same feature or even class) will invalidate the system:
+
This feature might be used frequently in a bigger system. As a consequence, the dynamic type sets of both arguments become large. It is not the performance problem that interests us here, but the fact that the feature will become invalid very fast. A system containing the following two calls to ''merge'' (even if the calls are not in the same feature or even class) will be reported as invalid:
  
 
<code>[eiffel, N]
 
<code>[eiffel, N]
Line 61: Line 37:
 
</code>
 
</code>
  
I consider this a strong error of kind A, since it obviously takes power (genericity) from the language.  
+
I consider this a strong error of kind A, since it obviously takes power (genericity) from the language.
 +
 
 +
====Why does the DTSA fail for the merge methode====
 +
==Proof obligation based algorithm==
 +
 
 +
Feature ''merge'' works with lots of dynamic types. It depends on one thing tough, the actual generic parameter of argument ''f'' needs to be equally or more specific compared to the actual generic parameter of argument ''t''. This constraint should be detected by an algorithm and made an obligation for every caller of ''merge''. In Eiffel an obligation made to a caller is a precondition.
 +
 
 +
====Rule 1====
 +
For calls of the form:
 +
 
 +
<code>
 +
t.f (a)
 +
</code>
 +
where feature the first formal argument of feature ''f'' is of generic type G the following obligation follows:
 +
a <= t.G, a needs to be more specific than the
 +
 
 +
 
 +
 
  
Feature ''merge'' works with lots of dynamic types. But it depends on one thing, the actual generic parameter of argument ''f'' needs to be equally or more specific compared to the actual generic parameter of argument ''t''. This constraint should be detected by an algorithm and made an obligation for every caller of ''merge''.
 
  
 
A better algorithm should detect what feature ''merge'' depends on to work properly.  
 
A better algorithm should detect what feature ''merge'' depends on to work properly.  
Line 73: Line 65:
 
|-valign="top" -halign="center"
 
|-valign="top" -halign="center"
 
|
 
|
<code>[eiffel,N]
+
<e>
foo is
+
foo
 
   local
 
   local
 
       l1: LIST_ANY
 
       l1: LIST_ANY
Line 87: Line 79:
 
       double_list (l2)
 
       double_list (l2)
 
   end
 
   end
</code>
+
</e>
 
|
 
|
<code>[eiffel, N]
+
<e>
double_list (l: LIST_ANY) is  -- backward obligation: l.put.item >= l.item
+
double_list (l: LIST_ANY)   -- backward obligation: l.put.item >= l.item
 
   do
 
   do
 
       l.put (l.item)           
 
       l.put (l.item)           
Line 105: Line 97:
 
   end
 
   end
  
</code>
+
</e>
 
|}
 
|}
  
Line 112: Line 104:
 
   
 
   
  
 +
The following system will be used for examples:
  
can make two kinds of errors
+
{|border="0" cellpadding="2" cellspacing="0" align="center"
But it is easy to come up with an algorithm that detects for a subset of all CAT-call free Eiffel systems that they are CAT-call free
+
|-valign="top" -halign="center"
   * detects a subset of all CAT-call free
+
|
But for some systems it is easy to show, that they are CAT call free.
+
<code>[eiffel,N]
 
+
class
The challenge is thus to find the
+
   LIST_ANY
So DTSA cannot do that,
+
feature
it will correctly declare some Eiffel systems as CAT call free
+
  put (i: ANY) is
 +
      do
 +
        item := i
 +
      end
 +
  item: ANY
 +
end
 +
</code>
 +
|
 +
<code>[eiffel,N]
 +
class
 +
  LIST_STRING
 +
inherit
 +
  LIST_ANY
 +
      redefine put, item end
 +
feature
 +
  put (i: STRING) is
 +
      do
 +
        item := i
 +
      end
 +
  item: STRING
 +
end
 +
</code>
 +
|}

Latest revision as of 08:35, 19 August 2013

Author: Matthias Konrad

Construction.png Not Ready for Review: This Page is Under Development!

CAT-Call freeness detection algorithms

Finding out, whether any given Eiffel system contains a CAT call is undecidable. A CAT call finding algorithm will thus make one or both of the following error kinds:

  • Kind A: Report a system that has no CAT-call as NOT CAT-call free.
  • Kind B: Report a system containing CAT-calls as CAT-call free.

Algorithms making errors of kind B are of no use. An algorithm that only makes errors of kind A leads to type safety, but may be useless if it makes too many (the trivial algorithm, that reports every Eiffel system as NOT CAT-call free makes no errors of kind B but is completely useless). The goal is thus to find the maximal (or most reasonable) subclass of the class of CAT-call free Eiffel systems that is decidable and fast enough to be used in practice.

Dynamic type set algorithm

The Dynamic type set algorithm (DTSA) as defined in ETL2 (combined with a system validity check) seems to make no errors of kind B (it remains to be proven) but certainly of kind A. By showing some of these errors we try to show what impact the DTSA has to the Eiffel language.

DTSA does not work well with generic algorithms. See feature merge, that merges the list f into the list t:

merge (f, t: LIST [ANY])
   require
      f /= Void
      t /= Void
      --f.G <= t.G
   do
      from f.start until f.after loop
         t.extend (f.item) 
         f.forth
      end
   end

This feature might be used frequently in a bigger system. As a consequence, the dynamic type sets of both arguments become large. It is not the performance problem that interests us here, but the fact that the feature will become invalid very fast. A system containing the following two calls to merge (even if the calls are not in the same feature or even class) will be reported as invalid:

merge (create {LINKED_LIST [STRING]}.make, create {LINKED_LIST [STRING]}.make)
merge (create {LINKED_LIST [ANY]}.make, create {LINKED_LIST [ANY]}.make)

I consider this a strong error of kind A, since it obviously takes power (genericity) from the language.

Why does the DTSA fail for the merge methode

Proof obligation based algorithm

Feature merge works with lots of dynamic types. It depends on one thing tough, the actual generic parameter of argument f needs to be equally or more specific compared to the actual generic parameter of argument t. This constraint should be detected by an algorithm and made an obligation for every caller of merge. In Eiffel an obligation made to a caller is a precondition.

Rule 1

For calls of the form:

t.f (a)

where feature the first formal argument of feature f is of generic type G the following obligation follows: a <= t.G, a needs to be more specific than the



A better algorithm should detect what feature merge depends on to work properly.


One weakness of the DTSA is, that the dynamic type sets of arguments of often used types become huge. This indirectly leads to many errors of kind A as the following example shows:

foo
   local
      l1: LIST_ANY
      l2: LIST_STRING
   do
      create l1
      l1.put ("")
      double_list (l1)
 
      create l2
      l2.put ("")
      double_list (l2)
   end
double_list (l: LIST_ANY)   -- backward obligation: l.put.item >= l.item
   do
      l.put (l.item)          
   end
 
merge_list (from_list, to_list: LIST_ANY)   --backward obligation: to_list.put.item >= from_list.start
   do
      to_list.put (from_list.start)
   end
 
add_to_list (list: LIST_ANY; elem: ANY)   --backward obligation: list.put.item >= elem
   do
      list.put (elem)
   end

The dynamic type set of argument i of feature put of type LIST_ANY becomes {INTEGER, STRING}. Same thing for attribute item of type LIST_ANY. DTSA will thus fail to report this system as CAT-call free.


The following system will be used for examples:

class
   LIST_ANY
feature
   put (i: ANY) is
      do
         item := i
      end
   item: ANY
end
class
   LIST_STRING
inherit
   LIST_ANY
      redefine put, item end
feature
   put (i: STRING) is
      do
         item := i
      end	
   item: STRING
end