Right. TLA+ and TLAPM is not used here because the requirements of handling industrial
applications require it to be a little more complicated.
I want to use formulas and decomposing them into smaller pieces. This is done using simple
definitions, rather than the more complex constructs of coding languages. To formalize mathematics
and make it easier to write a proof.
This was discussed in "How to Write a Proof" by Leslie Lamport in 1993.
Are there also other possibilities, using a variable for instance? How would one define the time
variable?
The seismogram f(t) is a stachastic generated function of time, not necessarily correlated
with an earthquake, but a more general recording of incessant earth motion.
On Thursday, November 21, 2024 at 3:31:02 PM UTC+12 Andrew Helwer wrote:
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 ?