TODO

-----
TODOs
-----

Jason
	Classes
	defines and typedefs (see Aaron's first email 1/23/08)
	Arrays DP long term work

	Bug: Lots of consecutive array updates kills vc generation, but old PiVC handles them just fine (see samples/array_updates.pi).
	Server on startup should ensure yices, included.pi, etc. are there and fail if not.
	Put filename into xml and ocaml data structures.
	Bug: Remove stupid a,b counterexample nodes (look for filename field in the location)
        Update README. Especially with information about email functionality.  Also talk about coloring/italicizing of things in VC pane and the inductive core.

Joel
	Let main server use multiple cores?

Unassigned
	i and l are not distinguishable in the VC pane (when bolded and red, I think) and l and 1 are not distinguishable in the code pane.  Also, the yellow text in the VC pane is almost impossible to read (see UnsortedUnion.pi).
	Should we support things like (l <= i <= u) as a convenience?
	Document the built-in predicates somewhere, probably the README.
	Add support for int e := ? syntax (see SortedUnion, UnsortedUnion).  Maybe it can mean this var can only be used in assertions?
	Make a webpage (or part of one) to get us ready for primetime.

--------------------
Possible later TODOs
--------------------
Provide better naming for _v nodes in counter-example.
Static analysis API
Better syntax highlighting?
Add support for warnings (:= vs =, postcondition that uses a parameter and not comparing it to rv (e.g. sorted(a, 0, |a|)))?  Asserts in Pi?
Running code/debugging.
Add an analysis that will propgate VCs?  Or maybe make it a heuristic?