DynamicTypeSet - Revision history

Conaclos: Remove 'is' keyword

2013-08-19T16:35:24Z

Remove 'is' keyword

2007-04-11T10:06:04Z

2006-11-20T17:58:39Z

‎Proof obligation based algorithm

2006-11-18T01:10:29Z

‎Dynamic type set algorithm

2006-11-18T00:43:52Z

Added category

2006-11-15T18:28:31Z

‎Proof obligation based algorithm

2006-11-15T18:27:33Z

‎Proof obligation based algorithm

2006-11-14T22:14:58Z

‎CAT-Call freeness detection algorithms

2006-11-14T22:12:58Z

2006-11-14T22:05:30Z

‎Dynamic type set algorithm

@@ Line 65: / Line 65: @@
 |-valign="top" -halign="center"
+|
-<code>[eiffel,N]
+<e>
-foo is
+foo
     local
        l1: LIST_ANY
@@ Line 79: / Line 79: @@
        double_list (l2)
     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
        l.put (l.item)
@@ Line 97: / Line 97: @@
     end
-</code>
+</e>
 |}

@@ Line 2: / Line 2: @@
 Author: Matthias Konrad
-{{Warning|'''Warning''': Article under development}}
+{{UnderConstruction}}
 ====CAT-Call freeness detection algorithms====

← Older revision		Revision as of 17:58, 20 November 2006
Line 39:		Line 39:
	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==		==Proof obligation based algorithm==

@@ Line 11: / Line 11: @@
 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.

@@ Line 128: / Line 128: @@
     put (i: STRING) is
        do
-          i.to_lower
+          item := i
        end
     item: STRING

@@ Line 40: / Line 40: @@
 ==Proof obligation based algorithm==
-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''. In Eiffel an obligation made to a caller is a precondition.
+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.
 A better algorithm should detect what feature ''merge'' depends on to work properly.

@@ Line 7: / Line 7: @@
 * 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).
+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.

← Older revision		Revision as of 22:12, 14 November 2006
Line 1:		Line 1:
	Author: Matthias Konrad		Author: Matthias Konrad
		+
		+	{{Warning\|'''Warning''': Article under development}}

	====CAT-Call freeness detection algorithms====		====CAT-Call freeness detection algorithms====

@@ Line 18: / Line 18: @@
        f /= Void
        t /= Void
     do
        from f.start until f.after loop