Initial state (JSON)
Hoare assertions (when tool = Verify Hoare)
Assertions are Python expressions (not While syntax).
Use and, or, not for booleans;
== for equality; // for integer divide;
% for modulo. Sample schema is JSON: {"n": [0, 30]} means n random in [0, 30].