File System Layer Models

There has been a restructuring of all models, and for that, some of them aren't available yet. If you are looking for any thing ins specific please contact us.

VDM++

• src_vdm.tar.bz: FileSystemLayer (VDM++)
  • Implemented Operations:
    • FS_DeleteFileDir
    • FS_OpenFileDir
    • FS_WriteFile
  • Operations to be implemented:
    • FS_ReadFileDir
    • FS_Init

Alloy

• src_alloy.tar.bz: FileSystemLayer (Alloy)
  • Implemented Operations:
    • FS_DeleteFileDir
  • Operations to be implemented:
    • FS_OpenFileDir
    • FS_WriteFile
    • FS_ReadFileDir
    • FS_Init

VDM++ adapted for VdmHolTranslator and HOL translation

Model

• src_vdm2hol.tar.gz: FileSystemLayer (VDM2HOL)
  • Implemented Operations:
    • FS_DeleteFileDir
  • Operations to be implemented:
    • FS_OpenFileDir
    • FS_WriteFile
    • FS_ReadFileDir
    • FS_Init

Proof Obligations

• The VDMTools generated 13 Proof Obligations, from which:
  • 3 aren't translatable to HOL with the VdmHolTranslator. These can be found in the excluded.pog file
  • 10 where translated to HOL by the VdmHolTranslator. These can be found in the FileSystemLayerAlg.vpp.pog file.
    • 7 of these Proof Obligations where discharged in HOL using the Overture Automated Proof Support
    • for the remaining 3 Proof Obligations HOL attempted to prove for more than 5 minutes and was manually interrupted.

• HOL model and Proof Obligations can be found in the:
  • FileSystemLayerAlg.vpp.pog.hol (for the unmodified version)
  • FileSystemLayerAlg.vpp.pog.hol.mod (for the executable version)

HOL (hand written)

• Will be published soon

Proof attempts by hand (point free style)

• Calculation of weakest pre-condition for preservation of referential integrity invariant on open files can be found here, on Lecture 5 (page 144).