3 ms·

>and have it only be valid if you or the computer can prove that it meets that specification (and have the specification be complete and correct of course Hasn

by krisgee 10y ago

>and have it only be valid if you or the computer can prove that it meets that specification (and have the specification be complete and correct of course Hasn't this just moved all the issues with writing code over to writing the specifications?

RGamma 10y ago
Somewhat, yes. A specification framework is there to help bridge the semantic gap between what you are trying to achieve in the real world and the world of bit-banging if you will. And even if you forget a part of a specification (like saying a sorting function needs to leave behind a sorted collection but forgetting to mention that the input and output collection need to contain the exact same elements or that the input collection needs to be finite for the function to terminate), you'll still have a notion of "incremental correctness". That's why I added in the part with what specifying "cryptographic strength" would mean (e.g.: strong against what exactly?). You could leave that or time-critical properties (e.g.: this function encrypts x bits in y seconds) out and retain the notion of "functional correctness" (i.e. the ciphertext always corresponds to what the definition says it should be). When you're writing code you'll (most of the time :)) have an idea of what you're trying to achieve. Formal specification should enable you to write that down in convenient form.
corysama 10y ago
Right now the way most people code is: Is this spec actually correct and complete? Shrug... Does this JavaScript actually implement the spec exactly? LoL! At least being told what to fix in your code so that it actually implements your spec is a big step up over "staring at your code really hard." Good formal systems make it easy to find inconsistencies and incompleteness in your specs. Very good formal systems should make it easy to test and verify your spec against your intent.
mannykannot 10y ago
>Hasn't this just moved all the issues with writing code over to writing the specifications? Not all the issues, or at least not to the same extent, and it is not like they were not there before: an incomplete or missing specification does not default to being considered correct. Perhaps the best we can hope for from more rigorous analysis is to catch more of the cases where we are being inconsistent, making unwarranted assumptions or even being contradictory. These are not just between requirements and implementation but also within the requirements. This may not look like much of a promise, but the silver bullets have not worked.

by krisgee 10y ago

RGamma 10y ago

Somewhat, yes. A specification framework is there to help bridge the semantic gap between what you are trying to achieve in the real world and the world of bit-banging if you will. And even if you forget a part of a specification (like saying a sorting function needs to leave behind a sorted collection but forgetting to mention that the input and output collection need to contain the exact same elements or that the input collection needs to be finite for the function to terminate), you'll still have a notion of "incremental correctness". That's why I added in the part with what specifying "cryptographic strength" would mean (e.g.: strong against what exactly?). You could leave that or time-critical properties (e.g.: this function encrypts x bits in y seconds) out and retain the notion of "functional correctness" (i.e. the ciphertext always corresponds to what the definition says it should be). When you're writing code you'll (most of the time :)) have an idea of what you're trying to achieve. Formal specification should enable you to write that down in convenient form.

corysama 10y ago

Right now the way most people code is: Is this spec actually correct and complete? Shrug... Does this JavaScript actually implement the spec exactly? LoL! At least being told what to fix in your code so that it actually implements your spec is a big step up over "staring at your code really hard." Good formal systems make it easy to find inconsistencies and incompleteness in your specs. Very good formal systems should make it easy to test and verify your spec against your intent.

mannykannot 10y ago

>Hasn't this just moved all the issues with writing code over to writing the specifications? Not all the issues, or at least not to the same extent, and it is not like they were not there before: an incomplete or missing specification does not default to being considered correct. Perhaps the best we can hope for from more rigorous analysis is to catch more of the cases where we are being inconsistent, making unwarranted assumptions or even being contradictory. These are not just between requirements and implementation but also within the requirements. This may not look like much of a promise, but the silver bullets have not worked.