Text this: Report on the formal specification and partial verification of the VIPER microprocessor /