Changes between Version 15 and Version 16 of Language

Timestamp:

05/18/23 20:43:36 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -476 +476 @@
 This mechanism serves as a "widening operator" (in the sense of abstract interpretation), which enables symbolic execution to converge.
 
-
-=== `$choose_int`
+=== Nondeterministic choice of integer: `$choose_int`
+
+This function has signature
+{{{
+$system int $choose_int(int n);
+}}}
+and returns an arbitrary integer in [0.''n''-1].  In verification mode, all possible choices are enumerated and explored.
 
 === `$default_value`