Date: Fri, 13 Apr 2007 08:47:45 -0400
From: Daniel Jackson

That's an interesting question. Perhaps someone out there has thought
about this. I don't have much to suggest, except to point out that
the way you build a spec in a model-based language like Alloy is very
different from how you do it in an equational language like Larch. As
you no doubt know, in Larch you consider applying observers to terms
made with the constructors; in Alloy, you construct the state
directly with sets and relations. You may find the books on Z and VDM
helpful in understanding the model-based approach, or you could just
dive into Alloy with my book. You could probably translate Larch very
directly into Alloy, since it's first order, representing the
constructors and observers as relations. It would be a rather
unnatural way to write Alloy, but it would be entertaining to see the
result. You'd have some trouble with "generated by", because of
Alloy's finite model limitation (see section 5.2 of my book).

Larch was a major influence an Alloy, more methodologically than
semantically -- in the idea of checkable redundancy (assert in Alloy,
implies in Larch), and in the idea of "formal specification as a design tool"
(see http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=567471).