Look up "model checking" and see how that compares to what you're thinking about. How would you specify tests (or rather, correct program behavior) in such a language?

The languages Alloy and TLA+ come to mind. (So does Coq, which is at the other extreme of actually proving your program correct.)