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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 10 Dec 2023 11:21:52 +0100*References*: <b167372b-d453-404c-a0c7-e4a2766c6a27n@googlegroups.com> <0926889F-DAF2-45F1-AEF6-A42B04734B24@gmail.com> <CAFZmCwChio673OGeZFz5N3u4U02cHTK6FAiy2MjED83iDeJAFA@mail.gmail.com>

I'd use similar predicates to specify the intended result. For example, one way to specify the merge of two sorted integer sequences is as follows: Range(f) == {f[x] : x \in DOMAIN f} \* better: extend CommunityModules Monotonic(f) == \A x,y \in DOMAIN f : x \leq y => f[x] \leq f[y] Merge(s,t) == CHOOSE u \in Seq(Int) : /\ Len(u) = Len(s) + Len(t) /\ \E f \in [1 .. Len(s) -> 1 .. Len(u)], g \in [1 .. Len(t) -> 1 .. Len(u)] : /\ Monotonic(f) /\ Monotonic(g) /\ Range(f) \inter Range(g) = {} /\ Range(f) \union Range(g) = 1 .. Len(u) /\ \A i \in 1 .. Len(s) : u[f[i]] = s[i] /\ \A i \in 1 .. Len(t) : u[g[i]] = t[i] Note that if you'd like to evaluate this operator using TLC, you'll have to rewrite the CHOOSE so that the quantifier ranges over a finite set, for example CHOOSE u \in [1 .. Len(s) + Len(t) -> Range(s) \union Range(t)] Again, such operators just serve as a logical specification of the result, they do not describe an algorithm for computing it. Stephan
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/620FA81C-54B4-427F-AE8A-8E11F51A4F6C%40gmail.com. |

**References**:**[tlaplus] How do you think abstractly***From:*Akash Gopalkrishnan

**Re: [tlaplus] How do you think abstractly***From:*Stephan Merz

**Re: [tlaplus] How do you think abstractly***From:*Akash

- Prev by Date:
**Re: [tlaplus] How do you think abstractly** - Next by Date:
**[tlaplus] Does TLC handle <> and ~[]~ differently?** - Previous by thread:
**Re: [tlaplus] How do you think abstractly** - Next by thread:
**[tlaplus] Does TLC handle <> and ~[]~ differently?** - Index(es):