#17 ✓resolved
me (at andresteingress)

old variable generation on inherited instance variables

Reported by me (at andresteingress) | April 11th, 2011 @ 08:57 PM | in 1.2.4

it seems that the old variable generation does not work on inherited instance variables:

import org.gcontracts.annotations.*

// by http://www.javacoffeebreak.com
class Account 
{
    protected BigDecimal balance

    def Account( BigDecimal amount = 0.0 )
    {
        balance = amount
    }

    void deposit( BigDecimal amount )
    {
        balance += amount
    }

    @Requires({ amount >= 0.0 })
    // @Ensures({ balance == old.balance - amount })
    BigDecimal withdraw( BigDecimal amount )
    {
        if (balance < amount) return 0.0
        
        balance -= amount
        return amount
    }

    BigDecimal getBalance()
    {
        return balance
    }
}  

class BetterAccount extends Account {
    
    @Ensures({ balance == old.balance - (amount * 0.5) })
    BigDecimal withdraw( BigDecimal amount )
    {
        if (balance < amount) return 0.0
        
        balance -= amount * 0.5
        return amount
    }
}

Account account = new BetterAccount()
account.deposit(30)
account.withdraw(10) // could be a program bug

account.balance       // uniform access principle: uniform access to computed or in-memory vals

Comments and changes to this ticket

Please Sign in or create a free account to add a new ticket.

With your very own profile, you can contribute to projects, track your activity, watch tickets, receive and update tickets through your email and much more.

New-ticket Create new ticket

Create your profile

Help contribute to this project by taking a few moments to create your personal profile. Create your profile »

core module

Shared Ticket Bins

People watching this ticket

Referenced by

Pages