//  /*--------------------------------------------------------*\
//  |   Main Program: Euclid's algorithm for GCD
//  |*--------------------------------------------------------*|
//  |   Date:         13 August 1996
//  |   Author:       Bruce W. Weide
//  |   
//  |   Brief User's Manual:
//  |   Asks for two integers, and if both are non-negative
//  |   and one is positive, reports the GCD of the two, and
//  |   then quits.
//  |   
//  \*--------------------------------------------------------*/

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

#include "RESOLVE_Foundation.h"

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

/*!
    math definition DIVIDES (
            d: integer,
            n: integer
        ): boolean is
        there exists k: integer (n = k * d)

    math definition IS_GCD (
            gcd: integer,
            m: integer,
            n: integer
	): boolean is
	(m /= 0  or  n /= 0) and
	DIVIDES (gcd, m)  and
	DIVIDES (gcd, n)  and  
	for all k: integer where
		(DIVIDES (k, m)  and
		 DIVIDES (k, n))
		       (k <= gcd)) 
!*/

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

global_function Integer Greatest_Common_Divisor (
        preserves Integer j,
        preserves Integer k
    );
/*!
    requires
	0 <= j <= k  and
	0 < k
    ensures
	IS_GCD (Greatest_Common_Divisor, j, k)
!*/
    
//--------------------------------------------------------------

global_function_body Integer Greatest_Common_Divisor (
        preserves Integer j,
        preserves Integer k
    )
{
    if (j == 0)
    {
        return k;
    }
    else
    {
        return Greatest_Common_Divisor (k mod j,  j);
    }
}

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

program_body main ()
{
    object Character_IStream input;
    object Character_OStream output;
    object Integer small, large;

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

    // Get two integers from user; put them in proper order
    
    output << "Please input an integer: ";
    input >> small;
    output << "Please input another integer: ";
    input >> large;
    if (small > large)
    {
        small &= large;
    }

    // Compute GCD of small and large
    
    if ((small < 0) or (large <= 0))  // Can't find GCD
    {
        output << "\nSorry, both integers must be non-negative, "
	       << "and one must be positive";
    }
    else  // Compute and report GCD
    {
        object Integer gcd;

        gcd = Greatest_Common_Divisor (small, large);
        output << "\nGCD = " << gcd << "\n";
    }

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