File Refinement (Q7361390)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry FileRefinement
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | File Refinement |
AFP entry FileRefinement |
Statements
9 December 2004
0 references
Karen Zee
0 references
Viktor Kuncak
0 references
File Refinement (English)
0 references
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.
0 references
