Tracker: Bugs
when i compile my Purse.java with jmlc , i get this long
list of errors that starts with
java.lang.RuntimeException: fail reached
at org.multijava.util.Utils.fail(Utils.java:100)
.......................
and it ends with this line:
at org.jmlspec.jmlrac.Main.main(Main.java:74)
Here is my Purse.java :
public class Purse {
int balance;
//@ public invariant balance >= 0;
/*@ ensures balance == 0;
@*/
public Purse() {
balance = 0;
}
/*@ requires s >= 0;
@ ensures balance == \old(balance) + s;
@*/
public void credit(int s) {
balance = balance + s;
}
/*@ public normal_behavior
@ requires s >= 0 && s <= balance;
@ assignable balance;
@ ensures balance == \old(balance) - s;
@*/
public void withdraw(int s) {
balance = balance - s;
}
}
the jmldoc command works..
i am using j2sdk1.4.2_08
thks
Nobody/Anonymous
jmlrac (i.e., the jmlc tool)
user reported
Public
Comments ( 7 )
|
Date: 2006-05-25 22:21 Logged In: YES |
|
Date: 2006-05-25 22:21 Logged In: YES |
|
Date: 2005-09-12 15:13 Logged In: YES |
|
Date: 2005-09-12 15:13 Logged In: YES |
|
Date: 2005-09-12 13:22 Logged In: YES |
|
Date: 2005-09-12 13:17 Logged In: YES |
|
Date: 2005-09-12 12:30 Logged In: YES |
Attached File
No Files Currently Attached
Changes ( 12 )
| Field | Old Value | Date | By |
|---|---|---|---|
| close_date | - | 2006-05-25 22:21 | leavens |
| resolution_id | None | 2006-05-25 22:21 | leavens |
| status_id | Open | 2006-05-25 22:21 | leavens |
| priority | 5 | 2006-05-19 04:32 | leavens |
| category_id | None | 2005-10-04 13:39 | leavens |
| artifact_group_id | None | 2005-10-04 13:39 | leavens |
| assigned_to | tongjie | 2005-10-04 13:38 | leavens |
| category_id | Installation problem | 2005-10-04 13:38 | leavens |
| data_type | 510629 | 2005-10-04 13:38 | leavens |
| summary | error with jmlc | 2005-10-04 13:38 | leavens |
| assigned_to | leavens | 2005-09-12 15:13 | leavens |
| category_id | Tool not parsing my input | 2005-09-12 12:30 | leavens |
