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

Question about how tla+ can do and how it works

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:

assert(N >= 0);
for(i = 0; i < N; i++){

We have the conclusion:

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)`

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

    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.