Question about how tla+ can do and how it works

[remuscl]

Hi, I'm new to tla+ and watching the video tutorials now, and I have two question about what tla+ could do and how it works.

There is a snippet of C code:

```c
assert(N >= 0);
for(i = 0; i < N; i++){
f(i);
}
```

We have the conclusion:

```c
N = 0: loop 0 times
N = 1: loop 1 time and equal to `f(0)`
N > 1: loop N times and equal to `f(0), f(1), f(2) ... f(N-1)`
```

Q1:
Could we use tla+ to prove the above conclusion is always true when N is ANY valid natural number (>= 0)?

Q2:
If the answer of Q1 is "yes", and how tla+ works? By the appropriate amount of sample testing or strict proof by some certain math methods which are ALWAYS right?

Thank you very much for your time.

[Ron Pressler]

On Sunday, October 14, 2018 at 2:16:17 AM UTC+1, remuscl wrote:

Hi, I'm new to tla+ and watching the video tutorials now, and I have two question about what tla+ could do and how it works.

There is a snippet of C code:

```c
assert(N >= 0);
for(i = 0; i < N; i++){
  f(i);
}
```

We have the conclusion:

```c
N = 0: loop 0 times
N = 1: loop 1 time and equal to `f(0)`
N > 1: loop N times and equal to `f(0), f(1), f(2) ... f(N-1)`
```

Q1:
    Could we use tla+ to prove the above conclusion is always true when N is ANY valid natural number (>= 0)?

Yes.

 

Q2:
    If the answer of Q1 is "yes", and how tla+ works? By the appropriate amount of sample testing or strict proof by some certain math methods which are ALWAYS right?

Thank you very much for your time.

By itself, TLA+ is a formal system -- a language with formal semantics and formal inference rules, but it is not a programming language that can be "run". This, however, allows the creation of tools that work on TLA+ specifications in various ways. One tool, included in the TLA+ Toolbox, is a model checker called TLC. It implements model-checking by a rather brute-force technique called explicit state space exploration, which is not testing samples but covers the specification's state graph exhaustively (sampling is also possible as a special mode in TLC). Because of how it works, a limitation of TLC is that it can only definitively prove a theorem about a specification with a finite number of states -- which yours isn't. However, model-checking a finite version of a specification (e.g., limiting N up to a certain number) often gives engineers enough confidence in their design.

Yet another tool is the TLA+ Proof System, or TLAPS, available for download here. It is not limited to a finite state space like TLC, but it is not fully automated. It is essentially a proof-assistant, that allows you to write a proof of a theorem you have about the specification, and it mechanically verifies that your proof is correct.

Ron

[remuscl]

Hi Ron, thank you very much for your excellent and detailed answer. It's so nice of you :-)