// @(#)$Id: withdraw.lh,v 1.10 1997/07/30 04:55:02 leavens Exp $
#include "BankAccount.lh"
extern void withdraw(BankAccount& a, Money amt) throw();
//@ behavior {
//@   requires assigned(a, pre) /\ amt >= 0;
//@   modifies a^.credit;
//@   ensures if a^.credit^ >= amt
//@           then a'.credit' = a^.credit - amt
//@           else unchanged(a^.credit);
//@ }

[Index]

HTML generated using lcpp2html.