PHP Warning: call_user_func_array() expects parameter 1 to be a valid callback, no array or string given in /am/paramount/vol/ecs/sites/whiley/wp-includes/class-wp-hook.php on line 298


  • No categories


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.