// @(#)$Id: transfer.h,v 1.8 1997/07/24 21:15:17 leavens Exp $

#ifndef transfer_h
#define transfer_h

#include "BankAccount.h"

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;
//@ }

#endif

[Index]

HTML generated using lcpp2html.