class AbPurse

instance variables
 
private balance : nat;
private lost : nat;

operations

-- Purse constructor: initialises the balance and lost variables.
public AbPurse : nat * nat ==> AbPurse
AbPurse(bal, lst) ==
( 
	balance := bal;
	lost := lst
);

-- Operation to return the value in the balance instance variable.
public GetBalance: () ==> nat
GetBalance() ==
( 
	return balance
);

-- Operation to return the value in the lost instance variable.
public GetLost: () ==> nat
GetLost() ==
(
	return lost
);

-- Operation to increase the balance variable by a given value.
public IncreaseBalance: nat ==> ()
IncreaseBalance(val) ==
(
	balance := balance + val
);

-- Operation to increase the lost variable by a given value.
public IncreaseLost: nat ==> ()
IncreaseLost(val) ==
(
	lost := lost + val
);

-- Operation to reduce the balance variable by a given value
--
-- Precondition : balance of purse is greater or equal to the given 
--			value, as required by Security Property 4: 
--			Sufficient Funds (pg. 12)
public ReduceBalance: nat ==> ()
ReduceBalance(val) ==
(
	balance := balance - val
)
pre balance >= val;

-- Operation to return the total money in the purse.
public GetTotal : () ==> nat
GetTotal() ==
(
	return balance + lost
);
end AbPurse