3 ms·

The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can. This is why I like end to end tests, UA

The spec may be provably perfect, but how to you prove the code perfectly conforms to the spec? I don't think you can. This is why I like end to end tests, UA testing, fuzzing, and property-based tests.

NovemberWhiskey 3y ago
>I don't think you can. Having done it, I'm pretty sure you can. Why don't you think it can be done? It requires a programming language (or language subset) with very well-defined semantics, and the use of theorem-proving tools but it's certainly possible.
- AnimalMuppet 3y ago
  You've done it? For how big a program? And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer overruns and use-after-free. Can you determine the absence of race conditions? Can you determine that it meets timing constraints with 100% certainty? There are a huge number of different kinds of things that a specification could specify. I'm pretty sure that we can't formally verify all of them.
  - NovemberWhiskey 3y ago
    Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.
jsenn 3y ago
Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1]. I doubt this is done much, but it is possible. [1] eg https://en.m.wikipedia.org/wiki/B-Method https://en.m.wikipedia.org/wiki/B-Method
dspillett 3y ago
> how to you prove the code perfectly conforms to the spec? I don't think you can That is actually the easy part. From my limited knowledge of formal verification (a university module decades ago and reading the occasional article since) it works very well for individual algorithms or small libraries, where the input ranges and desired outputs can be relatively easy to pin down with some accuracy and precision. As soon as you are working on something bigger and hairier, even under ideal circumstances the effort to produce the spec becomes exorbitant. And those ideal circumstances include end users (or other stake-holders) who know exactly what they want from the start or at least can be convinced to workshop it (at their cost) until they have bottomed out exactly what they want. More often than not, what happens instead is a PoC is produced, either as wireframes or a fuller prototype, and essentially that PoC and the issues raised against it becomes a partial spec, inconsistencies & holes included. Once you start down that track, getting back towards something formally verifiable is likely harder than starting towards that point in the first place. IMO formal verification, in an ideal world where you have effectively infinite time for doing things properly properly, or for smaller projects a large but not as infinite time, is the ideal. Unfortunately we don't usually work in an environment like that, so we have to compromise.
- NovemberWhiskey 3y ago
  The term "formal methods" covers a wide range of stuff, though. Basically we're just talking about mathematically rigorous approaches to code. The high-water-mark, which is stuff like formal proof of correctness or proof of worst-case runtime, gets a lot of attention; but there are plenty of valuable approaches that are less expensive. You can do, for example, formal proof of the absence of runtime exceptions (e.g. no bounds check violations), which doesn't require a formal specification and tends to result in a lot of theorems that are easy to prove automatically. Or you can do data and information flow analysis, which will let you verify that you don't depend on uninitialized values of variables or make sure that your expectations about how different inputs to a program should affect outputs ("hey, why doesn't the weapon release discrete depend on the weight-on-wheels sensor?")

NovemberWhiskey 3y ago

>I don't think you can. Having done it, I'm pretty sure you can. Why don't you think it can be done? It requires a programming language (or language subset) with very well-defined semantics, and the use of theorem-proving tools but it's certainly possible.

AnimalMuppet 3y ago
You've done it? For how big a program? And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer overruns and use-after-free. Can you determine the absence of race conditions? Can you determine that it meets timing constraints with 100% certainty? There are a huge number of different kinds of things that a specification could specify. I'm pretty sure that we can't formally verify all of them.
- NovemberWhiskey 3y ago
  Proof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.

jsenn 3y ago

Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1]. I doubt this is done much, but it is possible. [1] eg https://en.m.wikipedia.org/wiki/B-Method https://en.m.wikipedia.org/wiki/B-Method

dspillett 3y ago

> how to you prove the code perfectly conforms to the spec? I don't think you can That is actually the easy part. From my limited knowledge of formal verification (a university module decades ago and reading the occasional article since) it works very well for individual algorithms or small libraries, where the input ranges and desired outputs can be relatively easy to pin down with some accuracy and precision. As soon as you are working on something bigger and hairier, even under ideal circumstances the effort to produce the spec becomes exorbitant. And those ideal circumstances include end users (or other stake-holders) who know exactly what they want from the start or at least can be convinced to workshop it (at their cost) until they have bottomed out exactly what they want. More often than not, what happens instead is a PoC is produced, either as wireframes or a fuller prototype, and essentially that PoC and the issues raised against it becomes a partial spec, inconsistencies & holes included. Once you start down that track, getting back towards something formally verifiable is likely harder than starting towards that point in the first place. IMO formal verification, in an ideal world where you have effectively infinite time for doing things properly properly, or for smaller projects a large but not as infinite time, is the ideal. Unfortunately we don't usually work in an environment like that, so we have to compromise.

NovemberWhiskey 3y ago
The term "formal methods" covers a wide range of stuff, though. Basically we're just talking about mathematically rigorous approaches to code. The high-water-mark, which is stuff like formal proof of correctness or proof of worst-case runtime, gets a lot of attention; but there are plenty of valuable approaches that are less expensive. You can do, for example, formal proof of the absence of runtime exceptions (e.g. no bounds check violations), which doesn't require a formal specification and tends to result in a lot of theorems that are easy to prove automatically. Or you can do data and information flow analysis, which will let you verify that you don't depend on uninitialized values of variables or make sure that your expectations about how different inputs to a program should affect outputs ("hey, why doesn't the weapon release discrete depend on the weight-on-wheels sensor?")