public class Nat {
    public static void comm(int a, int b)
    /*: requires "True"
        ensures "a+b = b+a"
     */
    {
    }

    public static void assoc(int a, int b, int c)
    /*: requires "True"
        ensures "a+(b+c) = (a+b)+c"
     */
    {
    }

    public static void dist(int a, int b, int c)
    /*: requires "True"
        ensures "a*(b+c) = a*b+a*c"
     */
    {
    }

    public static int sum(final int n)
    /*:
      requires "n >= 0"
      ensures "result = n*(n+1) div 2"
     */
    {
        int s = 0;
        int i = 0;
        while
            /*: inv "(s+i) = i*(i+1) div 2" */
            (i != n+1)
        {
            s = s + i;
            i = i + 1;
        }
        return s;
    }
}