Introducing SymTest – the Bosque symbolic testing tool
If you have installed Bosque on your system, you will also have installed SymTest. It's a command-line program designed to symbolically test the Bosque source code. A deep analysis of how it works internally is out of the scope of this book. However, there are a couple of facts that are worth pointing out. Under the hood, SymTest uses something called Z3 Theorem Prover. It is a Satisfiability Modulo Theories (SMT) solver created by Microsoft. SMT problem is a mathematical logic term that refers to a decision problem for logical formulas. In fact, the definition is a lot more complicated and touches on many topics in the field of math. For the sake of this chapter, it is enough to know that it is a kind of mathematical logic problem that can be expressed using a set of formulas. This kind of problem needs to be solved using a symbolic analysis of a computer program, and that's why SymTest uses an SMT solver. In...