Formal Method Z notation of Print spooler

Click Here to download file

The state
used, free: P BLOCKS
BlockQueue: seq P BLOCKS


Data Invariant
used > free = \
used < free  =  AllBlocks
 i: dom BlockQueue  BlockQueue i # used
 i, j : dom BlockQueue  i ≠ j => BlockQueue i > BlockQueue j = \


Precondition
         #BlockQueue > 0


Postcondition
used' = used \ head BlockQueue   
free’ = free < head BlockQueue 
BlockQueue' = tail BlockQueue