4 ms·
The next step for this would be to statically verify the annotations are being obeyed.
by MarkSweep 16y ago
The next step for this would be to statically verify the annotations are being obeyed.
- spicyj 16y agoThat sounds (close to) impossible. How would you tell if a given piece of code sorts a list properly? There are a million and one sorting algorithms and the static analyzer would have to be really smart to be able to check that reliably.
- atamyrat 16y agoYes, it is impossible. See: Halting problem.
- likpok 16y agoThe thing about program verification is that everyone knows that of course it is in general impossible. However, I am not writing a simulator. Most of the code I write does not actually take advantage of the power of a Turing machine. The fact that the general problem is impossible does not mean that the entire area of study is useless.
- riffraff 16y agosee: dependent typing http://en.wikipedia.org/wiki/Dependent_type http://en.wikipedia.org/wiki/Dependent_type and restricted languages such as Spark http://en.wikipedia.org/wiki/SPARK_(programming_language) http://en.wikipedia.org/wiki/SPARK_(programming_language)
- deleted 16y ago[deleted]
- likpok 16y agoI'm pretty sure that Pex [1] does the static analysis on these things. It's C#, but should be close enough for you to get the idea. [1]: You can play with it here: http://www.pexforfun.com/ http://www.pexforfun.com/