[xgk]

   The latter ones can 
   be all incorrect for 
   all you care

Good point. Maybe we can call this the TSP (trusted specification base)?

In my experience the TSP is subtle and contains most of the intermediate definitions too. A few years back I had a very large Isabelle/HOL proof invalidated because of some small mistake in an obscure part of the specification that I never though could be important. It required a redesign from scratch of almost all of the proof.

   only have to specify "after 
   running the function sort() 
   on an array,

I'm afraid that's not enough in practise: you will also have to specify (and verify) things like: the implementation does not touch memory except the array to be sorted (and some auxiliary variables). If you don't, it will typically be difficult to use the proof of the sorting function in the context of the verification of a larger program.

   all the way down 
   to the machine code

No, that's an orthogonal dimension.

[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.

[wizeman]

  I'm afraid that's not enough in practise: you will also have to specify (and verify) things like: the implementation does not touch memory except the array to be sorted (and some auxiliary variables). If you don't, it will typically be difficult to use the proof of the sorting function in the context of the verification of a larger program.

Depending on the programming language being proved, you don't need to specify that the algorithm doesn't touch other memory, nor which variables it uses as temporary variables, because it's implicit in the definition of the language or the types themselves (or the fact that you are not referencing global variables).

See [1] for an example of a formally proved implementation of an array search algorithm (implemented in the Dafny language, in this case. You can press the play button to see if the theorem prover approves of this implementation).

As you can see, in Dafny there's no need to prove that no other memory is touched, as it's implicit in the type of the method. However, even this example is not as good as it could be because:

- Ideally, you wouldn't need to specify that function arguments aren't null. This would have been implicit had the implementation language (Dafny) not had the concept of null (like Rust doesn't, for instance).

- Also ideally, you would refactor the pre- and post-conditions into a separate predicate, like it was done for sorted(), so that you could prove any array search function to be correct using the same short specification (and if a bug is found in the specification, the fix would be applied to all implementations of array search functions automatically).

Regarding having a large Isabelle/HOL proof invalidated, that sounds very interesting and would love to read more about it! I can definitely admit I have never done any large proofs yet, so I am interested in hearing about your experience.

Ideally there should be some way of isolating parts of a large specification such that a bug in one part could not affect the other parts (similar to how functional languages guarantee that a function can never read anything but its input, and can never write to anything but its output), but I have absolutely no idea if this is even logically possible, as I am still just a beginner in this area.

Thanks for the interesting discussion!

[1] http://rise4fun.com/Dafny/loJb

[xgk]

   Depending on the programming 
   language being proved

That's true, GCed languages are simpler in this regard. But for low-level languages you have to do this 'by hand', and it can be complicated.

   not had the concept of null

That doesn't make the problem go away, you just have another case in the destructors (e.g. pattern matching) that you need to account for logically. Just kicking the can down the road.

   would love to read more 
   about it

Nothing published. Long story. I'll tell you in person, should we meet some day.