登入選單

返回Google圖書搜尋

A Ruby Proof System

Ole Rasmussen

出版	Department of Computer Science, Technical University of Denmark, 1995
URL	http://books.google.com.hk/books?id=3HjxHAAACAAJ&hl=&source=gbs_api

註釋

Abstract: "This report descibes a semantical embedding of the relation based language Ruby in Zermelo-Fraenkel set theory (ZF) using the Isabelle theorem prover. A small subset of Ruby, called Pure Ruby, is embedded as a conservative extension of ZF and characterised by an inductive definition. Many useful structures used in connection with VLSI design are defined in terms of Pure Ruby and their properties proved. Finally, we demonstrate how various kinds of proofs may be automated and the explicit type checking of ZF hidden by the definition of specialised tactics."