// @(#)$Id: PlusAccount_pi.lh,v 1.1 1997/07/31 02:45:09 leavens Exp $

#include "PlusAccount.lh"

extern void PlusAccount::pay_interest(double rate) throw();
  //@ behavior {
  //@    requires 0.0 <= rate /\ rate <= 1.0;
  //@    modifies credit;
  //@    ensures credit' = rational(1.0 + rate) * credit^;
  //@    example rate = 0.05 /\ credit^ = money(400/1)
  //@                        /\ credit' = money(420/1);
  //@  also
  //@    requires 0.0 <= rate /\ rate <= 1.0;
  //@    modifies credit, checking;
  //@    ensures checking' = rational(1.0 + rate) * checking^; 
  //@    example checking^ = money(50000/100) /\ rate = 0.05
  //@         /\ checking' = money(52500/100);
  //@ }

[Index]

HTML generated using lcpp2html.