TLAPS doesn't support quantification over tuples or set constructors
using tuples. That means it can't handle expressions like
\E <<x, y, z>> \in S : ...}
{<<x, y, z>> \in S : ...}
Such expressions are at best a minor convenience and are never
necessary. TLAPS supports quantification over arbitrary sets and the
use of arbitrary sets in set constructors--including sets of tuples.
TLA+ represents strings as sequences of characters, though it provides
no way to write the character 'a' except as something like "a"[1].
Thus, "abc" equals <<"a"[1], "b"[1], "c"[1]>>. However, TLAPS does
not support this and considers strings to be primitive objects. (TLC
can evaluate some operations from the Sequences module like \o and
Len on strings.)
I expect that the easiest way to represent strings in string algorithms is
as finite sequences of an unspecified set of characters.
Leslie
On Tuesday, May 19, 2015 at 11:25:48 AM UTC-7, Andrew Helwer wrote:
As a fun side-project with TLAPS, I'd like to prove correctness of some string search algorithms. However, TLAPS says it doesn't support quantification over tuples and set constructors. Would this affect ability to prove things about strings (which I guess are represented by sequences of characters)?