Ocena:
Książka została dobrze przyjęta jako doskonałe wprowadzenie do rozumowań temporalnych i metod formalnych, chwalona za przejrzystość i wciągający język. Jest odpowiednia zarówno dla początkujących, jak i doświadczonych czytelników, czyniąc złożone tematy bardziej zrozumiałymi. Niektórzy recenzenci zauważyli jednak, że brakuje jej głębi w niektórych aspektach teoretycznych.
Zalety:⬤ Świetnie napisana, wciągająca i łatwa w odbiorze.
⬤ Dobre wprowadzenie do rozumowania temporalnego zarówno dla nowicjuszy, jak i ekspertów.
⬤ Sprawia, że złożone tematy stają się przystępne nawet dla licealistów.
⬤ Zawiera praktyczne, rzeczywiste przykłady, które pomagają w zrozumieniu specyfikacji systemu.
⬤ Polecana osobom zainteresowanym współbieżnością i projektowaniem systemów rozproszonych.
⬤ Brakuje głębi w podstawowych teoriach, takich jak intuicjonizm i Z-notacja.
⬤ Niektóre treści są bardziej ukierunkowane na praktyczne zastosowania niż kompleksowe ramy teoretyczne.
⬤ Wyrażono chęć wydania nowszej edycji obejmującej TLA+2.
(na podstawie 7 opinii czytelników)
Specifying Systems: The Tla+ Language and Tools for Hardware and Software Engineers
Ta książka jest destylacją ponad 25 lat pracy jednego z najbardziej znanych informatyków na świecie. Specyfikacja to pisemny opis tego, co system powinien robić, a także sposób sprawdzenia, czy działa.
Określenie systemu pomaga nam go zrozumieć. Dobrym pomysłem jest zrozumienie systemu przed jego zbudowaniem, więc dobrym pomysłem jest napisanie specyfikacji systemu przed jego wdrożeniem. Najskuteczniejszym narzędziem do opisu specyfikacji jest Temporal Logic of Actions (TLA), ponieważ zapewnia matematyczne, tj.
precyzyjne, podstawy do opisywania systemów.
TLA+ jest językiem opracowanym przez autora do pisania specyfikacji matematycznych. TLA+ jest dostępny za darmo w sieci.
Może być używany zarówno dla oprogramowania, jak i sprzętu. W rzeczywistości Intel używa TLA+ z wielkim sukcesem przy projektowaniu nowego układu scalonego. Książka podzielona jest na cztery części.
Pierwsza część zawiera wszystko, co większość programistów i inżynierów musi wiedzieć o pisaniu specyfikacji. Druga część zawiera bardziej zaawansowany materiał dla bardziej zaawansowanych czytelników. Trzecia i czwarta część stanowią podręcznik referencyjny dla TLA+ - zarówno samego języka, jak i jego narzędzi.