Proposal for a code-tools project: spec description DSL and test case generation tool

[Eric McCorkle]

I would like to propose the creation of a repository in which I (and
possibly others) will work on a tool that provides a DSL for denoting
language and execution specifications.  This tool will also provide the
ability to generate code that enumerates test cases from a spec,
allowing for specification-driven testing.

The tentative title for the repository (and the language) is "lsl", a
shortening of "logical specification language"; however, I am open to
suggestions for a better name.

The repository will be open, and all code will be licensed under the
appropriate version of the GPL.


Details about the proposed LSL language and tools follow:

* The LSL language should allow users to write language specifications
in a syntax that can be parsed and operated on by tools.  The language
will be based on Gentzen-style inference rules, which are the
generally-accepted standard for writing language and type system
specifications in programming language literature.  Rules in this style
amount to logical "implies" statements, with a single conclusion and
possibly multiple premises.  Additionally, the language needs to allow
users to define abstract syntax structures, as well as maps, sequences,
sets, and other structures that are common in programming language
specifications.

* It should be possible to use LSL to formally describe important parts
of the JLS and JVMS, such as the grammar, the type system, the
selection/resolution logic for method invocation, and others.

* There will be a tool, tentatively named "lslproc", which will parse
specifications written using the DSL. The tool will have two builtin
backends, and will support a pluggable backend architecture, allowing
additional backends to be written in the future.

* The first backend will generate code that enumerates the
characteristic cases for a given spec. The primary use case for this is
testing problems where the following exist: 1) highly recursive
structure, 2) very difficult to determine expected results (ie. truth
tables lack large "blocks"), 3) very large sample spaces, with large
equivalence classes that are not easy to compute (related to (2)).  The
specnote tool will act similarly to a lex/yacc style tool, generating
test case enumeration code, which is then combined with a test harness
to create an enumeration test.

* The second backend will generate documentation in several formats
(docbook, LaTeX, etc) that renders as an abstract syntax definition, and
a set of inference rules in the standard Gentzen-style notation.

* The repository will also contain a library that will be used to
support the code generated by the first backend.  This library will
provide a framework for implementing enumeration procedures.  Should
components of this library prove to be generally useful, they may be
considered for addition to the core libraries.


General notes:

* The details of the spec DSL beyond the simple statement of its goals
are at this point undetermined.  The design of the DSL should consider
similar languages and tools already in existence.

* The DSL and tools should be sufficiently powerful to denote a
specification for a real programming language (ie. Java); however, they
should avoid additional complexity beyond that.

* The DSL and tools should be "industrial-grade" software.  They should
be usable, robust, and provide features suitable for production use (ie.
beyond a few toy examples).