  This document shows how Z specifications can be translated into $\{log\}$
and, later, on how $\{log\}$ can be used to run simulations and automated
proofs. This can help users of other specification languages such as B and VDM
to use $\{log\}$ along the same lines. The presentation is rather informal and
user-oriented. More technical and formal presentations can be found in the
papers published by the authors. We also assume the reader has at least a basic
knowledge of the Z notation.
