> I need to implement inference rules for arrays in axiomatic semantics. Just a few random thoughts...
One model of an array is as a mapping from the set of indices to the set of values stored in an array. To use this idea in an axiomatic system means that your logic has to be of a higher order calculus than LPC, I guess. I feel that you may be able to avoid any complications for normally declared arrays like
But arrays on the heap will demand them. For example, the statement p=malloc(n) has a precondition that n>0 and a postcondition like this:
I'd hate to see axioms without functional variables that would let you derive the meaning of the following:
My suspicion is that you will be forced into assuming a function space not unlike that used in denotational semantics.