This predicate is true
of every possible $id constructed from $prefix by appending an
integer. Thus (GeneratedId "thing" "thing1") would be true, as
would be (GeneratedId "thing" "thing2845728"). You can think of it
as being represented by a countably infinite set of such facts. If
$id were unbound, then (GeneratedId "thing" $id) should bind $id to
such strings. Logically speaking, it is perfectly reasonable to start
enumerating this infinite set of solutions with any $id, for example,
the $id with a number one higher than the last one you ever
generated. So long as we only ever try to find one solution, we get
the effect of generating a new id. Things get messy if you try to get
multiple solutions, since technically GeneratedId is "honour-bound"
not to fail until it has enumerated all solutions (and there are a lot
of them :-). For example, the first solution that
(and (Member $elt [1 2 3 4]) (GeneratedId "id" $id)) returns would
be something like $elt=1 $id="id57". If you forced it to look for
alternative solutions, to remain purely logical it would have to
return a different id (such as "id58") for the same element. This is
not what anyone would want, so it would be better for GeneratedId to
raise an exception rather than attempt to enumerate an infinite number
of solutions. This is more logical than failing to find another
solution, which falsely asserts that there is no other $id that can be
generated from "id". It is possible to stop SPARK from looking for
another solution to one part of a logical expression using "once",
which only seeks one solution for the subexpression. Unfortunately,
"once" is not purely logical, but it is better to have the
illogicality confined to as few predicates as possible rather than
introduce illogical predicates all over the place. Thus we could write
the following, which would return three solutions and still stay 100%
logical: (and (Member $elt [1 2 3 4]) (once (GeneratedId "id" $id)))
RandomId$prefix $id
Like GeneratedId but uses a random number generator