A formal specification format, where you enumerate all possible inputs and corresponding outputs. For example:
n % 3 | 
n % 5 | 
f(n) | 
|---|---|---|
| T | T | “FizzBuzz” | 
| T | F | “Fizz” | 
| F | T | “Buzz” | 
| F | F | n | 
Decision tables are extremely easy to learn; I’ve taught nonprogrammers how to use them in less than ten minutes. This makes them an excellent introduction to formal methods.