Things To Do

Release 1.0

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

• Implement library framework, including
  • MPI_Send, MPI_Recv, MPI_Comm_rank, MPI_Comm_size, MPI_Init, MPI_Finalize, MPI_Sendrecv, MPI_Bcast, MPI_Reduce, MPI_Allreduce, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_INT, MPI_DOUBLE, MPI_FLOAT, MPI_Comm, MPI_COMM_WORLD, ...
  • stdio: FILE, fopen, fclose, fprintf, fscanf, fread, fwrite, fseek
  • stdlib: malloc, free, NULL, abs, atoi, atof, atol, exit, rand, RAND_MAX
  • string: strlen, strcpy, memcpy, strcmp, strncmp
  • math: pow, sin, cos, tag, exp, fabs
• get rid of all compiler warnings
• improve error reporting

Tim's June 15 Goals

• fix FEVS repository
• fix integrator example
• get source/binary release process fixed
• add sizeof expression to model
• add evaluator support for record, array, and character literals

Steve's June 15 Goals

• add garbage collection
• fix cycle problem in dynamic type system

Ben's June 15 Goals

• ability to parse and generate TASS models from the FEVS examples using LLVM
  • ​http://vsl.cis.udel.edu/fevs

Other

• 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/

Library Functions

New library wiki page: Libraries