[tlaplus] Re: Defining a function in terms of variables in TLA

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

If you're using this for writing proofs over it, you'll probably make the function a constant then define some set of assumptions over it. Like:

CONSTANT f

ASSUME f \in [Real -> Real]

ASSUME IsContinuous(f) /\ IsDifferentiable(f)

Where you define IsContinuous and IsDifferentiable to mean some definition you can use in proofs. However, if you want to formally verify the proofs then TLAPM does not really support reasoning over Reals at this time. Some researchers developed an extension for it which you can read about here, but this work has not yet been integrated into the main development branch.

Andrew Helwer

On Wednesday, November 20, 2024 at 5:28:20 AM UTC-5 marta zhango wrote:

How can I define a function of time or some other variable, say of a seismogram

in TLA ?  But without specifying the mapping.

Using a VARIABLE, LET, or something else ?

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/5216caa6-610a-4fbd-b7ea-58b174ac0b20n%40googlegroups.com.