Darren New <dne### [at] sanrrcom> wrote:
> But honestly, I've never seen code where which element gets accessed 
> next is obvious to a programmer but not to the compiler. I've never seen 
> code where you could prove to a person's satisfaction that it was 
> correctly accessing the array but couldn't prove it in a formal way 
> given what's in the code itself, assuming you have all the code in front 
> of you, of course.

  Of course everything can be proven formally. The problem is how hard it
is to prove it. If you need to be a mathematician to formally prove that
certain values always keep within certain boundaries, that can be pretty
demanding for a programmer.

  One practical situation where it may be hard to prove you never access
out of boundaries is when you have a dynamic hash table, where the elements
at a certain position form a linked list, but all the elements are still
stored in the same dynamic array. Each element is a pair: The data, and an
index to the next element in the linked list. When you search for a value,
you calculate the hash index (which can already be hard to prove to be
inside the dynamically-sized has table), and check if the value is at that
position. If it isn't, you take from that position the index to the next
position and check that, etc.

  Assume that elements can be removed from the hash table, and that the
hash table array size can be reduced if enough elements are freed
appropriately. Naturally you would now have to prove that all the indices
left in the hash table point to valid indices in the now-smaller hash
table. In other words, it's not enough to prove that indices are valid
when you insert a new element in the hash table, you also have to prove
that the existing indices keep valid when the size of the hash table is
reduced.

  I would be pretty impressed by the programming language where you are
even able to express that.

  Intuitively proving this to a human could be much easier (although
it would probably not be a formal proof).

-- 
                                                          - Warp

Post a reply to this message