Formal Verification of Data Type Refinement - Theory and Practice
Tobias Nipkow
This paper develops two theories of data abstraction and refinement: one for
applicative types, as they are found in functional programming languages, and
one for state-based types found in imperative languages. The former are
modelled by algebraic structures, the latter by automata. The
automaton-theoretic model covers not just data types but distributed systems
in general. Within each theory two examples of data refinement are presented
and formally verified with the theorem prover Isabelle. The examples are an
abstract specification and two implementations of a memory system, and a
mutual exclusion algorithm.
dvi
SpringerLink
BibTeX:
<![CDATA[
@inproceedings{Nipkow-REX,
author="Tobias Nipkow",
title="Formal Verification of Data Type Refinement --- Theory and Practice",
booktitle="Stepwise Refinement of Distributed Systems",
editor="J.W. de Bakker and W.-P. de Roever and G. Rozenberg",
year=1990,publisher=Springer,series=LNCS,volume=430,pages="561--591"}
]]></plaintext></p></div></div>