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:

 

  1. Download the proper Clean distribution in which the proof sections are already integrated.
  2. Extract the zip-file.
  3. Integrate the Clean IDE (Integrated Development Environment) into windows
    1. Open the Clean folder
    2. Start the Clean.exe application
    3. Click Yes when asked whether to integrate
    4. Close the IDE again using Quit from the File menu.
  4. Now you can double-click on a project file and the IDE will open automatically. Open the ioproofs project.
    1. Open the Clean folder
    2. Open the Examples folder
    3. Open the IO Proofs Example folder
    4. Double-click on the ioproofs.prj file. The Clean IDE will open it.
  5. Choose Bring Up to Date from the Project menu.
  6. Choose Theorem Prover Project from the Project menu. This opens Sparkle.
  7. Click continue acknowledging that you use an alpha release now.
  8. Press load section in the section window.
  9. 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.
  10. 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.
  11. Have fun!