special issue on benchmark problems?
Aaron Stump
in Savannah, I am considering trying to put together a journal special
issue, or part of one, on benchmark problems for verified programming.
I am writing to see who might be interested in this idea, and get
some feedback on some aspects of its implementation.
The goal would be to collect a set of benchmark problems, described if
possible at least partially in a common formal language, for verified
programming. A benchmark problem as I see it is one of medium
difficulty, the sort that should require at most a few days to
implement, not a few weeks. So benchmark problems are significantly
easier than challenge problems. Certainly those are important, too,
but serve a different purpose. Creating a collection of benchmark
problems would spur us to think about what kind of examples make good
showcases for dependently typed programming or other verified
programming methods, and enable some kind of comparison, however
qualitative, of different verified programming approaches.
My current proposal, about which I would like some feedback, is to
solicit 4-5 page descriptions of benchmark problems. These should
-- explain why the problem is interesting as a benchmark; for example,
highlighting any special features (e.g., general recursion) that the
author anticipates would be necessary.
-- argue that the problem is appropriate difficulty for a benchmark
(neither trivial nor at the level of a challenge problem).
-- describe the types of all functions that are part of the benchmark,
using a common language of types; I am thinking something like CIC
would be general enough for the types (though very possibly not the
terms) of the benchmarks.
-- similarly, describe any external theorems that are part of the
benchmark, again using a common language; I again propose CIC.
-- describe in English any non-functional properties that should be
statically verified (e.g., statically verify linear running time, or
memory usage).
To ensure benchmarks are reasonable, after acceptance of a benchmark
problem paper, the author will be required to add a section detailing
her solution in whichever language she wishes. The solution should be
independently confirmable by others; for example, the author can post
the solution and information on running it through a publicly
available tool on a web page. Prior to this final version, however,
the author should try not to reveal his identity in the text, for
example by revealing that he is working in a language which he is
known to be developing. This will help ensure an impartial evaluation
of the problem submissions.
Looking forward to your suggestions,
Aaron
Hongwei Xi
I have a problem that I encountered when I was writing
my thesis in 1998. The following code is an implementation of
the KMP string search algorithm.
------
// An *untested* implementation in C
#include <stdlib.h>
#define MAXLEN 1024
int main()
{
unsigned int Fail[MAXLEN];
unsigned int M, K, R, i;
const char* P = "AAAABAABACA";
M = strlen(P);
K = 1;
Fail[K] = 0;
while (K <= M) {
R = Fail[K];
while ((R > 0) && (P[R-1] != P[K-1]))
R = Fail[R];
Fail[K+1] = R+1;
K++;
}
for (i = 1; i <= M+1; i++)
printf("Fail[%d] = %d\n", i, Fail[i]);
return 0;
}
------
The challenge here is to do in whatever language you like an
implementation of this algorithm and formally justify why your
implementation is terminating and cannot raise exceptions.
If you find it difficult to represent strings as arrays of
characters, you may represent them as lists of characters.
--Hongwei
Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215
Email: hw...@cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)