$\{log\}$: Applications to Software Specification, Prototyping and Verification
This is an incremental contribution for software engineers and formal methods practitioners, facilitating the use of {log} in specification and verification tasks.
The paper tackles the problem of translating Z specifications into {log} to enable simulations and automated proofs, and shows that this approach can also assist users of B and VDM specification languages.
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.