Numeric Types in Formal Synthesis

Autor:	Kai Kapp, Viktor K. Sabelfeld
Rok vydání:	2004
Předmět:	Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Transformation (function) Computer science Proof theory Computer Science::Logic in Computer Science Formal specification HOL Type (model theory) Arithmetic Data type Algorithm Higher-order logic
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540208136 Ershov Memorial Conference
Popis:	The Formal Synthesis methodology can be considered as the application of the transformational approach to circuit synthesis by logical transformations performed in a theorem prover. Additionally to the implementation of the circuit, the proof that the result is a correct implementation of a given specification is obtained automatically. In this paper, a higher-order formalisation for the arithmetic of bound numeric data types is given. We provide correct transformations implemented in the theorem prover HOL [4], to register-transfer level descriptions of arithmetic operations. For a restricted class of specifications, a correct transformation is described which eliminates the type num and replaces arithmetic operations by its bound variants.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::2a0e0a0df29b95c50a53c35de6e95ddb https://doi.org/10.1007/978-3-540-39866-0_10 Zobrazit plný text záznamu