3 ms·

For someone only passingly familiar with Spec, what's the benefit of Spec over just using a property based testing framework like Haskell's QuickCheck (and I th

For someone only passingly familiar with Spec, what's the benefit of Spec over just using a property based testing framework like Haskell's QuickCheck (and I think Clojure's test.check)? I can encode all those invariants as QuickCheck properties and have them automatically tested against random inputs on every test run. It's still all runtime verification, but with random inputs I actually have more confidence of hitting a corner case than with just asserting during regular program runs or hand written example tests. Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1]. And while a machine checked proof of your sorting algorithm is nice, it might be hitting the diminishing returns point the article mentions over just using property tests. [1] https://github.com/davidfstr/idris-insertion-sort https://github.com/davidfstr/idris-insertion-sort

sheepmullet 9y ago
Think of QuickCheck/test.check but with better integration into the language. This makes it much more likely to be used but it's fundamentally the same set of ideas. A really cool idea I'm playing with at the moment is using fuzzing/static analysis based generators to feed spec/test.check. I think it will help get past the, imo, biggest issue with generators in that they can miss exceptional cases in the code. E.g. If (x=="jack and Jill) {exceptional case} is unlikely to be triggered with standard generators but "easy" for static analysis tools to solve. > Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1] In theory. In practice it is multiple orders of magnitude harder to prove properties in Idris than it is to spec them using property based testing.
yogthos 9y ago
To add to what sheepmullet said, I think the insertion sort example is exactly the problem with advanced type systems. It takes nearly 300 lines of code to provide the specification. Somebody has to be able to read that specification and understand that it's correct in a semantic sense. Ultimately, the specification itself becomes a full blown program that the type checker executes. So, now you run a program to try and verify aspects of your original program, but how do you verify that the specification itself is correct? At some point a human has to be able to read the code and decide that it matches the intent. This step can't be automated, and I certainly don't think the Idris example improves things. I'd argue that it's far easier to tell that this version is correct: fun insertionSort(arr, int n) { var i, key, j; for (i = 1; i < n; i++) { key = arr[i]; j = i-1; while (j >= 0 && arr[j] > key) { arr[j+1] = arr[j]; j = j-1; } arr[j+1] = key; } }

sheepmullet 9y ago

Think of QuickCheck/test.check but with better integration into the language. This makes it much more likely to be used but it's fundamentally the same set of ideas. A really cool idea I'm playing with at the moment is using fuzzing/static analysis based generators to feed spec/test.check. I think it will help get past the, imo, biggest issue with generators in that they can miss exceptional cases in the code. E.g. If (x=="jack and Jill) {exceptional case} is unlikely to be triggered with standard generators but "easy" for static analysis tools to solve. > Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1] In theory. In practice it is multiple orders of magnitude harder to prove properties in Idris than it is to spec them using property based testing.

yogthos 9y ago

To add to what sheepmullet said, I think the insertion sort example is exactly the problem with advanced type systems. It takes nearly 300 lines of code to provide the specification. Somebody has to be able to read that specification and understand that it's correct in a semantic sense. Ultimately, the specification itself becomes a full blown program that the type checker executes. So, now you run a program to try and verify aspects of your original program, but how do you verify that the specification itself is correct? At some point a human has to be able to read the code and decide that it matches the intent. This step can't be automated, and I certainly don't think the Idris example improves things. I'd argue that it's far easier to tell that this version is correct: fun insertionSort(arr, int n) { var i, key, j; for (i = 1; i < n; i++) { key = arr[i]; j = i-1; while (j >= 0 && arr[j] > key) { arr[j+1] = arr[j]; j = j-1; } arr[j+1] = key; } }