If you liked that book, Software Abstractions is the Alloy version. It has some great examples and exercises. Easily translatable to TLA+. And I think the lessons demonstrate well why writing specifications is helpful.
From there, if you’ve digested those books then get to writing some specifications. Join the mailing lists or find a group on discord or slack or something. Try modelling an elevator. Make sure that every person that calls the elevator eventually arrives at their requested floor. Pick a favourite async library and see if you can model its structures and functionality. The important thing is to exercise that muscle and make mistakes.
agentultra|1 year ago
From there, if you’ve digested those books then get to writing some specifications. Join the mailing lists or find a group on discord or slack or something. Try modelling an elevator. Make sure that every person that calls the elevator eventually arrives at their requested floor. Pick a favourite async library and see if you can model its structures and functionality. The important thing is to exercise that muscle and make mistakes.
wiktor-k|1 year ago
Just for completeness apparently Alloy is at version 6 now (http://alloytools.org/alloy6.html) and the book is based on version 4 (http://alloytools.org/book.html). There's another resource linked on the site: https://haslab.github.io/formal-software-design/