  Formal techniques have been shown to be useful in the development of correct
software. But the level of expertise required of practitioners of these
techniques prohibits their widespread adoption. Formal techniques need to be
tailored to the commercial software developer. Alloy is a lightweight
specification language supported by the Alloy Analyzer (AA), a tool based on
off-the-shelf SAT technology. The tool allows a user to check interactively
whether given properties are consistent or valid with respect to a high-level
specification, providing an environment in which the correctness of such a
specification may be established. However, Alloy is not particularly suited to
expressing program specifications and the feedback provided by AA can be
misleading where the specification under analysis or the property being checked
contains inconsistencies. In this paper, we address these two shortcomings.
Firstly, we present a lightweight language called "Loy", tailored to the
specification of object-oriented programs. An encoding of Loy into Alloy is
provided so that AA can be used for automated analysis of Loy program
specifications. Secondly, we present some "patterns of analysis" that guide a
developer through the analysis of a Loy specification in order to establish its
correctness before implementation.
