Algebraic properties of functions

Motivation

Most of the common mathematical functions have certain properties that are of interest. Examples are commutativity, associativity, idempotent, etc. Often if would be helpful to prvoe these properties for functions in code. Proving the prorty provides us with two things: one is that we have proven a something that we have expected from the function's behavior and the secon thing is that such a property could be used in reasoning about these function when there being used in other code.

Examples

Naturally, we can simply reason about the specification:
 
public class MaxClass {                                  
    // the max function is commutative (resp. its specification is)
    //@ invariant (\forall int a, b; max(a, b) == max(b, a));

    //@ ensures (\result == a || \result == b) & (\result >= a & \result >= b);
    int /* pure */ max(int a, int b)
    { ... code for max .... }
}

But could we reason about the code itself? The motivation behind this question is that it sometimes might be easier because a complicated(complex) specification is needed. For example consider a function that is supposed to sum two integer numbers represented as arrays of digits in decimal notation:
 
    //@ public normal_behavior
    //@ requires a != null && b != null;
    //@ requires a.length == b.length;
    byte[] myPlus(byte[] a, byte[] b)
    {
      int resLen = a.length;
       byte[] retv = new byte[resLen];
       int c = 0;
       int digit;
       
       for (int i = 0; i < resLen; i++)
       {
          digit = a[i] + b[i] + c;
          retv[i] = (byte)(digit % 10);
          c = c / 10;
       }

       return retv;
    }

It is quite obvious that the code treats the parameters in a symmetrical way. Nevertheless, to prove that such a function is commutative requires rather complex specification of the function (we have to model unbounded integers).

Questions

Is there a reasonable class of function for which we could show ceratin algebraic properties directly from the code (easily)? How to enhance reasoning techniques (e.g. weakest precondition calculus, predicate abstraction) for proving algebraic properties?
Access Counter : 2271 (started on Dec 13 2005)
Local Time: [an error occured while processing this directive]
[an error occured while processing this directive]