Customer Reviews

Action Semantics (Cambridge Tracts in Theoretical Computer Science)

5 star:		(1)
4 star:		(0)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

Action Semantics covers in detail an algebra used to define almost all kinds of high level programming languages in a feasible manner - it is easy to read and understand the description informally, yet it is 100% formal and very expressive. The book is well written, but requires concentrated reading as there are few superfluous or repeated statements, as opposed to american literature. The reader is assumed to have a certain degree of knowledge of programming languages, different styles of semantics and related theory to gain the full benefit of the book.
Moreover, AS has shown itself interesting in automated (efficient and provably correct) compiler generation (refer to http://www.brics.dk/Projects/AS for details).

An Action Semantics-description is divided into a syntactic description of the language, semantic functions defining the mapping of syntax to entities, and semantics entities defining the computations on the entities operated on by the language. All three parts are described in Action Notation, making the syntax more expressive than EBNF and the computations more expressive than SOS or lambda calculi.

After having introduced the requirements and basic ideas, the book slowly guides the reader through the concepts, their raison d'etre and their use, by slowly applying them to a growing subset of Ada, starting with simple imperative constructs and ending with a description including agents and exceptions. The appendices gives the full, formal definition of the syntax, data notation, action notation and more. Formal proofs of some of the properties claimed to hold for AS are missing, but many pointers to further information given.

Having read the book and some of the papers in the rigourous bibliography, it seems to me that AS is one feasible way to go when discussing descriptions of programming languages, that can at the same time be read as a manual of the language, a formal description allowing for the proofs of certain properties of the language to be made, and input for a compiler generator for the specified language. The only serious shortcomings I see, is the description of continuation-passing-style constructs as found in Scheme/SML and the like, and the fact that the framework is not (yet?) widely known/used. The latter problem can be remedied by reading the book.