http://termination-portal.org/mediawiki/api.php?action=feedcontributions&user=C-Otto&feedformat=atomTermination-Portal.org - User contributions [en]2024-03-28T13:30:30ZUser contributionsMediaWiki 1.34.2http://termination-portal.org/mediawiki/index.php?title=User_talk:Flowgenerator&diff=1313User talk:Flowgenerator2013-05-29T19:13:42Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:C-Otto|C-Otto]] ([[User talk:C-Otto|talk]]) 21:13, 29 May 2013 (CEST)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1308Java Bytecode2013-01-31T11:21:18Z<p>C-Otto: </p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[[Tools:Julia|Julia]],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Version ===<br />
The bytecode major version must be 50 (Java 6) or lower. Version 51 (Java 7) is not allowed.<br />
<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from a Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set of Java 6, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1307Java Bytecode2013-01-28T09:43:09Z<p>C-Otto: /* Considered Types */</p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[[Tools:Julia|Julia]],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from a Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Peter_Schneider-Kamp&diff=1305People:Peter Schneider-Kamp2012-11-28T09:39:38Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Peter<br />
|middlenames=<br />
|lastname=Schneider-Kamp<br />
|titles=<br />
|email=petersk@imada.sdu.dk<br />
|homepage=http://imada.sdu.dk/~petersk/<br />
|country=Denmark<br />
|university=University of Southern Denmark, Odense<br />
|department=Mathematics and Computer Science<br />
|role=Associate Professor <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --><br />
<br />
[http://imada.sdu.dk/~petersk/ http://imada.sdu.dk/~petersk/petersk_floc2010.jpg]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1278Termination Portal2012-06-27T08:57:38Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1277Termination Portal2012-06-27T08:47:33Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DPL><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DPL><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Template:Extension_DPL&diff=1276Template:Extension DPL2012-06-27T08:45:48Z<p>C-Otto: Template:Extension DPL</p>
<hr />
<div><noinclude>This page was automatically created. It serves as an anchor page for all '''[[Special:WhatLinksHere/Template:Extension_DPL|invocations]]''' of [http://mediawiki.org/wiki/Extension:DynamicPageList Extension:DynamicPageList (DPL)].</noinclude></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1272Termination Portal2012-06-26T20:16:36Z<p>C-Otto: /* Testing */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1270Termination Portal2012-06-26T20:15:36Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
=Testing=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=created<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1268Termination Portal2012-06-26T20:13:13Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1262Termination Portal2012-06-26T14:52:24Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=100<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=News:Termination_Competition_2012:_June_26_-_June_29&diff=1261News:Termination Competition 2012: June 26 - June 292012-06-26T14:52:16Z<p>C-Otto: </p>
<hr />
<div>{{News<br />
|text=The [[Termination Competition 2012]] takes place "live" during the [http://ijcar.cs.manchester.ac.uk/ IJCAR conference]. <br />
|date=June 26 - June 29, 2012<br />
}}</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1260Termination Portal2012-06-26T14:52:01Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1259Termination Portal2012-06-26T14:51:51Z<p>C-Otto: /* Recent News */</p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=1000<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=News:Termination_Competition_2012:_June_26_-_June_29&diff=1257News:Termination Competition 2012: June 26 - June 292012-06-26T14:50:42Z<p>C-Otto: </p>
<hr />
<div><br />
<!--<br />
Please insert the corresponding information below so that<br />
the news page can be generated automatically.<br />
<br />
Line breaks are allowed! You may use MediaWiki syntax here to link to articles, highlight text, ...<br />
Please add some date to the news entry (e.g. today's date for current news, a time period for the competition, ....).<br />
Example:<br />
|text = The [[WST]] takes place in [http://en.wikipedia.org/wiki/Juneau Juneau] this year!<br />
|date = Sep 8 - Nov 1, 2008<br />
--><br />
<br />
The [[Termination Competition 2012]] takes place "live" during the [http://ijcar.cs.manchester.ac.uk/ IJCAR conference].<br />
<br />
{{News<br />
|text=The [[Termination Competition 2012]] takes place "live" during the [http://ijcar.cs.manchester.ac.uk/ IJCAR conference]. <br />
|date=June 26 - June 29, 2012<br />
}}</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Star_Exec&diff=1233Star Exec2012-06-12T14:50:03Z<p>C-Otto: </p>
<hr />
<div>[http://www.starexec.org/ StarExec] is a cross-community solver execution and benchmark library service under joint development at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions. StarExec should be available for public use in the fall of 2012.<br />
<br />
The termination community intends to use this platform for future competitions<br />
(and other tasks, like running experiments, archiving benchmarks and results, etc.)<br />
<br />
There will be a [http://clc.cs.uiowa.edu/starexec12/ Starexec Workshop] affiliated with IJCAR 2012<br />
(Manchester). We use this wiki page here to collect and organize some points<br />
that we want to make during that workshop.<br />
<br />
Open Questions:<br />
* Format of results: The specification does not speak explicitly about the format of the results. Is this going to be handled using Post-Processors?<br />
* Scoring systems: How can a scoring system like we use for the complexity competition be implemented? Post-processors seem to be restricted to working on one solver/result pair, while our scoring needs to see all results in a competition for a given example.<br />
* Will there be "Teams"? StarExec seems to know Communitys and single users, but not about the fact that some tools are produced by a group of people.<br />
* How are benchmark sets (note: the organizers call the individual examples/problems/TRSs/... "benchmarks") organized? For example I'd like to have the official TPDB and private benchmark sets (which might be submitted to TPDB lateron). Furthermore, it is very useful to have complex ways of picking the relevant benchmark for a tool run (not just "the whole TPDB", but maybe "just the Java Bytecode benchmarks which are not yet in the TPDB"). Here having a number of user-defineable tags for each benchmark and being able to pick benchmark sets based on boolean combinations of tags can be a solution I'd like to see. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))<br />
* What further information do benchmarks have? We made good experience with storing information about the expected result (entered manually), so that runs giving a different result can be identified easily. Furthermore, it is useful to get a list of tool runs in which the specific benchmark could be solved. Statistical data (for example: this benchmark has never been solved, yet) is useful, too. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Star_Exec&diff=1232Star Exec2012-06-12T14:49:01Z<p>C-Otto: </p>
<hr />
<div>[http://www.starexec.org/ StarExec] is a cross-community solver execution and benchmark library service under joint development at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions. StarExec should be available for public use in the fall of 2012.<br />
<br />
The termination community intends to use this platform for future competitions<br />
(and other tasks, like running experiments, archiving benchmarks and results, etc.)<br />
<br />
There will be a [http://clc.cs.uiowa.edu/starexec12/ Starexec Workshop] affiliated with IJCAR 2012<br />
(Manchester). We use this wiki page here to collect and organize some points<br />
that we want to make during that workshop.<br />
<br />
Open Questions:<br />
* Format of results: The specification does not speak explicitly about the format of the results. Is this going to be handled using Post-Processors?<br />
* Scoring systems: How can a scoring system like we use for the complexity competition be implemented? Post-processors seem to be restricted to working on one solver/result pair, while our scoring needs to see all results in a competition for a given example.<br />
* Will there be "Teams"? StarExec seems to know Communitys and single users, but not about the fact that some tools are produced by a group of people.<br />
* How are benchmark sets (note: the organizers call the individual examples/problems/TRSs/... "benchmarks") organized? For example I'd like to have the official TPDB and private example sets (which might be submitted to TPDB lateron). Furthermore, it is very useful to have complex ways of picking the relevant examples for a benchmark run (not just "the whole TPDB", but maybe "just the Java Bytecode examples which are not yet in the TPDB"). Here having a number of user-defineable tags for each example and being able to pick example sets based on boolean combinations of tags can be a solution I'd like to see. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))<br />
* What further information do examples have? We made good experience with storing information about the expected result (entered manually), so that runs giving a different result can be identified easily. Furthermore, it is useful to get a list of runs in which the specific example could be solved. Statistical data (for example: this example has never been solved, yet) is useful, too. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Star_Exec&diff=1231Star Exec2012-06-12T14:46:23Z<p>C-Otto: </p>
<hr />
<div>[http://www.starexec.org/ StarExec] is a cross-community solver execution and benchmark library service under joint development at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions. StarExec should be available for public use in the fall of 2012.<br />
<br />
The termination community intends to use this platform for future competitions<br />
(and other tasks, like running experiments, archiving benchmarks and results, etc.)<br />
<br />
There will be a [http://clc.cs.uiowa.edu/starexec12/ Starexec Workshop] affiliated with IJCAR 2012<br />
(Manchester). We use this wiki page here to collect and organize some points<br />
that we want to make during that workshop.<br />
<br />
Open Questions:<br />
* Format of results: The specification does not speak explicitly about the format of the results. Is this going to be handled using Post-Processors?<br />
* Scoring systems: How can a scoring system like we use for the complexity competition be implemented? Post-processors seem to be restricted to working on one solver/result pair, while our scoring needs to see all results in a competition for a given example.<br />
* Will there be "Teams"? StarExec seems to know Communitys and single users, but not about the fact that some tools are produced by a group of people.<br />
* How are example sets organized? For example I'd like to have the official TPDB and private example sets (which might be submitted to TPDB lateron). Furthermore, it is very useful to have complex ways of picking the relevant examples for a benchmark run (not just "the whole TPDB", but maybe "just the Java Bytecode examples which are not yet in the TPDB"). Here having a number of user-defineable tags for each example and being able to pick example sets based on boolean combinations of tags can be a solution I'd like to see. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))<br />
* What further information do examples have? We made good experience with storing information about the expected result (entered manually), so that runs giving a different result can be identified easily. Furthermore, it is useful to get a list of runs in which the specific example could be solved. Statistical data (for example: this example has never been solved, yet) is useful, too. ([[User:C-Otto|C-Otto]] 16:46, 12 June 2012 (CEST))</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Carsten_Otto&diff=1178People:Carsten Otto2011-11-29T07:30:02Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Carsten<br />
|middlenames=<br />
|lastname=Otto<br />
|titles=<br />
|email=otto@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/otto/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --><br />
<br />
[http://verify.rwth-aachen.de/otto/ http://verify.rwth-aachen.de/otto/otto.jpg]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Carsten_Otto&diff=1177People:Carsten Otto2011-11-29T07:29:00Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Carsten<br />
|middlenames=<br />
|lastname=Otto<br />
|titles=<br />
|email=otto@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/otto/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --><br />
<br />
[http://verify.rwth-aachen.de/otto/ http://verify.rwth-aachen.de/otto/otto.jpg]<br />
<poll><br />
Test Poll2<br />
Th2is poll is nice.<br />
No 2one likes this poll.<br />
Poll2y want crackers!<br />
</poll></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Carsten_Otto&diff=1176People:Carsten Otto2011-11-29T07:28:37Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Carsten<br />
|middlenames=<br />
|lastname=Otto<br />
|titles=<br />
|email=otto@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/otto/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --><br />
<br />
[http://verify.rwth-aachen.de/otto/ http://verify.rwth-aachen.de/otto/otto.jpg]<br />
<poll><br />
Test Poll<br />
This poll is nice.<br />
No one likes this poll.<br />
Polly want crackers!<br />
</poll></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Portal&diff=1174Termination Portal2011-11-29T07:07:26Z<p>C-Otto: </p>
<hr />
<div>Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.<br />
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).<br />
<br />
This portal aims to provide the research community with up-to-date information about the field<br />
of termination analysis.<br />
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),<br />
[[:Category:News|News]] (information about events and new publications),<br />
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and<br />
[[:Category:Bibtex|References]] (publications related to termination analysis). <br />
Additionally, the portal provides information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].<br />
<br />
Have [[Suggestions]] to improve this web resource?<br />
- How to [[Contribute]].<br />
<br />
=Recent News=<br />
<DynamicPageList><br />
category=News<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage={News}:date:text<br />
format =,,\n,<br />
table =class="wikitable",Caption,Date,Text<br />
tablerow =|%%<br />
</DynamicPageList><br />
Older news entries can be found on the [[:Category:News|news page]].<br />
<br />
<!--<br />
=New Publications=<br />
<DynamicPageList><br />
category=BibtexNews<br />
shownamespace=false<br />
count=10<br />
ordermethod=lastedit<br />
order=descending<br />
includepage=%1[100]<br />
format =,,\n,<br />
table =class="wikitable",Name,Content<br />
tablerow =|%%<br />
</DynamicPageList><br />
--></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Termination_Competition_2011&diff=1162Termination Competition 20112011-05-24T18:06:54Z<p>C-Otto: </p>
<hr />
<div>[https://listes.ens-lyon.fr/sympa/arc/rewriting/2011-04/msg00009.html Call for participation]<br />
<br />
Important dates<br />
<br />
* Software requests: May 13 2011<br />
* Problem submission: May 27 2011, 13:01 CEST<br />
* Tool submission: May 27 2011, 13:01 CEST<br />
* Competition start: May 30 2011, 09:00 CEST<br />
<br />
The [http://termcomp.uibk.ac.at/2011/rules.html rules of the competition] and <br />
[http://termcomp.uibk.ac.at/2011/index.html further information on the computer running the experiments] can be found on<br />
the [http://termcomp.uibk.ac.at/ termination competition] website.</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Marc_Brockschmidt&diff=1148People:Marc Brockschmidt2011-04-11T14:34:45Z<p>C-Otto: Created page with "<!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yoursel..."</p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Marc<br />
|middlenames=<br />
|lastname=Brockschmidt<br />
|titles=<br />
|email=brockschmidt@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/brockschmidt/<br />
|country=Germany<br />
|university=RWTH Aachen<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant<br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Mmjb&diff=1147User talk:Mmjb2011-04-11T14:34:26Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:C-Otto|C-Otto]] 16:34, 11 April 2011 (CEST)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Cryingshadow&diff=1146User talk:Cryingshadow2011-04-11T14:08:18Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!'''<br />
We hope you will contribute much and well.<br />
You will probably want to read the [[Help:Contents|help pages]].<br />
Again, welcome and have fun! [[User:C-Otto|C-Otto]] 16:08, 11 April 2011 (CEST)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Carsten_Otto&diff=1145People:Carsten Otto2011-04-11T13:54:10Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Carsten<br />
|middlenames=<br />
|lastname=Otto<br />
|titles=<br />
|email=otto@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/otto/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --><br />
<br />
[http://verify.rwth-aachen.de/otto/ http://verify.rwth-aachen.de/otto/otto.jpg]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Thomas_Str%C3%B6der&diff=1144People:Thomas Ströder2011-04-11T13:53:56Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Thomas<br />
|middlenames=<br />
|lastname=Ströder<br />
|titles=<br />
|email=stroeder@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/stroeder/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=Research Group Computer Science 2<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Thomas_Str%C3%B6der&diff=1143People:Thomas Ströder2011-04-11T13:53:36Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Thomas<br />
|middlenames=<br />
|lastname=Ströder<br />
|titles=<br />
|email=stroeder@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/stroeder/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=<br />
|role=Research and Teaching Assistant <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Thomas_Str%C3%B6der&diff=1142People:Thomas Ströder2011-04-11T13:52:52Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=Thomas<br />
|middlenames=<br />
|lastname=Ströder<br />
|titles=<br />
|email=stroeder@informatik.rwth-aachen.de<br />
|homepage=http://verify.rwth-aachen.de/stroeder/<br />
|country=Germany<br />
|university=RWTH Aachen University<br />
|department=<br />
|role=PhD Student <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Thomas_Str%C3%B6der&diff=1141People:Thomas Ströder2011-04-11T13:52:01Z<p>C-Otto: Created page with "<!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yoursel..."</p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname=<br />
|middlenames=<br />
|lastname=<br />
|titles=<br />
|email=<br />
|homepage=<br />
|country=<br />
|university=<br />
|department=<br />
|role= <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=People:Manh_Thang_Nguyen&diff=1140People:Manh Thang Nguyen2011-04-11T13:49:32Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that you can be added to some default<br />
categories and a simple user page can be created. You may extend<br />
that user page yourself after the following code block.<br />
--><br />
<br />
{{Person<br />
|firstname= Thang<br />
|middlenames= Manh<br />
|lastname= Nguyen<br />
|titles=<br />
|email= manhthang.nguyen@cs.kuleuven.be<br />
|homepage= http://www.cs.kuleuven.be/~manh<br />
|country= Belgium<br />
|university= KULeuven<br />
|department= Computer Science<br />
|role= PhD student <!-- role: Student, Professor, PhD Student, ... --><br />
}}<br />
(Manh Thang Nguyen deceased in 2009)<br />
<!-- If you want to add some personal data to your userpage, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1139Java Bytecode2011-03-28T12:28:28Z<p>C-Otto: (forbidden native method) Undo revision 1138 by C-Otto (talk)</p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[[Tools:Julia|Julia]],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1138Java Bytecode2011-03-28T12:27:20Z<p>C-Otto: </p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''(new Object()).hashCode()''' or '''args.length''' or '''args[i].length()''' one gets unknown (for the last two options: non-negative) '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[[Tools:Julia|Julia]],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=News:Termination_Competition_2010_in_July&diff=1122News:Termination Competition 2010 in July2010-08-19T09:55:43Z<p>C-Otto: </p>
<hr />
<div>{{News<br />
|text=The [[Termination_Competition_2010|Termination Competition 2010]] will be run during FLoC in July.<br />
|date=July, 2010<br />
}}</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Kdoss&diff=1121User talk:Kdoss2010-07-26T07:27:11Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well. <br />
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:C-Otto|C-Otto]] 07:27, 26 July 2010 (UTC)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Dean_Voets&diff=1111User talk:Dean Voets2010-06-24T13:25:26Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well. <br />
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:C-Otto|C-Otto]] 13:25, 24 June 2010 (UTC)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Arubio&diff=1092User talk:Arubio2010-05-14T11:55:23Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well. <br />
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:C-Otto|C-Otto]] 11:55, 14 May 2010 (UTC)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Complexity:Old&diff=1051Complexity:Old2010-03-26T13:55:08Z<p>C-Otto: /* Complexity proof techniques */</p>
<hr />
<div>This page is to record the current status of discussion<br />
on the proposed Complexity Category of the Termination Competition. <br />
<br />
== Overview of the Event ==<br />
<br />
It is a challenging topic to automatically determine upper bounds on<br />
the complexity of rewrite systems. By complexity of a TRS, we mean<br />
the maximal length of derivations, where either no restrictions on the<br />
initial terms are present ("derivational complexity") or only<br />
constructor based terms are considered ("runtime complexity"). See<br />
(Hirokawa, Moser, 2008) for further reading on the notion of runtime<br />
complexity. Additionally one distinguishes between complexities<br />
induced by full rewriting as opposed to complexities induced by<br />
specific strategies, as for example innermost rewriting.<br />
We propose four sub-categories:<br />
# Derivational Complexity (DC),<br />
# innermost Derivational Complexity (iDC),<br />
# Runtime Complexity (RC), and <br />
# innermost Runtime Complexity (iRC)<br />
<br />
== Syntax/Semantics for Input/Output ==<br />
<br />
As competition semantics, we propose to focus on <em>polynomial</em><br />
bounds. <br />
<br />
=== Input Format === <br />
Problems will be given in the newly TPDB-format, cf. <br />
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where <br />
the XML-element ''problem'' will have the type ''complexity'' given. <br />
Further, depending on the category DC, iDC, RC and iRC, the attributes <br />
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based<br />
respectively. <br />
In particluar, this allows the upload of one single tool for all categories the authors want to participate in. <br />
<br />
<br />
=== Output Format === <br />
The output format is adapted so that additional<br />
information on the asymptotic complexity is given for lower as well<br />
as upper bounds. Hence the output written to the first line of STDOUT<br />
shall be a complexity statement according to the following grammar:<br />
<br />
<pre><br />
S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)<br />
F -> O(1) | O(n^Nat) | POLY<br />
</pre><br />
<br />
where "Nat" is a non-zero natural number and YES(F1, F2) means F2 is<br />
upper bound and that F1 is a lower-bound. "O(n^k)" is the usual big-Oh<br />
notation and "POLY" indicates an unspecified polynomial. Either of<br />
the functions F1, F2 (but not both) may be replaced by ``don't know'',<br />
indicated by ?. Any remaining output on STDOUT will be considered as<br />
proof output and has to follow the normal rules for the competition.<br />
<br />
<em>Example</em>: Consider R= {a(a(x)) -> b(c(x)), b(b(x)) -> a(c(x)), c(c(x)) -> a(b(x))}. Within<br />
the derivational complexity category a syntactically correct output would be "YES(O(n^2),POLY)". <br />
(Whether this output would also indicate a correct tool, is another question.)<br />
<br />
== Scoring ==<br />
<br />
Currently we focus on (polynomial) <em>upper</em> bounds. As<br />
the output format indicates, this restriction should be lifted<br />
later, see below. In order to take into account the quality of the upper<br />
bound provided by the different tools, we propose the following<br />
scoring algorithm, where we suppose the number of competitors is x.<br />
<br />
Firstly, for each TRS the competing tools are ranked, where constant<br />
complexity, i.e., output "YES(?,O(1))" is best and "MAYBE", "NO" or<br />
time-out is worst.<br />
As long as the output is of form "YES(?,O(n^k))" or "YES(?,POLY)" the<br />
rank of the tool defines the number of points. More precisely the<br />
best tool gets x+1 points, the second gets x points and so on. On the<br />
other hand a negative output ("MAYBE", "NO" or time-out) gets 0<br />
points.<br />
If two or more tools would get the same rank, the rank of the<br />
remaining tools is adapted in the usual way.<br />
<br />
Secondly, all resulting points for all considered systems are summed<br />
up and the contestant with the highest number of points wins. If this<br />
cannot establish a winner, the total number of wins is counted. If<br />
this still doesn't produce a winner, we give up and provide two (or<br />
more) winners.<br />
<br />
The maximal allowed CPU time is 60 seconds.<br />
<br />
== Problem selection ==<br />
<br />
We propose to run subcategories DC and iDC<br />
on all TRS and SRS families from the newly organised TPDB, after <br />
the selection function defined below has been applied. <br />
For categories RC and iRC, we propose to run the competition on all TRS families<br />
after application of the selection function stated below:<br />
<br />
=== Selection function === <br />
<br />
In the following, we denote by ''select'' the function that relates<br />
each family from the TPDB to the number of randomly chosen examples within this family as defined <br />
for the termination competition. <br />
The idea is to make ''select''<br />
aware of different difficulties of proving complexity bounds. We do so by<br />
# partitioning each family ''F'' into ''n'' different sets ''F = F_1 \cup ... \cup F_n'', where the sets ''F_i'' may be seen as collections of TRSs similar in difficulty. For this years competition we propose following partitioning of a family ''F'':<br />
#:* '''subcategories RC, iRC and iDC:''' we propose to partition each family into <br />
#:*:(i) those upon which a polynomial bound could be shown automatically in last years competition (denoted by ''F_auto'' below) and <br />
#:*:(ii) those where a polynomial bound could not be shown (''F_nonauto''). <br />
#:* '''subcategory DC:''' as above, but we split (ii) into duplicating TRS (''F_duplicating'') and non-duplicating TRSs (note that any TRS from (i) is non-duplicating)<br />
# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F'' such that ''p(F_1) + ... p(F_n) = 1''. For this year's competition we propose the following distribution: <br />
#:for all subcategories and families ''F'', we propose ''p(F_auto) = 0.4'' and ''p(F_nonauto) = 0.6'' (For the category DC, we additionally set ''p(F_duplicating) = 0.0''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''select_comp(F,i) = min(|F_i|, p(i) * select(F))''. Here ''|F_i|'' denotes the size of ''F_i''. <br />
# From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.<br />
<br />
== Test Cases == <br />
In the following test cases we restrict to full rewriting.<br />
<em><br />
test cases - derivational complexity <br />
</em><br />
<br />
<pre><br />
R = {a(b(x)) -> b(a(x))}, expected output "YES(?,O(n^2))" or "YES(O(n^1),O(n^2))" or "YES(O(n^2),O(n^2))"<br />
<br />
R= {a(a(x)) -> b(c(x)), b(b(x)) -> a(c(x)), c(c(x)) -> a(b(x))}, expected output "YES(O(n^2),?)" or "YES(?,?)"<br />
<br />
R= {+(s(x),+(y,z)) -> +(x,+(s(s(y)),z)), +(s(x),+(y,+(z,w))) -> +(x,+(z,+(y,w)))}, expected output "YES(?,?)"<br />
</pre><br />
<br />
<em>test cases - runtime complexity </em><br />
<pre><br />
R = {a(b(x)) -> b(b(a(x)))}, expected output "YES(?,O(n^1))" or "YES(O(n^1),O(n^1))"<br />
<br />
R = {plus(0,y) -> y, plus(s(x),y) -> s(plus(x,y)), mul(0,y) -> 0, mul(s(x),y) -> plus(mul(x,y),y)}, expected output "YES(?,O(n^2))" or "YES(O(n^1),O(n^2))" or "YES(O(n^2),O(n^2))"<br />
<br />
R = {f(x,0) -> s(0), f(s(x),s(y)) -> s(f(x,y)), g(0,x) -> g(f(x,x),x)}, expected output "YES(?,O(n^1))" or "YES(O(n^1),O(n^1))"<br />
<br />
R= {f(0) -> c, f(s(x)) -> c(f(x),f(x))}, expected output "YES(?,?)"<br />
</pre><br />
<br />
In the following test cases we restrict to innermost rewriting.<br />
<br />
<em>test cases - derivational complexity </em><br />
<pre><br />
R = {f(x) -> c(x,x)}, expected output "YES(O(n^1),O(n^1))" or "YES(?,O(n^1))"<br />
</pre><br />
<br />
<em>test cases - runtime complexity </em><br />
<pre><br />
R= {f(x) -> c(x,x), g(0) -> 0, g(s(x)) -> f(g(x))}, expected output "YES(O(n^1),O(n^1))" or "YES(?,O(n^1))"<br />
</pre><br />
<br />
<br />
== Participation ==<br />
<br />
=== Requirements ===<br />
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.<br />
<br />
=== Participants ===<br />
<br />
Insert your name here if you intend to participate:<br />
<br />
==== Competition 2009 ====<br />
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])<br />
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)<br />
<br />
==== Competition 2008 ====<br />
* M. Avanzini, G. Moser, A. Schnabl (TCT)<br />
* N. Hirokawa (Hydra), but might need more time<br />
* M. Korp, C. Sternagel, H. Zankl (CaT)<br />
<br />
== Complexity proof techniques ==<br />
<br />
A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]<br />
<br />
== Discussion ==<br />
<br />
=== lower bounds ===<br />
<br />
In the future the tools should also be able to provide certificates on the<br />
lower bound. This would imply to extend the grammar as follows<br />
<br />
<pre><br />
F -> O(1) | O(n^Nat) | POLY | EXP | INF<br />
</pre><br />
<br />
such that e.g. "YES(EXP,?)" indicated an exponential lower-bound,<br />
or "YES(INF,INF)" indicated non-termination. <br />
<br />
(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)<br />
<br />
Scoring (proposals):<br />
<br />
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)<br />
<br />
* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from <br />
<PRE><br />
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2<br />
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".<br />
This would imply that if all answers are identical, then no-one gets a point.<br />
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" - <br />
so anyone who gives a better answer, gets at least one point.<br />
<br />
=== Concrete syntax ===<br />
<br />
* JW would prefer the following output format as it is easier to parse:<br />
<br />
F -> POLY(Nat) | POLY(?)<br />
<br />
Here "POLY(k)" abbreviates "O(n^k)" and "POLY(?)" denotes an unspecified<br />
polynomial.<br><br />
<br />
<em>resolved</em><br />
<br />
* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)<br />
<br />
* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4<br />
<br />
LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower<br />
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1032Java Bytecode2009-12-22T10:01:58Z<p>C-Otto: </p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[[Tools:Julia|Julia]],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Tools:Julia&diff=1031Tools:Julia2009-12-22T09:57:11Z<p>C-Otto: </p>
<hr />
<div><!--<br />
Please fill in the data so that your tool can be added to some default<br />
categories and a simple tool page can be created. You may extend<br />
that tool page yourself after the following code block.<br />
<br />
Please use the "publication" field to add a reference to a publication<br />
introducing your tool. The "References" page can be used to enter a bibtex<br />
record for this publication.<br />
Example: |publication=[[Bibtex:Giesl04|Automated Termination Proofs with AProVE]]<br />
--><br />
<br />
{{Tool<br />
|shortname=Julia<br />
|longname=Julia<br />
|homepage=http://julia.scienze.univr.it/<br />
|country=Italy and France<br />
|university=University of Verona and University of Reunion<br />
|developers=Fausto Spoto, Fred Mesnard, and Etienne Payet<br />
|publication=<br />
}}<br />
<br />
<!-- If you want to add some additional information to the tool page, you can do so after this comment. --></div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=User_talk:Fred&diff=1029User talk:Fred2009-12-22T07:20:41Z<p>C-Otto: Welcome!</p>
<hr />
<div>'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well. <br />
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:C-Otto|C-Otto]] 07:20, 22 December 2009 (UTC)</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1028Java Bytecode2009-12-21T14:52:45Z<p>C-Otto: /* Categories */</p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[http://julia.scienze.univr.it:8080/julia/ Julia],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
The JBC problems are divided into two categories.<br />
One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.<br />
<br />
The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1027Java Bytecode2009-12-21T14:51:30Z<p>C-Otto: /* Participants */</p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[http://julia.scienze.univr.it:8080/julia/ Julia],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC categories.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
We propose to have two categories of Java Bytecode problems. One category<br />
contains programs with recursion and one only contains programs without<br />
recursion. The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1026Java Bytecode2009-12-21T14:50:10Z<p>C-Otto: </p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== Participants ==<br />
In the 2009 competition the tools<br />
[http://julia.scienze.univr.it:8080/julia/ Julia],<br />
[http://costa.ls.fi.upm.es/costa/costa.php COSTA] and<br />
[[Tools:AProVE|AProVE]] took part in the JBC category.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
We propose to have two categories of Java Bytecode problems. One category<br />
contains programs with recursion and one only contains programs without<br />
recursion. The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Java_Bytecode&diff=1025Java Bytecode2009-12-21T14:48:32Z<p>C-Otto: </p>
<hr />
<div>This page is to record the current status of the Java Bytecode (JBC) Category of the Termination Competition.<br />
(Discussion should take place on the termtools mailing list.) <br />
== Java vs. Java Bytecode ==<br />
Every Java problem can be compiled into an equivalent Java Bytecode problem.<br />
For technical reasons, the current tools only work on this compiled version of the original program.<br />
However, the result of the analysis also gives information about the termination behaviour of the original Java program.<br />
<br />
Every JBC problem that resulted out of Java source code should include this source in addition to the compiled class files.<br />
This way we can communicate that we are interested in termination analysis of a real imperative programming language.<br />
<br />
As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.<br />
<br />
There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).<br />
The JBC category can be filled with corresponding problems.<br />
Here, too, the source files used to generate the JBC code should be provided.<br />
== Problem definition ==<br />
A JBC problem is defined by up to three parts.<br />
<br />
* byte code<br />
* source<br />
* start method<br />
<br />
=== Code ===<br />
Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.<br />
=== Java Source ===<br />
This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.<br />
<br />
=== Start Method ===<br />
Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.<br />
<br />
Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.<br />
<br />
public static void main(String[] args) {<br />
// create list of given length<br />
List list = new List(args.length);<br />
<br />
// work on the created list<br />
doSomething(list);<br />
}<br />
<br />
== (Possible) Participants ==<br />
[http://julia.scienze.univr.it:8080/julia/ Julia], [http://costa.ls.fi.upm.es/costa/costa.php COSTA] and [[Tools:AProVE|AProVE]] are able to work on Java Bytecode problems.<br />
<br />
== Details ==<br />
=== Errors and Exceptions === <br />
In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.<br />
If an example problem triggers this, we should consider this example as broken and not use it in the competition.<br />
<br />
=== Considered Types ===<br />
Exactly the types provided in the .jar file are considered, with a few additions needed for basic examples.<br />
<br />
The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.<br />
<br />
All additional class files are taken from the current Debian version of<br />
OpenJDK [1].<br />
<br />
The class '''java.lang.String''' needs to be considered. Especially the method<br />
'''String.length()I''' is useful to construct problem instances out of the<br />
argument array of the initial method ('''String[] args''').<br />
<br />
To be able to initialize '''java.lang.String''', we also need the classes<br />
'''java.lang.String$CaseInsensitiveComparator''',<br />
'''java.util.Comparator''', and '''java.io.ObjectStreamField'''.<br />
<br />
Furthermore, usage of all the exceptions/errors mentioned in the JVMS is allowed (all in '''java.lang.*'''):<br />
* AbstractMethodError<br />
* ArithmeticException<br />
* ArrayIndexOutOfBoundsException<br />
* ArrayStoreException<br />
* ClassCastException<br />
* IllegalAccessError<br />
* IncompatibleClassChangeError<br />
* NegativeArraySizeException<br />
* NoClassDefFoundError<br />
* NoSuchFieldError<br />
* NoSuchMethodError<br />
* NullPointerException<br />
<br />
Because all array types implement '''java.lang.Cloneable''' and<br />
'''java.io.Serializable''', these interfaces must also be allowed.<br />
<br />
The following types are part of the hierarchy of a type<br />
mentioned before, so they must be included (all in '''java.lang.*'''):<br />
* CharSequence<br />
* Comparable<br />
* Error<br />
* Exception<br />
* IndexOutOfBoundsException<br />
* LinkageError<br />
* Object<br />
* RuntimeException<br />
* Throwable<br />
<br />
==== Native Methods ====<br />
To initialize '''Object''', we need to implement the native method '''Object.registerNatives()V'''.<br />
This method is implemented "no-op".<br />
To actually throw instances of '''Exception''' (or '''Throwable''' in general), the native method<br />
'''Throwable.fillInStackTrace()V''' needs to be implemented. This method, too, is implemented as "no-op".<br />
<br />
The remaining native methods are not considered (all in '''java.lang.*'''):<br />
* Object.clone()Ljava/lang/Object;<br />
* Object.getClass()Ljava/lang/Class;<br />
* Object.hashCode()I<br />
* Object.notifyAll()V<br />
* Object.notify()V<br />
* Object.wait(J)<br />
* String.intern()Ljava/lang/String;<br />
<br />
==== Example ====<br />
<br />
As an example, examples calling<br />
'''java.lang.Object.equals(Ljava/lang/Object;)Z''' are allowed, but the method<br />
'''java.lang.Object.toString()Ljava/lang/String;''' may not be called because the class<br />
'''java.lang.StringBuilder''' is unknown.<br />
<br />
==== Included Files ====<br />
* java/io/ObjectStreamField.class<br />
* java/io/Serializable.class<br />
* java/lang/AbstractMethodError.class<br />
* java/lang/ArithmeticException.class<br />
* java/lang/ArrayIndexOutOfBoundsException.class<br />
* java/lang/ArrayStoreException.class<br />
* java/lang/CharSequence.class<br />
* java/lang/ClassCastException.class<br />
* java/lang/Cloneable.class<br />
* java/lang/Comparable.class<br />
* java/lang/Error.class<br />
* java/lang/Exception.class<br />
* java/lang/IllegalAccessError.class<br />
* java/lang/IncompatibleClassChangeError.class<br />
* java/lang/IndexOutOfBoundsException.class<br />
* java/lang/LinkageError.class<br />
* java/lang/NegativeArraySizeException.class<br />
* java/lang/NoClassDefFoundError.class<br />
* java/lang/NoSuchFieldError.class<br />
* java/lang/NoSuchMethodError.class<br />
* java/lang/NullPointerException.class<br />
* java/lang/Object.class<br />
* java/lang/RuntimeException.class<br />
* java/lang/String$CaseInsensitiveComparator.class<br />
* java/lang/String.class<br />
* java/lang/Throwable.class<br />
* java/util/Comparator.class<br />
<br />
[1]: rt.jar in:<br />
openjdk-6-jre-headless_6b11-9.1+lenny2_amd64.deb:<br />
http://packages.debian.org/lenny/amd64/openjdk-6-jre-headless/download<br />
Exact Size 22423776 Byte (21.4 MByte)<br />
MD5 checksum 645caac427ee007eed470895fc12ab9e<br />
SHA1 checksum f2cbf934681503b648f7dceb662e086a3bda5767<br />
SHA256 checksum 349a2a500d01574906d96ca7a8ee2486415d1aba5bf2c3e4c0cc2fe8a5c00efd<br />
<br />
=== Opcodes ===<br />
All opcodes are allowed, with the following exceptions.<br />
<br />
* The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.<br />
* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.<br />
* The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.<br />
* The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.<br />
<br />
=== Overflows ===<br />
Integer overflows and related problems are not handled. This means proving<br />
termination of the following Java program snippet is not considered to be wrong.<br />
<br />
int i = 0;<br />
while (i <= 2147483647) {<br />
i++;<br />
}<br />
<br />
=== Categories ===<br />
<br />
We propose to have two categories of Java Bytecode problems. One category<br />
contains programs with recursion and one only contains programs without<br />
recursion. The reason is that recursion poses a special problem for the<br />
analysis since one has to handle the call stack properly. We think that<br />
it is interesting to evaluate the performance of termination analyzers<br />
separately for programs with and without recursion.<br />
<br />
=== Verification ===<br />
All input problems must pass the bytecode verification process. Therefore,<br />
the analyzers do not need to verify the given bytecode.<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Category:Categories&diff=1024Category:Categories2009-12-21T14:46:32Z<p>C-Otto: </p>
<hr />
<div>The tools work on different types of problems, which are listed on this page.</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Category:Categories&diff=1023Category:Categories2009-12-21T14:46:21Z<p>C-Otto: Created page with 'The tools work on different types of problems, which are listed on this site.'</p>
<hr />
<div>The tools work on different types of problems, which are listed on this site.</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=Integer_Term_Rewriting&diff=1021Integer Term Rewriting2009-12-21T14:43:00Z<p>C-Otto: moved ITRS to Integer Term Rewriting</p>
<hr />
<div>The main idea of ITRSs is to add<br />
pre-defined constructors for integers (the integers themselves) and Booleans<br />
(true / false) and arithmetic, relational and Boolean functions like <br />
<br />
+, -, *,/ ,%, >, >=, <, &&, ||, !, ... <br />
<br />
to conventional TRSs. To this<br />
aim it is necessary to extend the XTC format by the ability to represent<br />
pre-defined semantics for function symbols.<br />
Not only ITRSs, but also other extensions with pre-defined functions can be<br />
represented using this extension of the XTC format.<br />
<br />
[http://lists.lri.fr/pipermail/termtools/2009-October/000775.html full text of the proposal]<br />
<br />
[[Category:Categories]]</div>C-Ottohttp://termination-portal.org/mediawiki/index.php?title=ITRS&diff=1022ITRS2009-12-21T14:43:00Z<p>C-Otto: moved ITRS to Integer Term Rewriting</p>
<hr />
<div>#REDIRECT [[Integer Term Rewriting]]</div>C-Otto