wiki:Things To Do

Version 21 (modified by Stephen Siegel, 16 years ago) ( diff )

--

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:

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?

Note: See TracWiki for help on using the wiki.