$\{log\}$: Applications to Software Specification, Prototyping and Verification

TL;DR

This paper demonstrates how Z specifications can be translated into  and utilized for simulations and automated proofs, aiding users of other specification languages like B and VDM.

Contribution

It introduces a method for translating Z specifications into , enabling simulations and proofs, and extends usability to other specification languages.

Findings

Enables simulation of Z specifications using 

Supports automated proofs for specifications

Facilitates cross-language specification work

Abstract

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.