/*	Loop Invariants: code for a computing carol

        J.P. Dougherty		Fall 2003
*/

// standard IO and string
#include <iostream>
#include <string>

using std::cout;
using std::endl;
using std::string;

// global constant
const int N = 2;

// returns true if the integer is odd
bool odd(int i)
{
    return i % 2 == 1;
}

// returns a chorus of the lyrics
string Chorus(int c)
{
    // function precondition: c >= 0
    string chorus = "";
    // loop precondition: c >= 0 and chorus is empty
    for (int i = 0; i < N; i++)
    {
        // invariant:
        //
        //	Holiday surprise ;-)
        //
        chorus += "Loop invariants, loop invariants\n";
        if (odd(i) && !odd(c))
            chorus += "As I write my code.\n\n";
        else if (!odd(i) && !odd(c))
            chorus += "Keep me on the road,\n";
        if (!odd(i) && odd(c))
            chorus += "They can be a pain.\n";
        else if (odd(i) && odd(c))
            chorus += "Oh, but what I gain.\n\n";
    }
    // loop postcondition:
    //
    //	Holiday surprise ;-)
    //
    
    // function postcondtition:
    //  chorus holds the text of chorus c
    return chorus;
}

// returns a verse of the lyrics
string Verse(int v)
{
    // function precondition: true
    string verse = "";
    if (odd(v))
    {	verse += "Executing, substituting,\n";
        verse += "Each does complement.\n";
        verse += "Code correctness is the goal\n";
        verse += "Of loop invariants.\n\n";
    }
    else
    {	verse += "Preconditions, postconditions,\n";
        verse += "Help to shed some light.\n";
        verse += "Assertions used to write the loop\n";
        verse += "Will help me get it right.\n\n";
    }
    // function postcondition:
    //  verse has the lyrics of verse(v)
    return verse;
}

// returns the lyrics of the song
string AllLyrics()
{
    // function precondition: true
    string lyrics = "";
    int i;
    
    // loop precondition: lyrics is empty
    for (i = 0; i < N; i++)
    {
        // invariant:
        //  lyrics == SUM(j=0,i-1,Chorus(j) + Verse(j))
        lyrics = lyrics + Chorus(i) + Verse(i);
    }

    // loop postcondition:
    //  lyrics == SUM(j=0,N-1,Chorus(j) + Verse(j))
    //		&& i >= N
    
    // function postcondition: lyrics is complete and full
    return lyrics;
}

// driver functions
int main()
{
    cout << endl << "Loop Invariants" << endl << endl;
    cout << "J.P. Dougherty c2003" << endl << endl;
    cout << AllLyrics() << endl;
    return 0;
}