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

Re: [tlaplus] Function domains in TLAPS

Just knowing that g[3] = 8 doesn't allow you to infer that g is a function or to conclude anything about DOMAIN g, so TLAPS does the right thing. (For example, 42[3] denotes some unspecified value in TLA+, would you want to conclude that 42 is a function?) You want to state "type predicates" for the functions that appear in your specification – typically as ASSUME clauses for constant parameters, and as invariants for variables.

Best regards,

On 14 Jun 2016, at 16:09, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:


I've noticed that TLAPS does not automatically deduce anything about a function's domain from facts about its mapping. E.g., the lemma in the following snippet fails:


    AXIOM A == g[3] = 8

    LEMMA 3 \in DOMAIN g BY A

This means that axioms must be specified/theorems proven separately for functions' mappings and their domains, which is extra work. Is this an artifact of the logic (if 3 is outside f's domain, f[3] may be anything, and if I know it's 8, that doesn't mean that 3 is in the domain) or just a limitation of TLAPS?


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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.