[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLAPS and string search algorithms



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

On 20 May 2015, at 07:34, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

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