4 ms·

- Unit testing: Provide every test case possible Even if your program only takes a 32 bit integer as an input you'd have to provide 4294967296 test cases. Most

• gravypod 10y ago
  > Even if your program only takes a 32 bit integer as an input you'd have to provide 4294967296 test cases. Most programs' inputs are a bit larger than that. How do I go about defining a test using a formal method? Also, you know as well as I do that you don't need to test every input, only a representative subset if you use unit tests and use a fuzzing testing library. Using fuzzing, unit testing, pure functions and liberal preconditions through your project in development you'll likely come up with a product that has exactly what you are promising. Add a linter on top of that and for free you've got the safety of healthy paranoia. Do you have an example of a project that uses "formal methods" so I can see what they are? I'd also like to see something written that has a comprehensive security audit. Again, from what I'm seeing you're writing code to verify code and calling it "bug proof" just because you've written double the code. That's insanely misguided in my book.
  • pka 10y ago
    > Also, you know as well as I do that you don't need to test every input, only a representative subset if you use unit tests and use a fuzzing testing library. The thing is that you can never be sure that you chose a "representative subset". Unless you test every conceivable input you've verified that your program works for the subset you chose to test, nothing more. For example, how sure are you that your unit tests cover every conceivable edge case? > How do I go about defining a test using a formal method? You don't, it's a proof. You don't need tests. Some links from another comment [0]. I'd also point you to Idris [1] for a friendly dependently typed language if you are interested in learning more. [0] https://news.ycombinator.com/item?id=12544477 https://news.ycombinator.com/item?id=12544477 [1] http://www.idris-lang.org http://www.idris-lang.org
    • gravypod 10y ago
      > You don't, it's a proof. You don't need tests. Ok well what does it look like? Can you show me an example of this proof and how it is tested? You can't just say it's proven and remove the need for you to prove you've implemented it correctly. How is the proof validated and how is the source code checked against this? Also by the act of checking the source code you've essentially just created a test case. So we are back to my initial phrasing. What I'd like is for someone to show me how I go about proving something. Could you, if possible, walk through "proving" an implementation of a Fahrenheit and Celsius converter or something? What do you do? Where do you start? What does this look like? That's whats been driving me crazy about all of this "formal methods" thing. People say "it's proven" and when you say "how do you check your code or how do you verify what you did was correct" they say "we made a proof, it's proven". No information is exchanged other then the assertion of "what I did was right".
      • pka 10y ago
        Well, an F to C converter is not a terribly interesting case, because it would be trivial to implement. When you think about it, how would you test this in your favourite language of choice? By computing the expected value by using the same formula you used to compute the value you are testing in the first place. But here's another example that came up recently. Let's say you want to write a function that takes a string and returns its first character. Now, it would be an error to call this function with an empty string, because then what would it return? In a normal language, you'd probably check if the string was empty and then return null or something. When testing the function, you'd have to remember the empty string case and write an unit test for it (now I don't know about you, but I can't say I'd always remember to write a test case for this particular edge case; normally I'd forget). Can we do better? It turns out we can. We can encode invariants about our program on the type level. Types can be more than just strings, ints and chars. They can also be propositions, i.e. statements about our program. In this particular case we can construct a type NonEmptyString that can only be constructed by a function like this (using Haskell syntax): neString :: String -> Maybe NonEmptyString (This means that neString takes a String and returns a Maybe NonEmptyString). But what is this Maybe (also called Option, etc)? It's like a union type - it can either contain some value, or it must be empty. Now the cool thing about Maybe is that we can't just take out the potential value contained inside it - we have to pattern match on it! What this means is, that whenever you want to see what's inside a Maybe the compiler forces you to tell it what to do in both cases - when there's something inside and when there's nothing inside. Maybe you can see where this is going. This is how our takeFirstChar function would look like: takeFirstChar :: NonEmptyString -> Char Notice - we say that it only works on NonEmptyStrings! If we try to pass a regular string to it that would be a compiler error. But now we want to read something from the command line and returns it's first char. Let's say we have a read function: read :: String Every time you call this function it gives you a string read from the terminal. Ok, let's put our program together now: a = read print (takeFirstChar a) But wait! We can't do that - as I said above, the compiler complains, because we try to pass a String to a function that expects a NonEmptyString. Instead we have to: a = read case (neString a) Just st: print (takeFirstChar st) Nothing: print "String was empty" Notice how we pattern match on the result of (neString a). If the string was empty, we'd match the Nothing clause. In all other cases we'd print the first char. What we did is prove that the program will behave correctly in all cases - no tests needed! We can't put the program together in any other way, because it would be a type error. In a sense, the fact that the program exists is a proof of its type (programs have types too!) Now this is a pretty trivial invariant to encode on the type level, but in a dependently typed language you could encode whatever you'd like, i.e. for example that a list is sorted or that a number is the GCD of two other numbers, etc. This is often not trivial to do, and at some point you start seeing diminishing returns, because the time it takes to rigorously encode a proof is longer than any possible return of investment caused by proving that there are no bugs. But doesn't have to be an either-or situation. You can encode as much invariants as you'd want in your code. I think Haskell strikes a good balance in that regard, although Idris is a very interesting language too. (Sorry for typos, errors etc, didn't proofread).