Formal Method (object constraint language) of Print spooler

Click here to download file

No block will be marked as both unused and used.
  context BlockHandler inv:
    (self.used->intersection(self.free)) ->isEmpty()
All the sets of blocks held in the queue will be subsets of the collection of currently used blocks.
  context BlockHandler inv:
    blockQueue->forAll(aBlockSet | used->includesAll(aBlockSet ))
No elements of the queue will contain the same block numbers.
  context BlockHandler inv:
    blockQueue->forAll(blockSet1, blockSet2 |
      blockSet1 <> blockSet2 implies
      blockSet1.elements.number->excludesAll(blockSet2.elements.number))
The expression before implies is needed to ensure we ignore pairs where both elements are the same Block.
The collection of used blocks and blocks that are unused will be the total collection of blocks that make up files.
  context BlockHandler inv:
    allBlocks = used->union(free)
The collection of unused blocks will have no duplicate block numbers.
  context BlockHandler inv:
    free->isUnique(aBlock | aBlock.number)
The collection of used blocks will have no duplicate block numbers.
  context BlockHandler inv:
    used->isUnique(aBlock | aBlock.number)