# File Refinement

 Title: File Refinement Authors: Karen Zee and Viktor Kuncak Submission date: 2004-12-09 Abstract: 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. BibTeX: @article{FileRefinement-AFP, author = {Karen Zee and Viktor Kuncak}, title = {File Refinement}, journal = {Archive of Formal Proofs}, month = dec, year = 2004, note = {\url{https://isa-afp.org/entries/FileRefinement.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License