= Things To Do =


== Release 1.0 ==

Release 1.0 is scheduled for June 1, 2010.  This is the first public release of TASS.  Here is a list of features we expect in the release:

 * the MiniMP front-end we have been using
 * A C front-end, supporting at least a subset of C, with either pragmas or type qualifiers used to provide the meta-information needed by TASS.
 * XML representation of a model, including a model extractor which takes C source and produces a model in XML format, and the ability to read the XML file and construct a model from it
 * convenient binary packaging that bundles everything together and makes installation as easy as possible.   Versions for OS X, Windows, and linux (32- and 64-bit in each case).
 * relatively complete HTML documentation on the TASS web page: background, usage, MiniMP language reference, TASS Intermediate Representation (including XML)
 * bigger, more complex examples (e.g., laplace)
 * complete javadocs

== General To-Do Items ==

 * add good Javadocs for all public methods, classes, and packages
 * achieve much better statement and branch coverage in JUnit tests

== Symbolic Module ==

Is the assumption argument necessary?   Is it ever used for anything?  How about removing it?

Check out other automated theorem provers:

 * http://symbolaris.com/orbital/index.html
 * http://yices.csl.sri.com/



== Examples ==

== Parameters ==


== Library Functions ==

Special functions that are currently included in the grammar can instead be treated just like any other function and "linked in" at a later stage.   This will simplify the grammar and front-end. Functions that can be removed include {{{send}}}, {{{recv}}}, {{{allocate}}}, {{{deallocate}}}.

When {{{ModelIF.complete}}} is invoked, it will look for functions which are called but not defined.   It will then look through a standard library for a function of the correct name, and add that function to the process containing the call.

Note:  {{{allocate}}} takes a type argument, so we should also add to the grammar a new expression {{{sizeof(type)}}}.   The semantics module will associate a special symbolic constant to this expression, corresponding to the type (e.g., {{{SIZEOF_INT}}}).   We can then replace our {{{allocate}}} and {{{deallocate}}} with the standard C functions {{{malloc}}} and {{{free}}}


Some libraries add state: shared state and process global state.  How do manage this?