Wyone is the automated theorem prover that comes as part of the Whiley Development Kit; it is the “whiley one”. Wyone is used by the Whiley-to-Java Compiler (wyjc) to perform compile-time checking of constraints. Wyone is (roughly speaking) an SMT solver which accepts logical conditions and attempts to find a satisfying assignment, or to find a proof that no such assignment exists.
For example, consider the following logical condition (written in the language of wyone):
int x; int y; x < 0 && y > 0 && y > x
This formula has many satisfying assignments. For example, when x=-1 and y=1.
Popular Posts