Skip to content


June 2, 2011

Today got the reference from on chex4j and wanted to try it out with Eclipse and here it goes. The code written here are from the article.

package com.jagan.chex4j;

import java.math.BigDecimal;

import net.sf.chex4j.Contract;
import net.sf.chex4j.Post;
import net.sf.chex4j.Pre;

public class SimpleAccount {

private BigDecimal balance;

@Post(“amount.doubleValue() >= 0.0d”)
public SimpleAccount(BigDecimal amount) {
this.balance = amount;

@Post(“$_.doubleValue() >= 0.0d”)
public BigDecimal getBalance() {
return this.balance;

@Pre(message = “Negative deposit.”)
// invokes deposit$Pre(amount)
@Post(message = “Balance exceeds 25k.”)
// invokes deposit$Post(amount)
public BigDecimal deposit(BigDecimal amount) {
this.balance = this.balance.add(amount);
return this.balance;

private boolean deposit$Pre(BigDecimal amount) {
return amount.doubleValue() >= 0.0d;

private boolean deposit$Post(BigDecimal amount) {
return this.balance.doubleValue() <= 25000;


package com.jagan.chex4j;

import java.math.BigDecimal;

public class SimpleAccountTest {

public static void main(String[] args) {
SimpleAccount saA = new SimpleAccount(new BigDecimal(100));
saA.deposit(new BigDecimal(50000));


I use Maven and hence add the following dependency to your pom.xml.


To run the code in Eclipse do the following (credits)

chex4j-Eclipse config

chex4j-Eclipse config

Already got a query on whether the post and pre conditions can be parametrized…..

No comments yet

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: