// @(#)$Id: transfer3.lh,v 1.10 1997/07/24 21:14:07 leavens Exp $

#include "BankAccount.lh"

extern void transfer(BankAccount& source, BankAccount& sink, Money amt)
            throw();
//@ behavior {
//@  requires source ~= sink /\ assigned(sink, pre) /\ assigned(source, pre)
//@           /\ source^.credit^ >= amt /\ amt >= 0;
//@  modifies source^.credit, sink^.credit;
//@  ensures sink'.credit' = sink^.credit^ + amt
//@     /\ source'.credit' = souce^.credit^ - amt;
//@   example amt = money(100/1)
//@         /\ source^.credit^ = money(500/1) /\ sink^.credit^ = money(200/1)
//@         /\ source'.credit' = money(400/1) /\ sink'.credit' = money(300/1);
//@ }

[Index]

HTML generated using lcpp2html.