TLAPS and string search algorithms

[Andrew Helwer]

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)?

[Y2i]

Andrew, would quantification over tuple domain be useful for your project?

\A i \in DOMAIN(<<1,2,3,4,5>>) : i < 6

[Leslie Lamport]

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:

[Stephan Merz]

Actually, the following works:

LEMMA "abc" = <<"a"[1], "b"[1], "c"[1]>>

OBVIOUS

It is proved by the Isabelle backend, which faithfully encodes strings as sequences of characters, while the other backends fail. However, I do not expect this to scale very far, and agree with Leslie that string algorithms are best modeled as operating over an unspecified set of characters.

Stephan