File Refinement

Karen Zee 🌐 and Viktor Kuncak 🌐

December 9, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session FileRefinement

Cite

× 
@article{FileRefinement-AFP,
  author  = {Karen Zee and Viktor Kuncak},
  title   = {File Refinement},
  journal = {Archive of Formal Proofs},
  month   = {December},
  year    = {2004},
  note    = {\url{https://isa-afp.org/entries/FileRefinement.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: