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

AW: [tlaplus] teaching TLA



Dear Daniel Leivant,

 

My experience shows that it is best to use Leslie’s hyperbook as the primary starting source and add (more!) theoretical background as appropriate for a possibly required understanding of related notations and/or concepts. Students tend to appreciate machine support for “thinking” quite a bit!

Another issue is the application background. The level of the “informal” understanding of the concepts of e. g. distributed systems is key before entering “formal” descriptions of it.

 

All the best

 

Fritz

 

Von: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx] Im Auftrag von Stephan Merz
Gesendet: Montag, 16. Dezember 2013 18:21
An: tla...@xxxxxxxxxxxxxxxx
Betreff: Re: [tlaplus] teaching TLA

 

Dear Daniel Leivant,

 

Leslie's hyperbook is an obvious source for many ideas for such a course, it is essentially a tutorial: http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html.

 

I have occasionally given TLA courses at summer schools, and I'll send you a set of slides off-list. For a description that focuses more on the logic of TLA, you may find some material in http://www.loria.fr/~merz/papers/tla+logic2008.html.

 

The TLA+ distribution comes with a set of a few examples for the use of the model checker. I'm not sure if these are part of the TLA+ Toolbox distribution of TLC, but they are (or at least used to be) part of the standalone (command-line) tools available from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html#downloading.

 

Best regards,

 

Stephan

 

On 16 Dec 2013, at 18:04, Daniel Leivant <lei...@xxxxxxxxxxxxxx> wrote:



I plan to incorporate next semester an introduction to TLA (and temporal logic) into a graduate introductory course on formal logic and program verification.
If anyone has any ideas, material, pointers, or experience to share, that would be tremendously helpful and greatly appreciated.

Thanks much in advance and best wishes  - Daniel

Daniel Leivant
Professor of computer science
and adjunct professor of mathematics
Indiana University Bloomington

 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.

 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.