Specifications are Preferably Amenable to Proof and Animation

The influential article “Specifications are not (necessarily) executable” by Hayes and Jones from 1989 argues that a formal specification should not be overcomplicated or over-specified due to the secondary goal of making the specification executable. In this paper, we examine to what extent the following two goals can be reconciled: 1) developing natural high-level specifications not marred by implementation aspects and 2) bringing these high-level specifications to life to detect inconsistencies. We first review the examples of non-executable specifications from the paper by Hayes and Jones, and check to what extent they can now be animated 35 years later by the ProB validation tool, and other current tools. We also present an approach for writing high-level specifications for proof and readability, while creating instances for animation, execution, visualization and model checking.