// @(#)$Id: transfer2.lh,v 1.12 1997/07/24 21:14:49 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;
//@ }

[Index]

HTML generated using lcpp2html.