Difference between revisions of "DynamicTypeSet"
m |
m |
||
| Line 1: | Line 1: | ||
| + | ====CAT-Call 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: | 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 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. | ||
An algorithm that makes errors of kind B is of no use. An algorithm that only makes errors of kind A leads to type safety. But too many errors of kind A limit its useless (the trivial algorithm, that reports every Eiffel system as NOT CAT call free makes no errors of Kind B bot is completely useless). | An algorithm that makes errors of kind B is of no use. An algorithm that only makes errors of kind A leads to type safety. But too many errors of kind A limit its useless (the trivial algorithm, that reports every Eiffel system as NOT CAT call free makes no errors of Kind B bot is completely useless). | ||
| − | The goal is thus to find | + | 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. |
| − | + | ||
| − | + | ====Dynamic type set algorithm==== | |
| − | + | ||
| + | |||
| + | The dynamic type set algorithm (DTSA) as defined in ETL2 combined with a system validity check, removes the most serious holes in the Eiffel type system. | ||
| − | + | ||
can make two kinds of errors | can make two kinds of errors | ||
| Line 16: | Line 20: | ||
But for some systems it is easy to show, that they are CAT call free. | But for some systems it is easy to show, that they are CAT call free. | ||
| − | |||
The challenge is thus to find the | The challenge is thus to find the | ||
So DTSA cannot do that, | So DTSA cannot do that, | ||
it will correctly declare some Eiffel systems as CAT call free | it will correctly declare some Eiffel systems as CAT call free | ||
Revision as of 15:29, 10 November 2006
CAT-Call 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.
An algorithm that makes errors of kind B is of no use. An algorithm that only makes errors of kind A leads to type safety. But too many errors of kind A limit its useless (the trivial algorithm, that reports every Eiffel system as NOT CAT call free makes no errors of Kind B bot 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.
Dynamic type set algorithm
The dynamic type set algorithm (DTSA) as defined in ETL2 combined with a system validity check, removes the most serious holes in the Eiffel type system.
can make two kinds of errors
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 * detects a subset of all CAT-call free
But for some systems it is easy to show, that they are CAT call free.
The challenge is thus to find the So DTSA cannot do that, it will correctly declare some Eiffel systems as CAT call free
