chris@mimsy.UUCP (Chris Torek) (05/24/89)
In article <2555@bucsb.UUCP> castong@bucsb.UUCP (Paul Castonguay) writes: [small program deleted] >Output produced: > >*(a+i) = 4 *(i+a) = 4 > >Does that not show that *(a+i) == *(i+a) ? Although *(a+i) (where `a' is some pointer-valued expression and `i' is some integral expression, and neither contain side-effects that affect the other expression, and the sum produces a valid pointer, e.g., does not point beyond the end of an array) is equivalent in all instances to *(i+a) (for the same two expressions), the program in <2555@bucsb.UUCP> does not prove it---all it does is show that at least one instance appears to work. To prove some property P, it is necessary to show that P always holds, or, equivalently, that not-P never holds. In this case it is easy to go back to the language definition and find the statement that addition (including pointer addition) is commutative%. Then, knowing that *p designates a unique object whenever p is a valid value of type `pointer to T' for any type T, we can conclued that *(a+i) and *(i+a) designate the same unique object. ----- % Despite what I said earlier, addition of any `reasonable' values on most if not all machines is commutative. I was thinking of floating point and microcoded operations, in which a microcoded add routine might read something like # float add value1+value2 if EXPONENT(value1) == 0 then # common case return value2 fi ... compute exponent for result, do add, adjust exponent if required, then build and return result ... in which -0.0 + 0.0 gives 0.0, but 0.0 + -0.0 gives -0.0. -- In-Real-Life: Chris Torek, Univ of MD Comp Sci Dept (+1 301 454 7163) Domain: chris@mimsy.umd.edu Path: uunet!mimsy!chris