// @(#)$Id: transfer.lh,v 1.12 1997/07/24 21:14:36 leavens Exp $

#include "BankAccount.lh"

extern void transfer(BankAccount& source, BankAccount& sink, Money amt)
            throw();
//@ behavior {
//@   let presrc:BankAccount be source^, presink:BankAccount be sink^,
//@      src:Obj[Money] be presrc.credit, snk:Obj[Money] be presink.credit;
//@   requires source ~= sink /\ assigned(source, pre) /\ assigned(sink, pre)
//@            /\ src^ >= amt /\ amt >= 0;
//@   modifies src, snk;
//@   ensures snk' = snk^ + amt /\ src' = src^ - amt;
//@ }

[Index]

HTML generated using lcpp2html.