Definizione di ML standard

Recensioni dei lettori

Le recensioni di questo libro sullo Standard ML evidenziano prospettive contrastanti: alcuni lettori apprezzano il suo approccio preciso e matematicamente rigoroso alle definizioni del linguaggio, mentre altri lo trovano eccessivamente criptico e inaccessibile, soprattutto per i principianti.

Il libro fornisce una definizione sintetica, accurata e matematicamente precisa dello Standard ML, rendendolo ideale per l'implementazione e il ragionamento sulla correttezza. È una lezione su come dovrebbero essere realizzate le definizioni dei linguaggi.

La scrittura è considerata impenetrabile ed eccessivamente complessa, suggerendo che è più adatta a chi ha conoscenze avanzate, come i dottori in matematica. Si teme che la difficoltà possa limitare l'accessibilità ai principianti e ostacolare la popolarità del linguaggio.

(basato su 3 recensioni dei lettori)

Titolo originale:

Definition of Standard ML

Contenuto del libro:

Standard ML è un linguaggio di programmazione di uso generale progettato per grandi progetti. Questo libro fornisce una definizione formale di Standard ML a beneficio di tutti coloro che si occupano del linguaggio, compresi gli utenti e gli implementatori.

Poiché sempre più spesso i programmi per computer devono essere sottoposti a un'analisi rigorosa, è ancora più importante che il linguaggio in cui sono scritti sia definito con pieno rigore. Uno degli scopi della definizione di un linguaggio è quello di stabilire una teoria dei significati su cui basare la comprensione di particolari programmi. Per definire correttamente un linguaggio di programmazione, è necessario utilizzare una forma di notazione diversa dal linguaggio di programmazione.

Data la preoccupazione per il rigore, la notazione matematica è una scelta ovvia. Gli autori hanno definito i loro oggetti semantici in una notazione matematica completamente indipendente dallo standard ML. Nel definire un linguaggio si devono anche definire con precisione le regole di valutazione, cioè definire quale significato risulta dalla valutazione di qualsiasi frase del linguaggio.

La definizione costituisce quindi una specifica formale per un'implementazione. Gli autori hanno sviluppato abbastanza la loro teoria per dare un senso alle loro regole di valutazione. La Definizione di Standard ML è il punto di riferimento essenziale per lo Standard ML.

Dalla sua pubblicazione nel 1990, la tecnologia di implementazione del linguaggio è progredita enormemente e il numero di utenti è cresciuto. L'edizione rivista include una serie di novità, omette funzioni poco utilizzate e corregge errori di definizione.