Ensuring Correctness of Ruby Transformations
Ole Rasmussen · Electronic workshops in computing · 1996
Equivalence transformations are widely used in practical designs of VLSI circuits using Ruby. This paper demon-strates how proofs of these equivalences easily may be performed within a formal framework by a theorem prover. The proof tool used is called RubyZF and contains a semantical embedding of Ruby within Zermelo-Fraenkel set theory using the Isabelle theorem prover. The use of the system is exemplified by a concrete example taken from the T-Ruby design system.