4 ms·

A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belie

by xgk 9y ago

A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belief. Instead I conjecture that on average the full specification of an algorithm is at best proportional in length to the algorithm itself. There are two main issues: - Most verification does not tackle the full specification, but rather some aspect. - Verification needs many intermediate specifications (e.g. induction hypotheses in proofs), which need to be accounted for. I'm happy to be convinced otherwise. prove that a sorting algorithm is I produced the full verification of Quicksort (probably the first), and I needed to produce a large amount of intermediate specifications for auxiliary lemmas. The full specification was much longer than the algorithm.

wizeman 9y ago
You sound like you have more experience in this area than I do, so please correct me if I'm wrong. In the context of the original poster, the size of the specification that matters with respect to being a potential source of errors is the specification of the final (initial?) theorems that you want to prove, not the actual proof, nor the intermediate lemmas/theorems, induction hypothesis, etc. The latter ones can be all incorrect for all you care, but it doesn't matter because the theorem prover will always tell you that your implementation does not implement the specification unless the proof and the intermediate theorems are also correct. In the sorting example, what matters is that you correctly specify what is a sorted array and that the result of the sort() function should be a sorted array with the same elements as the input. If you decide to prove that your implementation of Quicksort implements that specification, you can use whatever implementation code you want and whatever intermediate lemmas or proofs you want, but again, if you make any mistake in implementing the algorithm or specifying the intermediate lemmas and proofs or even the final proofs, the theorem prover will complain loudly. If you simply mean that the total size of all the specification, including proofs and intermediate theorems and proofs can be as large or larger than the actual implementation, I agree with you, that can be the case and that is definitely a problem, because that is one of the reasons why most programmers and the industry in general won't find formal verification to be worth it. That said, SMT solvers (if you are so inclined) and proof automation in general can really help to reduce the size of the complete specification, including intermediate results and proofs (this is the main reason why I prefer Isabelle/HOL to Coq). (As an aside, I was pretty sure I knew of an example where a real-world system was verified with an SMT solver and where the complete specification and proofs ended up being around 10% of the code size of the implementation, but for the life of me I cannot find that example... perhaps I am misremembering). If by full verification you mean verifying all the way down to the machine code, I would argue that this kind of verification probably belongs in the compiler (e.g. CompCert or CakeML) rather than being something that the typical programmer should do. But perhaps, and most likely, I have not understood you completely :)
- xgk 9y ago
  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.
  - wizeman 9y ago
    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 http://rise4fun.com/Dafny/loJb
jojo3000 9y ago
But your "intermediate specifications" are not part of your specification! The specification says that the result is a sorted version of the input. It does not care about the induction hypothesis in your program. It might be technically necessary depending on the verification condition generator you are using. When you verify a functional program using Isabelle, Lean, or Coq your statement is that the output is a sorted version of the input.
- xgk 9y ago
  Yes. Mostly. But in practise, you need to specify what sortedness means, and in a generic sorting algorithm that means axiomatising the comparison predicate, including its side-effects. Note for example the C standard library implementation of Quicksort does take an arbitrary predicate, which may not be transitive, may have arbitrary side effects etc. The behaviour of sorting becomes pretty complicated in this scenario.
cgmg 9y ago
Verification ≠ specification.

by xgk 9y ago

wizeman 9y ago

You sound like you have more experience in this area than I do, so please correct me if I'm wrong. In the context of the original poster, the size of the specification that matters with respect to being a potential source of errors is the specification of the final (initial?) theorems that you want to prove, not the actual proof, nor the intermediate lemmas/theorems, induction hypothesis, etc. The latter ones can be all incorrect for all you care, but it doesn't matter because the theorem prover will always tell you that your implementation does not implement the specification unless the proof and the intermediate theorems are also correct. In the sorting example, what matters is that you correctly specify what is a sorted array and that the result of the sort() function should be a sorted array with the same elements as the input. If you decide to prove that your implementation of Quicksort implements that specification, you can use whatever implementation code you want and whatever intermediate lemmas or proofs you want, but again, if you make any mistake in implementing the algorithm or specifying the intermediate lemmas and proofs or even the final proofs, the theorem prover will complain loudly. If you simply mean that the total size of all the specification, including proofs and intermediate theorems and proofs can be as large or larger than the actual implementation, I agree with you, that can be the case and that is definitely a problem, because that is one of the reasons why most programmers and the industry in general won't find formal verification to be worth it. That said, SMT solvers (if you are so inclined) and proof automation in general can really help to reduce the size of the complete specification, including intermediate results and proofs (this is the main reason why I prefer Isabelle/HOL to Coq). (As an aside, I was pretty sure I knew of an example where a real-world system was verified with an SMT solver and where the complete specification and proofs ended up being around 10% of the code size of the implementation, but for the life of me I cannot find that example... perhaps I am misremembering). If by full verification you mean verifying all the way down to the machine code, I would argue that this kind of verification probably belongs in the compiler (e.g. CompCert or CakeML) rather than being something that the typical programmer should do. But perhaps, and most likely, I have not understood you completely :)

xgk 9y ago
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.
- wizeman 9y ago
  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 http://rise4fun.com/Dafny/loJb

jojo3000 9y ago

But your "intermediate specifications" are not part of your specification! The specification says that the result is a sorted version of the input. It does not care about the induction hypothesis in your program. It might be technically necessary depending on the verification condition generator you are using. When you verify a functional program using Isabelle, Lean, or Coq your statement is that the output is a sorted version of the input.

xgk 9y ago
Yes. Mostly. But in practise, you need to specify what sortedness means, and in a generic sorting algorithm that means axiomatising the comparison predicate, including its side-effects. Note for example the C standard library implementation of Quicksort does take an arbitrary predicate, which may not be transitive, may have arbitrary side effects etc. The behaviour of sorting becomes pretty complicated in this scenario.

cgmg 9y ago

Verification ≠ specification.