proving hypotheses (was Another silly question)
Chris Torek
chris at mimsy.UUCP
Wed May 24 13:01:34 AEST 1989
In article <2555 at bucsb.UUCP> castong at 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 at 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 at mimsy.umd.edu Path: uunet!mimsy!chris
More information about the Comp.lang.c
mailing list