//  /*--------------------------------------------------------*\
//  |   Main Program: Determine when you will become a
//  |       millionaire
//  |*--------------------------------------------------------*|
//  |   Date:         13 August 1996
//  |   Author:       Bruce W. Weide
//  |   
//  |   Brief User's Manual:
//  |   Asks for your initial investment and annual interest
//  |   rate, then reports how many years it takes you to
//  |   become a millionaire with that investment, and then
//  |   quits.
//  |   
//  \*--------------------------------------------------------*/

///-------------------------------------------------------------
/// Global Context ---------------------------------------------
///-------------------------------------------------------------

#include "RESOLVE_Foundation.h"

///-------------------------------------------------------------
/// Interface --------------------------------------------------
///-------------------------------------------------------------

global_function Integer Years_To_Millionaire (
        preserves Real base,
        preserves Real rate
    );
/*!
    requires
	0 < base < 1000000  and
	rate > 0
    ensures
	base * (1 + rate)^(Years_To_Millionaire - 1) <
	    1000000 <=
		base * (1 + rate)^(Years_To_Millionaire) 
!*/
    
//--------------------------------------------------------------

global_function_body Integer Years_To_Millionaire (
        preserves Real base,
        preserves Real rate
    )
{
    object Real total;
    object Integer years;

    total = base;
    while (total < 1000000.0)
    /*!
	preserves rate
	alters total, years
	requires
	    0 < total < 1000000  and
	    rate > 0  and
	    years = 0
	ensures
	    total = #total * (1 + rate)^(years)  and
	    total / (1 + rate) < 1000000 <= total
    !*/
    {
        total *= (1.0 + rate);
        years++;
    }
    return years;
}

//--------------------------------------------------------------

program_body main ()
{
    object Character_IStream input;
    object Character_OStream output;
    object Real initial_investment, annual_rate;

    // Open input and output streams
    
    input.Open_External ("");
    output.Open_External ("");

    // Get information from user
    
    output << "Initial investment: ";
    input >> initial_investment;
    output << "Annual interest rate (%): ";
    input >> annual_rate;

    // Compute number of years to make a million
    
    if (initial_investment <= 0.0)
    {
        output << "\nSorry, you'll never become a millionaire\n"
             << "by investing a non-positive amount.\n";
    }
    else if (initial_investment >= 1000000.0)
    {
        output << "\nYou're already a millionaire.\n";
    }
    else if (annual_rate <= 0.0)
    {
        output << "\nSorry, you'll never become a millionaire\n"
             << "by investing at a non-positive rate.\n";
    }
    else
    {
        object Integer years;

        years = Years_To_Millionaire (initial_investment,
				      annual_rate / 100.0);
        output << "\nYou'll be a millionaire in " << years
             << " years.\n";
    }

    // Close input and output streams
    
    input.Close_External ();
    output.Close_External ();
}