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

*From*: remuscl <remus.cl...@xxxxxxxxx>*Date*: Sat, 13 Oct 2018 18:16:16 -0700 (PDT)

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.

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

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