Trouble w/ r118 in Eclipse: cannot find Symbol class

[Marcel Bruch]

Hi there,

I'm setting up an simple Banking Account hierarchy with Contracts. I
followed FSteeg's tutorial on how to set up Eclipse for this.
Unfortunately I get this error on almost every save:

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:32:39.911
!MESSAGE error in contract: com.google.java.contract://
com.google.java.contract/dbc/CheckingAccount.java:2: cannot find
symbol
symbol : class Account
location: package dbc


Account is the abstract superclass of CheckingAccount. Any quick ideas
how to solve/get around this?


Thanks for help. It would be great if someone could find the time
today. I had planned to use cofoja as exercise in my course - it would
be great to show DbC with it.


The Account class looks as follows:

package dbc;

import com.google.java.contract.Ensures;
import com.google.java.contract.Requires;

/**
* Interface for bank accounts.
*
* @INVARIANT balance must always be higher than or equal to the
(negative)
* lineOfCredit.
*/
public abstract class Account {

/**
* Closes this account. After the account is closed not further
transfers
* are allowed!
*
* @REQUIRE balance must be 0 or higher - we do not close negative
accounts
* @ENSURE the account is closed (i.e., isOpen returns false)
*/
public abstract void close();

/**
* Computes the maximum available money to withdraw. This is the
* lineOfCredit + the current balance of an account.
*
* @ENSURE result = lineOfCredit + balance
*/
public abstract int getMaxWithdraw();

/**
* Returns the current balance of this account.
*
* @ENSURE balance cannot be less than line of credit (loc = 1000
then
* balance cannot be less than -1000)
*/
public abstract int getBalance();

/**
* Returns the line of credit for this account. Lines of credits
are
* specified using positive values.
*
* @ENSURE Line of credit must a positive value
*/
@Ensures("result > 0")
public abstract int getLineOfCredit();

/**
* Returns {@code true} if this account is active, {@code false}
otherwise.
*
* @see #open()
* @see #close()
*/
public abstract boolean isOpen();

/**
* Opens this account. This method does nothing if this account is
already
* open.
*
* @see #close() for additional constraints.
*
* @REQUIRE balance is higher than lineOfCredit
* @ENSURE the account is open after this call
*/
@Ensures({"isOpen()"})
@Requires({"getBalance() > getLineOfCredit()"})
public abstract void open();

/**
* Transfers some money into this account.
*
* @see #close() for additional constraints.
*
* @REQUIRE call this method only if the account is already open
* @REQUIRE charge must be positive
*/
@Requires({"isOpen()","charge > 0"})
public abstract void deposit(final int charge);

/**
* Sets the balance for this account directly. The account may be
open or
* not. To ensure consistency, the balance must be larger than the
current
* line of credit.
*
* @see #close() for additional constraints.
*
* @REQUIRE balance >= -lineOfCredit
*/
@Requires({"getBalance() > - getLineOfCredit()"})
public abstract void setBalance(final int balance);

/**
* Sets the line of credit for this account.
*
* @see #close() for additional constraints.
*
* @REQUIRE balance >= -lineOfCredit
* @ENSURE newValue must be positive
*/
@Requires({"getBalance() > - getLineOfCredit()"})
@Ensures({"newValue > 0"})
public abstract void setLineOfCredit(final int newValue);

/**
* Withdraws the given charge from this account.
*
* @see #close() for additional constraints.
*
* @REQUIRE charge must be positive;
* @REQUIRE charge must be smaller or equal to the maximum
available money.
*/
@Requires({"charge > 0"})
public abstract void withdraw(final int charge);
}

[David Morgan ☯]

Hi Marcel,

Thanks for trying Cofoja! Hopefully we can get to the bottom of this.

Nhat or Leo will undoubtedly have more ideas than me. For my part,
though, I wonder if we've actually accounted for pure abstract
classes. Could you try making it an interface, or adding a concrete
method, to see if that makes any difference?

Cheers

David

[David Morgan ☯]

[Marcel Bruch]

Hi David,

thanks for fast reply. Changing Account to an interface leads to slightly different errors:

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.231
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:2: cannot find symbol

symbol : class Account
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.231
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:41: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.232
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:45: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.232
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:49: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.232
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:53: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.232
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:57: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.233
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:61: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.233
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/CheckingAccount.java:65: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.233
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/SavingsAccount.java:18: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.233
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/JuniorCheckingAccount.java:14: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

!ENTRY org.eclipse.jdt.apt.pluggable.core 1 1 2011-05-17 14:59:23.234
!MESSAGE error in contract: com.google.java.contract://com.google.java.contract/dbc/JuniorCheckingAccount.java:18: cannot find symbol
symbol : class Account$com$google$java$contract$H
location: package dbc

Any further ideas? :)

Thanks.

[David Morgan ☯]

Hmm, then I guess we do deal with abstract classes, which is good, but
unhelpful here :)

Unfortunately I suspect it's a problem with your Eclipse setup, which
I don't know much about -- did you try building on the command line to
see if it works there?

Hopefully Leo can comment re: Eclipse.

Cheers

David

[Leonardo Chatain]

Hi Marcel,

  could you try compiling it without eclipse?

Doing:    javac -cp <cofoja.jar> your_classes

Or if you have an ant build.xml file, just add cofoja.jar to javac's classpath.

The problem is not on abstract classes (we do this fine, well... that's what we think :D).

I think this may be a problem with your eclipse configuration.

Cheers

--
Leo

[Leonardo Chatain]

--
Leo

[Leonardo Chatain]

The problem is on eclipse side. It works fine compiling with javac.

Are you sure you configured eclipse correctly?

Could you do some simple tests? If you instead of adding contracts to a superclass/interface, add them to a subclass (or to a class that does not have an explicit superclass), does it work? Does the real-time error detection work? What if you clean and rebuild your project?

Integration with eclipse is not perfect, but should work fine for this simple example.

Cheers

--
Leo

[Nhat Minh Le]

Hi Marcel,

As the others have pointed out, integration with Eclipse is not quite
good enough yet. The problem is probably due to the fact that Cofoja
can't find your sources because the source/class path is not set
properly. When compiling with javac, we auto-detect these things, but
we don't have support for the Eclipse environment yet (these things
are non-standard).

All in all that means you have to set up these options by yourself;
actually I think there's an error in Fabian's article. His explanation
of the values of the annotation processor's options is inaccurate, but
that's because I've just noticed the Wiki page has never been updated
with the newest information, so I've just done that. Please (re)read
the QuickReference page, section "Contract compilation (annotation
processor)".[1] And check that the following options are set
correctly:

- com.google.java.contract.classpath should be set to the class path
used by your project, not Cofoja's class path, but yours. This is
what you'd pass as the -cp option to javac if you compiled manually.

- com.google.java.contract.sourcepath should be set to the source path
where your source files reside. This is what you'd pass as
the -sourcepath option to javac if you compiled manually.

- com.google.java.contract.classoutput should be set to the directory
where you want to place .contracts and helper .class files generated
by Cofoja; usually, that'd be the same directory where you output
your classes. This is the equivalent of javac's -d option.

Could you try this?
And thanks for your interest!

[1] http://code.google.com/p/cofoja/wiki/QuickReference?ts=1305640819&updated=QuickReference#Contract_compilation_%28annotation_processor%29

--
Nhat

[Marcel Bruch]

Just in the case you wonder why I'm quiet... I'm still struggling but at least my JUnit Test Suite executed from within Eclipse produced some good results. I'll keep you updated...