Alloy 4, Software Abstractions 2E, and the seq keyword

Question

Not long ago I acquired the second edition of Software Abstractions, and when I needed to refresh my memory on how to spell the name of the elems function I thought "Oh, good, I can check the new edition instead of trying to read my illegible handwritten notes in the end-papers of the first edition."

But I can't find "seq" or "elems" or the names of any of the other helper functions in the index, nor do I see any mention of the seq keyword in the language reference in Appendix B.

One or more of the following seems likely to be the case; which?

• I am missing something. (What? where?)
• The seq keyword is not covered in Appendix B because it's not strictly speaking a keyword in the way that set and the other unary operators are. (Please expound!)
• The support for sequences was added to Alloy 4 after the second edition went to press, and so the book needs to be augmented by reference to the discussion of new features in Alloy 4 in the Quick Guide and the Alloy 4 grammar on the Web site. (Ah, OK. Pages are slow, bits are fast.)
• Other ...

I guess, to try to put a generally useful question here, that I'm asking: what exactly is the relation between the language implemented by the Alloy Analyzer 4.2 (or any 4.*) and the language defined in Software abstractions second edition?

Answer 1

The current implementation corresponds to this online documentation.

Sequences are really not part of the language; x: seq A can be seen just as a syntactic sugar for x: Int -> A, and all the utility functions (e.g., first, last, elems) are library-defined (in util/sequence). The actual implementation is a little more complicated (just so that we can let the user write something like x.elems and make the type checker happy at the same time), but conceptually that's what's going on.