#------------------------------------------------------------------------------
#$Author: saulius $
#$Date: 2009-11-09 18:23:40 +0500 (Mon, 09 Nov 2009) $ 
#$Revision: 571 $
#$URL: svn+ssh://saulius-grazulis.lt/home/saulius/svn-repositories/paskaitos/VU/programavimo-metodologijos-pagrindai/skaidr%C4%97s/tests/2009.11.09/GCD-with-full-proof.pm $
#------------------------------------------------------------------------------
#*
#  Eucluds GCD (Greates Common Divisor) algorthim.
#**

package GCD;

use strict;
use warnings;
use Carp::Assert;

require Exporter;
@GCD::ISA = qw(Exporter);
@GCD::EXPORT = qw( gcd );

sub gcd($$)
{
    my ($x, $y) = @_;

    assert( $x > 0 );
    assert( $y > 0 );

    # assume: $X0 == initial $x
    # assume: $Y0 == initial $y
    # precondition: $x > 0
    # precondition: $y > 0

    while( $x != $y ) {
        # precondition: $x > 0
        # precondition: $y > 0
        # precondition: $x != $y
        if( $x > $y ) {
            # precondition: $x > $y
            # GCD( $x, $y ) == GCD( $X0, $Y0 );
            $x -= $y;
            # postcondition: $x > 0 (because $x > $y => $x - $y > 0)
            # GCD( $x, $y ) == GCD( $X0, $Y0 );
        } else {
            # precondition: $y > $x (because !$x > $y && $x != $y)
            # GCD( $x, $y ) == GCD( $X0, $Y0 );
            $y -= $x;
            # postcondition: $y > 0
            # GCD( $x, $y ) == GCD( $X0, $Y0 );
        }
        # postcondition: new $x < old $x || new $y < $old $y
        # postcondition: $x > 0 && $y > 0
        # GCD( new $x, new $y ) == GCD( old $x, old $y ) == GCD( $X0, $Y0 )
        # in other words:
        # invariant: GCD( $x, $y )
        # invariant: $x > 0 && $y > 0
    }
    # postcondition: $x == $y
    # postcondition: $x == GCD( $x, $x ) == GCD( $x, $y ) == GCD( $X0, $Y0 )
    # (because $x == $y && GCD( $x, $y ) == GCD( $X0, $Y0 ) =>
    #          $x == GCD( $x, $y ) =>
    #          $x == GCD( $X0, $Y0 )
    return $x;
}

1;