[jroesch]

In your second point you are referring to fact that is needed in a calling context when proving a large spec, that means it is a top level specification, and therefor trusted. You don't need to prove an implementation only touches the allocated array to verify it as a sorting algorithm, its because there is some other part of the top level specification that requires that.

For example I recently verified a JIT compiler, and the compiler spec was functional correctness but we really wanted to ensure it was correct AND only used the memory we allocated for it. In this case we had to grow the specification to be larger, its not longer just being correct, but isolated in some way. This of course has a trickle effect where we need intermediate facts, and proofs in order to be able to prove the top level theorem.

As some posters remarked above you should still be able to give a concise top level specification that is much smaller then the implementation. You really just want to say (where m is pre-sort, and m' is post-sort):

    (forall addr m m',
      addr < addr_of(array) \/ addr_of(array) + length < addr -> read addr m = read addr m')

We have a spec very similar to this in said JIT compiler, where we prove it doesn't write outside its input and output buffers. The top level spec is no more then a few definitions and a few lines of spec, compared to the JIT compiler which is 10,000s of lines of proof & implementation it is tiny and very easy to audit.

You can also make proofs obligations like this easier by using regions, a framing rule, or some programming model that gives some amount of memory isolation.

[xgk]

   calling context

In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling context.

   spec very similar to this

Yes, I was using something similar. Note that this is right only in a purely sequential setting ...

   I recently verified a JIT compiler,

That sounds exciting. That must have been a major piece of work. Anything published yet?

With JIT compilers the issue of self-modification becomes pertinent. I know that Magnus Myreen has verified a small JIT compiler a few years back but I don't remember exactly what theorem he proves. IIRC he was using a tailor-made Hoare logic for x86 code that basically moved some of the complexity of the spec into the logic.