========================================================================
 TO-DO List
========================================================================
12/23/2009 AS
Implement jml set comprehension (level 1 feature)

12/23/2009 AS
Implement jml import statements (level 1 feature)

09/01/2009 AS
Implement Jml-annotation statements with labels

08/28/2009 AS
Implement Jml-annotation statements

08/27/2009 AS
Implement Desugaring of method specification

07/12/2009 AS
Implement history constraints for old expressions (\old())

07/12/2009 AS
Implement history constraints for methods.

06/28/2009 AS
Numerical Quantified Expression (\num_of, \min, \max, \sum, \product)

05/14/2009 AS
Quantified Expression for inline assertions and class invariants

05/13/2009 AS
Quantified Expression: recursive definition (ie. i < i + 1 or  i < j)
Disable Warning for QE.
QE for Set-Based.

12/28/2008 YC
Implement history constraints.

12/12/2008 YC
Need to disable assertion checks while a class or an object is being
initialized.

12/06/2008 YC
Translation of local and anonymous classes.

12/02/2008 YC
Upon violation of an in-line assertion such as assert and assume,
evaluate the exception argument to compose an error message
(see a TODO in InlineAssertionVisitor).
		
11/22/2008 YC
AST merging. Nullify all JML specifications because they may interfere
with generated RAC code, as well as give unnecessary runtime overhead
(refer to AstMerger.nullifyJml). Perhaps, we can introduce a AST visitor
class to do this.

11/22/2008 YC
Non_null-ness. Check non_null-ness of fields, arguments, and the return
value as a part of invariant, and pre and postcondition checks, respectively.

11/13/2008 YC
Generalize the expression translation framework to accommodate expressions
such as quantifiers that may not be translated into a single Java expression
but to a sequence of statements. The current framework assume that each
Java/JML expression be translated into a single Java expression. 
Need to rewrite the ExpressionTranslator and all its subclasses.

11/12/2008 YC
Format the RAC code so that it becomes readable. This will be handy 
for debugging. As the first step, I added a flag RacPrettyPrinter.DEBUG
which, if true, prints RAC code to System.out; it may also be turned on
in JUnit test, I guess. Compare this output with that of JML2.

11/12/2008 YC
Review carefully all modifications done outside the RAC package, 
especially introduction of fields such as racCode to AST nodes, and 
eliminate them, e.g., by introducing RAC-specific AST nodes.


========================================================================
 KNOWN ERRORS AND UNIMPLEMENTED FEATURES
========================================================================

7/12/2009 AS
History constraints for methods are not supported. 
(eg //@ public constraint true for method();)

11/15/2008 YC
Distinction between static and non-static assertions; e.g., a
static invariant should be checked for both instance and static
methods, while a non-static (or instance) invariant should be
checked for only instance methods.

11/15/2008 YC
Native methods are not supported by the current RAC framework. A native
method is an abstract method. As its internal method will get
a different name in the current framework, it is not clear how it 
can be associated with an external, native method.

11/15/2008 YC
In-line assertions in (static) initialization blocks. It may be a 
straightforward extension to the current framework to support them. 


========================================================================
 DONE List
========================================================================
09/01/2009 AS
Implemented Jml-annotation statements except labels

08/28/2009 AS
Desugaring of method specification completed.

07/12/2009 AS
Support for helper methods/constructors implemented. 

07/12/2009 AS
History constraints implemented. 

06/28/2009 AS
Numerical Quantified Expression (\num_of, \min, \max, \sum, \product) implemented

06/21/2009 AS
QE for inline translation has been implemented.

05/14/2009 AS
QE for Set-Based has been implemented [preliminary].
Class Invariants for QE completed.

03/22/2009 AS
Assert and assume statement supported with user-defined message.

03/22/2009 AS
Static and instance invariants both supported.

03/17/2009 AS
Nullification of jml specifications after rac code generation.

03/17/2009 AS
Added in-line jml assertion statements (assert,assume,set) inside static/
non-static initialization blocks

12/02/2008 YC
Add ghost field getter/setter methods only if needed; currently
they are always added (see a FIXME in ClassDeclarationTranslator).

12/12/2008 YC
Review the translation of generic types (especially, type parameters) as they
may produce warnings during the second round compilation (refer to
RoundManager.java).

12/10/2008 YC
Review AST visitors w.r.t. update to the front end.

12/10/2008 YC
Clean the testing framework and tests; i.e., use compileAndRun and remove
other bogus methods.

12/12/2008 YC
Disable assertion check while evaluating assertions; it may cause an 
infinite loop.

12/12/2008 YC
Add a marker field to a class/interface to indicate that it was
RAC compiled; there're tools such as JML-JUnit that use this information.

12/10/2008 YC
Review the expression translator w.r.t. update to the front end.

12/10/2008 YC
Update the jar-generating ant file w.r.t. a new main class.

11/22/2008 YC
Come up with a clean way of getting and reporting source location
information upon an assertion violation. Refer to InvariantTranslator 
to start with.

12/02/2008 YC
Upon violation of an in-line assertion such as assert and assume,
give source code location and state information
(see a TODO in InlineAssertionVisitor).

11/20/2008 YC
Expressions in in-line assertions (assert, assume, and set) are
not translated; they are just verbatim copied to RAC code.

11/30/2008 YC
Completed translation of JML old expressions.

11/17/2008 YC
Nested set statements are not translated (see a test in KnownFailureTest).
Integrate the translation of set statement into the framework for
in-line assertions. I'll do it soon.

11/15/2008 YC
Unify translations of various in-line assertions into a single visitor class.
Perhaps, the mutation visitor should also be integrated into the translator;
otherwise, it may be error prone as the two have to work in a tight 
collaboration.

11/15/2008 YC
Consider method modifiers when translating method specifications, e.g.,
there should be no internal method for an abstract method. Special
care should be taken for abstract, native, visibility, and JML-specific
modifiers such as spec_public and spec_protected; see several test cases
in KnownFailureTest (more tests are needed, including those for
constructors).

11/14/2008 YC
Support in-line assertions such as assert and set statements for
constructor body.

11/12/2008 YC
Translate in-line assertions contained in a constructor body
(refer to the class ConstructorBodyTranslatorForClass).

11/13/2008 YC
Implement post-state assertion checks (such as invariant and postcondition)
for constructors; refer to ConstructorDeclaration.createConstructor.
