Towards Machine-Verified
Proofs for I/O
This page
contains a clean/sparkle distribution including file I/O proofs. These proofs
are referred to in the paper "Towards
Machine-Verified Proofs for I/O", authored by Malcolm Dowse, Andrew Butterfield, Marko van Eekelen, Maarten de Mol and Rinus Plasmeijer, which appeared as Technical
Report NIII-R0415 at the Nijmegen
Institute for Computing and Information Science.
Through
this page you will be able to examine the proofs and the theorems that are
'behind' the paper. The model is specified in the lazy functional programming
language Clean. The proofs are made
using Clean's dedicated proof assistant Sparkle.
The way to
play with the proofs of the paper is by proceeding conform the following steps:
- Download the proper
Clean distribution in which the proof sections are already integrated.
- Extract the zip-file.
- Integrate the Clean IDE
(Integrated Development Environment) into windows
- Open the Clean folder
- Start the Clean.exe
application
- Click Yes when asked whether
to integrate
- Close the IDE again using
Quit from the File menu.
- Now you can double-click on a
project file and the IDE will open automatically. Open the ioproofs
project.
- Open the Clean folder
- Open the Examples folder
- Open the IO Proofs Example
folder
- Double-click on the
ioproofs.prj file. The Clean IDE will open it.
- Choose Bring Up to Date from
the Project menu.
- Choose Theorem Prover Project
from the Project menu. This opens Sparkle.
- Click continue acknowledging
that you use an alpha release now.
- Press load section in the
section window.
- Load the sections channel and
mnext_fs. 49 proofs of the paper are now loaded and checked fairly
quickly. The last proof (a biggie: nr 50) will be loaded and checked if
you open the section intermingle_channel. This last proof may take 15
minutes to check if you have a 400 MHZ machine.
- Now you're off! Open a section
by clicking on its name. Press on show propositions to see the theorems.
Open a theorem to see its proof.
- Have fun!