Things To Do

General

• change names of MiniMP to TASS throughout project
  • for example, in the URL for test data, in the name of the package edu.udel.cis.vsl.minimp, and so on. The name "MiniMP" should only be used for the language.
• add good Javadocs for all public methods, classes, and packages
• achieve much better statement and branch coverage in JUnit tests
• create separate test tree which mirrors the source tree but contains only JUnit tests

Symbolic Module

Consider re-designing the symbolic module based on lessons learned.

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

Then we can separate entirely the code for manipulating symbolic expressions from the code responsible for proving things and simplifying expressions based on an assumption.

How about multiple layers for the symbolic package:

1. Layer 0: Herbrand arithmetic. No simplifications of anything. This just produces new symbolic expressions based on the given arguments. Straightforward factory; operator, arguments type of thing.
2. Layer 1: Very basic simplifications only, such as x+0->x, 1*x->x, x+y->y+x. Integers commutative/associative, etc. All of which are applicable to IEEE arithmetic. Place boolean expressions in canonical form, such as CNF?
3. Layer 2: rational canonical form for real expressions. Valid for real arithmetic but does not necessarily preserve IEEE arithmetic.

Each layer could implement the same interface, SymbolicUniverseIF.

Add: a SymbolicSimplifierIF interface and a TheoremProverIF interface.

So, the following are the items exported by the symbolic module:

• SymbolicUniverseIF
  • methods for creating and manipulating symbolic expressions
  • SymbolicExpressionIF and all kinds of subtypes, operators, and so on
• SymbolicSimplifierIF
  • see the simplifier class currently in the value package
• TheoremProverIF
  • boolean valid(BooleanSymbolicExpressionIF assumption, BooleanSymbolicExpressionIF predicate);