Articles

Generating Verification Conditions for Whiley

Probably the most interesting aspect of the Whiley language is that it supports compile-time verification of preconditions, postconditions and other invariants.  There are two main aspects of how this works:

Generation of Verification Conditions (VCs) from the source code.  A verification condition is a logical expression which, if proved to be satisfiable, indicates an . . . → Read More: Generating Verification Conditions for Whiley