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

*From*: Ron Pressler <ron.pr...@xxxxxxxxx>*Date*: Sun, 14 Oct 2018 04:56:45 -0700 (PDT)*References*: <0ec61b21-73b1-43a6-9b59-50ca8cbef284@googlegroups.com>

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

**Follow-Ups**:**Re: Question about how tla+ can do and how it works***From:*remuscl

**References**:**Question about how tla+ can do and how it works***From:*remuscl

- Prev by Date:
**Question about how tla+ can do and how it works** - Next by Date:
**Re: Question about how tla+ can do and how it works** - Previous by thread:
**Question about how tla+ can do and how it works** - Next by thread:
**Re: Question about how tla+ can do and how it works** - Index(es):