[Index] [Schedule] [Syllabi] [Text] [Labs] [Projects] [Resources] [Search] [Grading]

Thu Jan 22 13:30:24 PST 2004

- char buffer[20];
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: - either p=NULL
- or for some a:0..(n-1)->char( p points_at address(a) )
I'd hate to see axioms without functional variables that would let you derive the meaning of the following:

- typedef double real2real(double);
- real2real trig[]= { sin, cos, sin, cos };
(Assuming I got the syntax right).
My suspicion is that you will be forced into assuming a function space not unlike that used in denotational semantics.

> 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