Automatic XML Documentation Synthesis
SEAMLESS
SEAMLESS is a synthesis framework for synthesising complexity bounded algorithms. It consists of a set of generic methods, based upon various problem solving strategies, eg., divide-and-conquer, generalisation, reduction, case-based reasoning, partitioning and applying known upper and lower bounds. Having provided the domain description and further problem solving knowledge in terms of generic predicates, a solution term is automatically derived, given a problem specification and an upper or lower bound. The synthesis process is automatically evaluated. Learned knowledge will be re-used in further synthesis processes.
Selection Problem
The selection problem – used here to illustrate our approach –
is a classic problem in computer science. Given a totally ordered set of n elements,
Vi ( n ) denotes the worst-case number
of pairwise comparisons needed to find the i-th
largests among n distinct ordered keys. It is known that
V1 ( n ) = n-1, V2 ( n ) = n-2 + ⌈ log n ⌉.
Few exact values of the function are known, but upper and lower bounds were established in the mathematical literature. This knowledge was employed in the solutions of complexity-bounded selection problems automatically derived using the SEAMLESS system. The synthesis complexity is highly exponential. Hence, the discovery of new optimal non-trivial algorithms usually exhausts existing computing resources, although it is possible to improve existing bounds by incomplete searches. As a surprising result (*), a previous version of SEAMLESS synthesised a new optimal algorithm in the case i=3, n=22 which also provided a counter-example to a published lower bound.
(*) Donald Knuth, The Art of Computer Programming, Errata Volume Three
PDF (991 KB)
Traceability
A drawback of automated algorithm synthesis is that automatically constructed results are hard to understand and to validate. Proof results are either non-constructive and it is up to the user to trust the results of the computer, or the proofs are lengthy, very detailed and tedious. For these reasons, the SEAMLESS component for generating synthesis explanations has been completely redesigned. SEAMLESS generates algorithm descriptions which consist of textual descriptions, mathematical formula, diagrams and links which refer to re-used subcase solutions. The explanations are similar to textbook descriptions.
Experimental Results
Beneath, some automatically generated solutions for selection problems are assembled. In combination with lower bounds, it is proven that these algorithms are optimal. It should be mentioned that currently approximately up-to 1,5 million classe1s of isomorphic subcases will be examined during a proof search. The XML documents are stored in a file system.
Samples of Automatically Synthesised Selection Algorithms and Documentations