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

[tlaplus] Re: university courses using TLA+?

      In Victoria university Wellington New Zealand I am teaching 23 students in a  400 level course on applied formal methods.  This year is the first year using TLA+, previous years used  Spark Ada  and Event B.
     Personally there is a lot about TLA+ that I like. But, of course, a lot of frustrations.  Certainly the PlusCal extension is essential for the students to be able to do much in a single course.  I will have a better idea how easy it was for the students to cope with at the end of the course, or at the end of next years course.  Finding easy high level strategies for applying TLA+ and strategies for debugging TLA+ specs has consumed a lot of time. But, hopefully next year I will be more able  to help the students in these areas.

kind regards david

On Friday, 26 April 2019 07:57:56 UTC+12, markos...@xxxxxxxxxxxxxx wrote:
Dear All,

Hillel Wayne made me aware of Murat Demirbas using TLA+/PlusCal as part of teaching distributed algorithms. I imagine it can be used in many more courses and would like to hear of experiences. For example, does someone have experience using it in an analysis of algorithms course? Any other course?

Thanks and best regards,


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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.