File Refinement

Karen Zee 🌐 and Viktor Kuncak 🌐

December 9, 2004


These theories illustrates the verification of basic file operations (file creation, file read and file write) in the Isabelle theorem prover. We describe a file at two levels of abstraction: an abstract file represented as a resizable array, and a concrete file represented using data blocks.


BSD License


Session FileRefinement