// Two non-negative integers a and b are given. Compute a + b. 

// Only the following operations are allowed:

// - if, while, any comparisons

// - variable1 := variable2

// - variable := number

// - variable := variable + 1 (in C# you can write "variable++;")

using System;

using System.Diagnostics;

public class Program

{

    public static int InputInt(string prompt)

    {

        Console.Write("Enter " + prompt + ":");

        return Convert.ToInt32(Console.ReadLine());

    }

    public static void Main(string[] args)

    {

        int a = InputInt("integer a");

        int b = InputInt("integer b");

        Trace.Assert(a >= 0 && b >= 0);

​

        int i = 0;

        int r = a;

        // invariant: r = a + i and i <= b 

        while (i != b)

        {

            // r = a + i and i<b 

            i += 1;

            // r = a+i-1 and i<=b

            r += 1;

            // r = a+i and i<=b

        }

        // r=a+i and i=b hence r=a+b

        Console.Write("a+b=" + r);

    }

}