Re: quick question about TLA

Dear Yining Liu,

may I suggest that you start by reading some of the introductory material on TLA+, in particular the hyperbook available from http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html. It is a tutorial introduction that will give you a much clearer idea on what TLA+ is intended for than what a forum discussion could achieve.

The main difference to a programming language is that TLA+ is not a priori executable, although you can use the model checker to simulate a significant fragment of the language. TLA+ is meant for precisely describing algorithms, at appropriate levels of abstraction.

Regards,

Stephan

On Sunday, December 6, 2015 at 10:26:58 AM UTC+1, Floria wrote:

Dear TLA+ community member,

How are you? This is Yining Liu from Beijing China. I am a math-major student in college.

I first heard about TLA+ at Mr. Lamport's presentation in Tsinghua University this November, and began very interested in it for its powerful engineering application he described. I feel like it is very different from the programming languages like C and R, and I am wondering what exactly the specifications can do. Will it be able to do basic calculations like 1+2? Will it be able to form for loops? Will it be able to solve differential equations?

I would be really appreciated if you can offer me some instructions and examples for the questions mentioned. Thank you so much for your time!!

Best,
Yining

School of Information

Renmin University of China

No. 59 Zhongguancun Street, Haidian District Beijing

(100872)

Cell Phone:+86-15652992529