Articles

  • No categories

Wyone

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.