class CreditCardCount ^=inherits CreditCard  
abstract
    var withdrawals: nat;

confined
    function withdrawals;

    schema !set_withdrawals(withdrawals_in:nat)
        post withdrawals! = withdrawals_in;



interface

    operator = (arg);

    build{!withdrawals:nat, balance_in:int, limit_in:nat}
        pre withdrawals = 0
        inherits CreditCard {balance_in, limit_in};
    redefine function INIT: bool
    ^= limit in set of nat {1000, 2000, 5000} &
       limit > balance &
       balance = 0 &
       withdrawals = 0;

    
    redefine function withdraw_prec (amount_in:nat) : bool
        ^= amount_in <= balance + limit &
           (exists withdrawals_temp:nat :- (withdrawals_temp = withdrawals + 1));
    redefine schema !withdraw (amount_in:nat)
        pre withdraw_prec(amount_in:nat)
        post change  withdrawals
             satisfy balance' = balance - amount_in &
                     withdrawals' = withdrawals + 1;
end;