// @(#)$Id: PlusAccount.jml,v 1.7 2007/07/01 14:39:10 chalin Exp $

// Copyright (C) 1998, 1999 Iowa State University

// This file is part of JML

// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.

// JML is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.

// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING.  If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.


package org.jmlspecs.samples.prelimdesign;

public class PlusAccount extends Account {
  //@ public model MoneyOps savings, checking;  in credit;

  /*@ public represents credit \such_that
    @                   credit.equals(savings.plus(checking));
    @*/
  //@ public invariant savings != null && checking != null;
  /*@ public invariant_redundantly
    @           savings.plus(checking)
    @                  .greaterThanOrEqualTo(new USMoney(0));
    @*/

  /*@  public normal_behavior
    @    requires sav != null && chk != null && own != null
    @          && (new USMoney(1)).lessThanOrEqualTo(sav)
    @          && (new USMoney(1)).lessThanOrEqualTo(chk);
    @    assignable credit, owner;
    @    assignable_redundantly savings, checking;
    @    ensures savings.equals(sav) && checking.equals(chk)
    @             && owner.equals(own);
    @    ensures_redundantly credit.equals(sav.plus(chk));
    @*/
  public PlusAccount(MoneyOps sav, MoneyOps chk, String own);


  /*@ also
    @  public normal_behavior
    @    old boolean can_scale = credit.can_scaleBy(1.0 + rate);
    @    requires 0.0 <= rate && rate <= 1.0
    @          && can_scale;
    @    assignable credit, savings, checking;
    @    ensures checking.equals(
    @             \old(checking).scaleBy(1.0 + rate));
    @ for_example
    @  public normal_example
    @    requires rate == 0.05
    @          && checking.equals(new USMoney(2000));
    @    assignable credit, savings, checking;
    @    ensures checking.equals(new USMoney(2100));
    @*/
  public void payInterest(double rate);

  /*@ also
    @  public normal_behavior
    @    requires amt != null
    @            && (new USMoney(0)).lessThanOrEqualTo(amt)
    @            && amt.lessThanOrEqualTo(savings);
    @    assignable credit, savings;
    @    ensures savings.equals(\old(savings).minus(amt))
    @            && \not_modified(checking);
    @ also
    @  public normal_behavior
    @    requires amt != null
    @            && (new USMoney(0)).lessThanOrEqualTo(amt)
    @            && amt.lessThanOrEqualTo(credit)
    @            && amt.greaterThan(savings);
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(0))
    @           && checking.equals(
    @                \old(checking).minus(amt.minus(savings)));
    @ for_example
    @   public normal_example
    @    requires savings.equals(new USMoney(40001))
    @             && amt.equals(new USMoney(40000));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(1))
    @            && \not_modified(checking);
    @  also
    @   public normal_example
    @    requires savings.equals(new USMoney(30001))
    @           && checking.equals(new USMoney(10000))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(0))
    @           && checking.equals(new USMoney(1));
    @*/
  public void withdraw(MoneyOps amt);

  /*@ also
    @  public normal_behavior
    @    old boolean can_add = credit.can_add(amt);
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && can_add;
    @    assignable credit, savings;
    @    ensures savings.equals(\old(savings).plus(amt))
    @            && \not_modified(checking);
    @ for_example
    @  public normal_example
    @    requires savings.equals(new USMoney(20000))
    @           && amt.equals(new USMoney(1));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(20001));
    @*/ 
  public void deposit(MoneyOps amt);

  /*@    public normal_behavior
    @    old boolean can_add = credit.can_add(amt);
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && can_add;
    @    assignable credit, checking;
    @    ensures checking.equals(\old(checking).plus(amt))
    @          && \not_modified(savings);
    @ for_example
    @  public normal_example
    @    requires checking.equals(new USMoney(20000))
    @           && amt.equals(new USMoney(1));
    @    assignable credit, checking;
    @    ensures checking.equals(new USMoney(20001));
    @*/
  public void depositToChecking(MoneyOps amt);

  /*@  public normal_behavior
    @    requires amt != null;
    @    {|
    @      requires (new USMoney(0)).lessThanOrEqualTo(amt)
    @             && amt.lessThanOrEqualTo(checking);
    @      assignable credit, checking;
    @      ensures checking.equals(\old(checking).minus(amt))
    @             && \not_modified(savings);
    @     also
    @      requires (new USMoney(0)).lessThanOrEqualTo(amt)
    @             && amt.lessThanOrEqualTo(credit)
    @             && amt.greaterThan(checking);
    @      assignable credit, checking, savings;
    @      ensures checking.equals(new USMoney(0))
    @          && savings.equals(
    @              \old(savings).minus(amt.minus(checking)));
    @    |}
    @ for_example
    @  public normal_example 
    @    requires checking.equals(new USMoney(40001))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, checking;
    @    ensures checking.equals(new USMoney(1))
    @           && \not_modified(savings);
    @ also
    @  public normal_example
    @    requires savings.equals(new USMoney(30001))
    @           && checking.equals(new USMoney(10000))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, checking, savings;
    @    ensures checking.equals(new USMoney(0))
    @          && savings.equals(new USMoney(1));
    @*/
  public void payCheck(MoneyOps amt);
}