Definicja standardowego ML

Opinie czytelników

Recenzje tej książki na temat Standard ML podkreślają kontrastujące perspektywy: niektórzy czytelnicy doceniają jej precyzyjne i matematycznie rygorystyczne podejście do definicji języka, podczas gdy inni uważają ją za zbyt tajemniczą i niedostępną, szczególnie dla początkujących.

Książka zapewnia zwięzłą, dokładną i matematycznie precyzyjną definicję Standard ML, dzięki czemu idealnie nadaje się do implementacji i wnioskowania o poprawności. Służy jako lekcja tego, jak powinny być tworzone definicje języków.

Tekst jest uważany za nieprzenikniony i zbyt złożony, co sugeruje, że jest bardziej odpowiedni dla osób z zaawansowaną wiedzą, takich jak doktorzy matematyki. Istnieje obawa, że trudność może ograniczyć jego dostępność dla początkujących i utrudnić popularność języka.

(na podstawie 3 opinii czytelników)

Oryginalny tytuł:

Definition of Standard ML

Zawartość książki:

Standard ML to język programowania ogólnego przeznaczenia przeznaczony do dużych projektów. Niniejsza książka zawiera formalną definicję Standard ML z korzyścią dla wszystkich zainteresowanych tym językiem, w tym użytkowników i implementatorów.

Ponieważ od programów komputerowych coraz częściej wymaga się, aby wytrzymywały rygorystyczną analizę, tym ważniejsze jest, aby język, w którym są pisane, był zdefiniowany z pełnym rygorem. Jednym z celów definicji języka jest ustanowienie teorii znaczeń, na której może opierać się zrozumienie poszczególnych programów. Aby poprawnie zdefiniować język programowania, konieczne jest użycie jakiejś formy notacji innej niż język programowania.

Biorąc pod uwagę dbałość o rygor, oczywistym wyborem jest notacja matematyczna. Autorzy zdefiniowali swoje obiekty semantyczne w notacji matematycznej, która jest całkowicie niezależna od Standard ML. Definiując język, należy również precyzyjnie zdefiniować reguły ewaluacji - to znaczy określić, jakie znaczenie wynika z ewaluacji dowolnej frazy języka.

Definicja stanowi zatem formalną specyfikację dla implementacji. Autorzy rozwinęli wystarczająco swoją teorię, aby nadać sens swoim regułom ewaluacji. Definicja Standard ML jest podstawowym punktem odniesienia dla Standard ML.

Od czasu jej opublikowania w 1990 roku, technologia implementacji języka znacznie się rozwinęła, a liczba użytkowników wzrosła. Zmienione wydanie zawiera szereg nowych funkcji, pomija mało używane funkcje i poprawia błędy w definicjach.