ABSTRACT
For many years, researchers have claimed that software specifications can be used to improve many software development activities. A formal specification documents important properties and hence is useful in understanding programs [41,67]. Formal specifications can be used to automatically generate test inputs [14, 21, 60]. Program verification needs a formal specification that defines the correct behaviors of a program [34, 41, 67]. Other uses include refining a specification into a correct program [1] and protecting a programmer from making changes that violate important invariants [26].
