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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 19 May 2015 22:34:28 -0700 (PDT)*References*: <436d2d6d-38d0-4423-be06-f6a730296f18@googlegroups.com>

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

**Follow-Ups**:**Re: [tlaplus] TLAPS and string search algorithms***From:*Stephan Merz

**References**:**TLAPS and string search algorithms***From:*Andrew Helwer

- Prev by Date:
**Re: TLAPS and string search algorithms** - Next by Date:
**Re: [tlaplus] TLAPS and string search algorithms** - Previous by thread:
**Re: TLAPS and string search algorithms** - Next by thread:
**Re: [tlaplus] TLAPS and string search algorithms** - Index(es):