Specification of Viper1 in Z
D. H. Kemp · 1988
Abstract : As a continuation of the use of the specification language Z which was used to specify the Viper 1 microprocessor this paper covers the specification of the Viper 2. This was completed before the definitive HOL specification was complete, therefore there is no proof of correspondence between the two. Using Z did highlight inconsistencies in the HOL specification that may not have appeared until later in the specification. Great Britain.