--- /dev/null
+[forall u in UsedInode], u.inodestatus=literal(Used)
+[forall f in FreeInode], f.inodestatus=literal(Free)
+[forall u in UsedBlock], u.blockstatus=literal(Used)
+[forall f in FreeBlock], f.blockstatus=literal(Free)
+[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof) or i in RootDirectoryInode
+[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192)
+[forall b in FileDirectoryBlock],sizeof(b.~contents)=1
+[],sizeof(SuperBlock)=1
+[],sizeof(GroupBlock)=1
+[],sizeof(InodeTableBlock)=1
+[],sizeof(InodeBitmapBlock)=1
+[],sizeof(BlockBitmapBlock)=1
+[],sizeof(RootDirectoryInode)=1