3 ms·

> This is incredibly valuable because a good testsuite lets you check your specification. Could the test suite actually serve as the specification?

• chriswarbo 5y ago
  Tests are specifications, but they can only encode "there exists" statements. For example, consider a test like this: def canUpdateUsername(): u = User("u1", "user@example.com") n = "u2" assert u.setUsername(n).getUsername() == n As a specification, this states that there exists a user 'u' and a username 'n', such that u.setUsername(n).getUsername() equals n. We prove that statement by providing explicit examples of 'u' (the value User("u1", "user@example.com")) and 'n' (the value "u2"), and the computer checks the proof by executing the code. That execution is equivalent to substituting-in/inlining definitions, and rewriting primitives like 'if (True): x', until we get the value 'True'. QED. Usually what we actually want is a "for all" statement. Sometimes tests can achieve this by being exhaustive, e.g. checking every boolean, or all 256 bytes. More generally, a "for all" statement is a function, e.g. def canUpdateUsernames(u: User, n: str): assert u.setUsername(n).getUsername() == n This is a better specification, since we're asserting the relationship between 'setUsername' and 'getUsername' for any/every User and string. Unfortunately, we can't prove this by substituting-in/inlining definitions, since we don't have definitions for 'u' and 'n'. One way to prove it is to use a more general approach, e.g. using equational rewriting, induction, etc. That's the approach taken by (interactive) theorem provers, but it can be a lot of work. Systems I've used for this include https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what... https://coq.inria.fr https://coq.inria.fr https://www.idris-lang.org https://www.idris-lang.org and https://isabelle.in.tum.de https://isabelle.in.tum.de An easier alternative is to try disproving the statement, by executing it on thousands of examples and seeing if any fail. That gives us less confidence than a full proof, but can still be better than traditional "there exists" tests. This is called property checking or property-based testing. Systems I've used for this include https://hypothesis.works https://hypothesis.works https://hackage.haskell.org/package/QuickCheck https://hackage.haskell.org/package/QuickCheck https://scalacheck.org https://scalacheck.org and https://jsverify.github.io https://jsverify.github.io
  • mch82 5y ago
    Thank you for sharing your reply.