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

[Eric McCorkle]

Minor issue, but a possible better name occurred to me: Logic, Abstract
Syntax, and Enumeration Representation (laser)

On 07/22/14 13:51, Eric McCorkle wrote:
> 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).
>