1999 | OriginalPaper | Chapter
Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems
Authors : Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury
Published in: Automated Deduction — CADE-16
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstraction is a useful tool in verification, often allowing the proof of correctness of a large and complex system to be reduced to showing the correctness of a much smaller simpler system. We use the Nuprl theorem prover to verify the correctness of a simple but commonly occurring abstraction. From the formal proof, we extract a program that succeeds when the abstraction method is applicable to the concrete input specification and in this case, computes the abstracted system specification. One of the main novelties of our work is our “implicit syntax” approach to formal metatheory of programming languages. Our proof relies entirely on semantic reasoning, and thus avoids the complications that often arise when formally reasoning about syntax. The semantic reasoning contains an implicit construction of the result using inductive predicates over semantic domains that express representability in a particular protocol language. This implicit construction is what allows the synthesis of a program that transforms a concrete specification to an abstract one via recursion on syntax.